Alonso-Ovalle & Menéndez-Benito (2010): modal indefinites

Spanish algún conveys that at least two individuals in its domain are possibilities — the Modal Variation component (18), ModalVariation — where German irgendein conveys the stronger Free Choice component (13c), FreeChoice: in the hide-and-seek scenario (15) Pedro can use algún with the bathroom ruled out (hideAndSeek), and under uniqueness Free Choice entails Modal Variation but not conversely (modalVariation_of_freeChoice). The component is a conversational implicature: as a presupposition it would make the negated (36) contradictory (not_modalVariation_of_box_empty), and it is cancellable (42), absent under downward entailing operators (43)–(44), and reinforceable (45d).

The paper derives it from an anti-singleton constraint (53)–(54) on the subset selection function algún takes (algún), which excludes the singleton restrictors of (47)/(49) (algún_ne_one_of_singleton). The competitors (58) are the singleton subdomains; their falsity under a necessity modal (59) gives Modal Variation (modalVariation_of_box), and under a possibility modal, where some competitor must be true (exists_singleton_of_diamond), the anti-exhaustivity implicatures (67)–(68) do (modalVariation_of_singletons). A domain widener competes with every proper subdomain (70), and the same reasoning yields Free Choice (freeChoice_of_proper). Without uniqueness the blocked exhaustivity inference (76) and the plural competitor (77) give ignorance of number (numberIgnorance_of_competition), which uniqueness makes unavailable (not_numberIgnorance_of_uniqueness) — the two parameters of Table 1. The scenario verdicts (24)–(30) are checked in rows_agree.

References

• [AOMB10]
• [KS17]
• [Chi06]
• [vF00b]
• [Day97]
• [Sch02]
• [Pot05]
• [Zim00]
• [JT06]

Subset selection functions (§4.1)

def AlonsoOvalleMenendezBenito2010.IsSingleton {E : Type u_1} (f : Finset E → Finset E) : Prop

A singleton subset selection function (52).

Equations

• AlonsoOvalleMenendezBenito2010.IsSingleton f = ∀ (P : Finset E), (f P).card = 1

def AlonsoOvalleMenendezBenito2010.IsAntiSingleton {E : Type u_1} (f : Finset E → Finset E) : Prop

An anti-singleton subset selection function (53).

Equations

• AlonsoOvalleMenendezBenito2010.IsAntiSingleton f = ∀ (P : Finset E), (f P).card ≠ 1

noncomputable def AlonsoOvalleMenendezBenito2010.un {E : Type u_1} {W : Type u_2} (f : Finset E → Finset E) (P : Finset E) (Q : W → E → Prop) : W → SignType

un (50) quantifies existentially over the subdomain that f selects from P.

Equations

• AlonsoOvalleMenendezBenito2010.un f P Q w = SignType.ofProp (∃ x ∈ f P, Q w x)

noncomputable def AlonsoOvalleMenendezBenito2010.algún {E : Type u_1} {W : Type u_2} (f : Finset E → Finset E) (P : Finset E) (Q : W → E → Prop) : W → SignType

algún (54) is un, defined only for an anti-singleton f.

Equations

• AlonsoOvalleMenendezBenito2010.algún f P Q = {_w : W | AlonsoOvalleMenendezBenito2010.IsAntiSingleton f}.indicator (AlonsoOvalleMenendezBenito2010.un f P Q)

theorem AlonsoOvalleMenendezBenito2010.algún_ne_one_of_singleton {E : Type u_1} {W : Type u_2} {f : Finset E → Finset E} (hf : ∀ (P : Finset E), f P ⊆ P) {P : Finset E} (hP : P.card = 1) (Q : W → E → Prop) (w : W) : algún f P Q w ≠ 1

On a singleton restrictor (46)–(49) an anti-singleton selection returns no domain, so algún's claim cannot be true where un's can.

Non-uniqueness (§5)

def AlonsoOvalleMenendezBenito2010.NumberIgnorance {E : Type u_1} {W : Type u_2} (R : SetRel W W) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] : Prop

Ignorance with respect to number holds when the number of witnesses varies across the accessible worlds.

Equations

• One or more equations did not get rendered due to their size.

theorem AlonsoOvalleMenendezBenito2010.modalVariation_of_numberIgnorance {E : Type u_1} {W : Type u_2} (R : SetRel W W) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (h : NumberIgnorance R w D Q) : Exhaustification.ModalVariation R w D Q

theorem AlonsoOvalleMenendezBenito2010.numberIgnorance_of_competition {E : Type u_1} {W : Type u_2} (R : SetRel W W) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (hc : ModalLogic.Box R (Exhaustification.claim Q D) w) (h₁ : ¬ModalLogic.Box R (fun (v : W) => (Exhaustification.witnesses D Q v).card = 1) w) (h₂ : ¬ModalLogic.Box R (fun (v : W) => 2 ≤ (Exhaustification.witnesses D Q v).card) w) : NumberIgnorance R w D Q

With the exhaustivity inference of a singleton domain blocked and the plural competitor (77) unassertable, a true claim conveys ignorance of number ((76)–(78)).

theorem AlonsoOvalleMenendezBenito2010.not_numberIgnorance_of_uniqueness {E : Type u_1} {W : Type u_2} (R : SetRel W W) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (hU : Exhaustification.Uniqueness R w D Q) (h : ModalLogic.Box R (Exhaustification.claim Q D) w) : ¬NumberIgnorance R w D Q

Under uniqueness a true claim fixes the number of witnesses at one in every accessible world, so ignorance of number conflicts with the common ground.

The scenarios

inductive AlonsoOvalleMenendezBenito2010.Room : Type

The hiding places; the domain of habitación de la casa is the house.

• bedroom : Room
• livingRoom : Room
• bathroom : Room
• kitchen : Room
• barn : Room

@[instance_reducible]

instance AlonsoOvalleMenendezBenito2010.instDecidableEqRoom : DecidableEq Room

Equations

• AlonsoOvalleMenendezBenito2010.instDecidableEqRoom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlonsoOvalleMenendezBenito2010.instFintypeRoom : Fintype Room

Equations

• One or more equations did not get rendered due to their size.

def AlonsoOvalleMenendezBenito2010.inRoom (w r : Room) : Prop

Worlds are Juan's hiding places.

Equations

• AlonsoOvalleMenendezBenito2010.inRoom w r = (w = r)

@[instance_reducible]

instance AlonsoOvalleMenendezBenito2010.instDecidablePredRoomInRoom (w : Room) : DecidablePred (inRoom w)

Equations

• AlonsoOvalleMenendezBenito2010.instDecidablePredRoomInRoom w r = AlonsoOvalleMenendezBenito2010.instDecidablePredRoomInRoom._aux_1 w r

@[reducible, inline]

abbrev AlonsoOvalleMenendezBenito2010.house : Finset Room

Equations

• One or more equations did not get rendered due to their size.

def AlonsoOvalleMenendezBenito2010.epist (A : Finset Room) : SetRel Room Room

Pedro's epistemic alternatives, the rooms he takes to be possible from any world.

Equations

• AlonsoOvalleMenendezBenito2010.epist A = SetRel.ofSuccessors fun (x : AlonsoOvalleMenendezBenito2010.Room) => ↑A

@[instance_reducible]

instance AlonsoOvalleMenendezBenito2010.instDecidableMemProdRoomSetRelEpistMk (A : Finset Room) (w r : Room) : Decidable ((w, r) ∈ epist A)

Equations

• AlonsoOvalleMenendezBenito2010.instDecidableMemProdRoomSetRelEpistMk A w r = AlonsoOvalleMenendezBenito2010.instDecidableMemProdRoomSetRelEpistMk._aux_1 A w r

@[reducible, inline]

abbrev AlonsoOvalleMenendezBenito2010.pedro15 : Finset Room

Pedro rules out the bathroom and the kitchen (15).

Equations

• AlonsoOvalleMenendezBenito2010.pedro15 = {AlonsoOvalleMenendezBenito2010.Room.bedroom, AlonsoOvalleMenendezBenito2010.Room.livingRoom}

@[reducible, inline]

abbrev AlonsoOvalleMenendezBenito2010.pedro23 : Finset Room

Pedro considers only the bathroom (23).

Equations

• AlonsoOvalleMenendezBenito2010.pedro23 = {AlonsoOvalleMenendezBenito2010.Room.bathroom}

@[reducible, inline]

abbrev AlonsoOvalleMenendezBenito2010.pedro27 : Finset Room

Pedro considers the other rooms or the barn (27).

Equations

• AlonsoOvalleMenendezBenito2010.pedro27 = {AlonsoOvalleMenendezBenito2010.Room.bedroom, AlonsoOvalleMenendezBenito2010.Room.livingRoom, AlonsoOvalleMenendezBenito2010.Room.barn}

inductive AlonsoOvalleMenendezBenito2010.Candidate : Type

The candidates of (29); worlds are the permitted hires.

• phdA : Candidate
• phdB : Candidate
• noPhd : Candidate

@[instance_reducible]

instance AlonsoOvalleMenendezBenito2010.instDecidableEqCandidate : DecidableEq Candidate

Equations

• AlonsoOvalleMenendezBenito2010.instDecidableEqCandidate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlonsoOvalleMenendezBenito2010.instFintypeCandidate : Fintype Candidate

Equations

• One or more equations did not get rendered due to their size.

def AlonsoOvalleMenendezBenito2010.hires (w c : Candidate) : Prop

Equations

• AlonsoOvalleMenendezBenito2010.hires w c = (w = c)

@[instance_reducible]

instance AlonsoOvalleMenendezBenito2010.instDecidablePredCandidateHires (w : Candidate) : DecidablePred (hires w)

Equations

• AlonsoOvalleMenendezBenito2010.instDecidablePredCandidateHires w c = AlonsoOvalleMenendezBenito2010.instDecidablePredCandidateHires._aux_1 w c

def AlonsoOvalleMenendezBenito2010.permitted : SetRel Candidate Candidate

The permitted hires, from any world.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance AlonsoOvalleMenendezBenito2010.instDecidableMemProdCandidateSetRelPermittedMk (w c : Candidate) : Decidable ((w, c) ∈ permitted)

Equations

• AlonsoOvalleMenendezBenito2010.instDecidableMemProdCandidateSetRelPermittedMk w c = AlonsoOvalleMenendezBenito2010.instDecidableMemProdCandidateSetRelPermittedMk._aux_1 w c

theorem AlonsoOvalleMenendezBenito2010.hideAndSeek (w : Room) : Exhaustification.ModalVariation (epist pedro15) w house inRoom ∧ ¬Exhaustification.FreeChoice (epist pedro15) w house inRoom ∧ (∀ S ∈ Exhaustification.subdomainAlternatives Exhaustification.Subdomains.singletons house, ¬ModalLogic.Box (epist pedro15) (Exhaustification.claim inRoom S) w) ∧ (∀ S ∈ Exhaustification.subdomainAlternatives Exhaustification.Subdomains.singletons house, Exhaustification.AntiExhaustivity (epist pedro15) w house inRoom S) ∧ ¬Exhaustification.AntiExhaustivity (epist pedro15) w house inRoom {Room.bedroom, Room.livingRoom}

In (15) Modal Variation holds without Free Choice; the singleton competitors are all false (59b) and carry their anti-exhaustivity implicatures (68b), while the widening competitor bedroom or living room (72) does not.

The paper's verdicts

def AlonsoOvalleMenendezBenito2010.predicted (row : Datum) : Option Bool

A row's predicted verdict, where algún needs Modal Variation, cualquiera Free Choice, and un nothing.

Equations

• One or more equations did not get rendered due to their size.

def AlonsoOvalleMenendezBenito2010.predicted.verdictIn {E W : Type} [DecidableEq E] [DecidableEq W] [Fintype W] (R : SetRel W W) [(x y : W) → Decidable ((x, y) ∈ R)] (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] : String → Option Bool

Equations

• AlonsoOvalleMenendezBenito2010.predicted.verdictIn R D Q "algún" = some (decide (∀ (w : W), Exhaustification.ModalVariation R w D Q))
• AlonsoOvalleMenendezBenito2010.predicted.verdictIn R D Q "cualquiera" = some (decide (∀ (w : W), Exhaustification.FreeChoice R w D Q))
• AlonsoOvalleMenendezBenito2010.predicted.verdictIn R D Q "un" = some true
• AlonsoOvalleMenendezBenito2010.predicted.verdictIn R D Q a✝ = none

def AlonsoOvalleMenendezBenito2010.observed (row : Datum) : Bool

A row's observed verdict, which is fine unless the row is deviant or judged false.

Equations

• AlonsoOvalleMenendezBenito2010.observed row = (row.judgment == Judgment.acceptable && row.feature? "verdict" != some "false")

theorem AlonsoOvalleMenendezBenito2010.rows_agree (row : Datum) : row ∈ Examples.all → ∀ (b : Bool), predicted row = some b → observed row = b

Every row in a modelled scenario carries the predicted verdict.