Cooper (2023): From Perception to Communication: A Theory of Types for Action and Meaning

Cooper's theory of types with records reads a type as true when something witnesses it. A modal type system assigns objects to types in each of a family of possibilities, and subtyping is inclusion of witnesses in every possibility, so an attitude, which matches its complement against a type of the agent's information state, depends on which postulates restrict the possibilities. A witness for a quantified sentence is a witness set with a function into or out of it, following Barwise and Cooper's two procedures for monotone quantifiers, and the sets a witness carries are the anaphora sets the noun phrase makes available. Scope ambiguity comes from storing a quantifier in the context and retrieving it over the sentence, and binding from marking pronouns as local or reflexive.

Main statements

• Venus.not_believe_oneStar, Venus.believe_oneStar_reporter: the ancients do not believe that Hesperus is Phosphorus under their own postulates, and do under the reporter's.
• nonempty_generalWCIncr_iff_toGQ, nonempty_generalWCDecr_iff_toGQ: the general witness conditions are Barwise and Cooper's two procedures for the tree quantifier of their relation.
• witnessType_propAtLeast_iff: a probabilistic witness condition of §7.3 is its cardinal one.
• WitnessCondition.exists_set_subset: each witness condition can be met by a witness whose set lies in the anaphora set it makes available, which anaphora_rows checks against the book's judgements.

Implementation notes

• Within one possibility, types are Lean's own, and a property is E → Type. A modal type system assigns shared objects to types, so subtyping, and every attitude built on it, compares witnesses across possibilities. The postulates for transitive verbs are hypotheses on Lean types.
• A negated type ¬T (Ch. 7, (69)) is the function type T → Empty.
• Proportional thresholds are cross-multiplied n / d over a nonempty extension, and the thresholds θ_q(P) are parameters, shared by few and a few only where stated.
• Context labels are chosen distinct by hand rather than incremented at combination, and a stored quantifier keeps its foreground, its background merged at storage. Localisation folds the whole assignment into a property's domain, and alignment supplies the constant assignment at the antecedent's witness.

TODO

• The closure of a content type under the operations (Ch. 8, (21), (89)) and the combination of content types (23)–(24) are not modelled: each reading is derived by composing the operations by hand.
• The asymmetric merge ∧̣ of a type with a point of view (Ch. 6, (55)–(58)) is not defined: an information state lists which types are such merges.
• The number of a pronoun is not modelled, so the contrast between it and they with a universal antecedent, (46b)–(46e), is recorded in the rows but not derived.
• A reflexive inside a verb phrase (The guru revealed Kim to himself) and picture noun phrases are outside the treatment, as in the book.
• Purification is determiner-independent, so both donkey readings are predicted for every determiner; the experimental record of [DS22] on non-monotonic determiners and the question-based selection of [CBH19] are the tests to state.

References

• R. Cooper, From Perception to Communication (2023)
• J. Barwise, R. Cooper, Generalized Quantifiers and Natural Language (1981)
• J. van Benthem, Questions about Quantifiers (1984)
• L. M. Moxey, A. J. Sanford, Quantifiers and Focus (1987)
• A. Kratzer, What 'must' and 'can' must and can mean (1977)
• A. Kratzer, The Notional Category of Modality (1981)
• E. Breitholtz, Enthymemes and Topoi in Dialogue (2020)
• G. Chierchia, Dynamics of Meaning (1995)
• M. Kanazawa, Weak vs. Strong Readings of Donkey Sentences (1994)
• A. Ranta, Type-Theoretical Grammar (1994)
• R. Montague, The Proper Treatment of Quantification in Ordinary English (1973)
• M. Denić, Y. Sudo, Donkey Anaphora in Non-Monotonic Environments (2022)
• L. Champollion, D. Bumford, R. Henderson, Donkeys under Discussion (2019)

Properties, quantifiers and their contents (Chs. 3, 4)

@[reducible, inline]

abbrev Cooper2023.Ppty (E : Type) : Type 1

A property (30) gives each individual its type of situations.

Equations

• Cooper2023.Ppty E = (E → Type)

@[reducible, inline]

abbrev Cooper2023.Quant (E : Type) : Type 1

A quantifier maps properties to types, as Montague's ⟨⟨e,t⟩,t⟩ does.

Equations

• Cooper2023.Quant E = (Cooper2023.Ppty E → Type)

@[reducible, inline]

abbrev Cooper2023.Ppty.Witnessed {E : Type} (P : Ppty E) (a : E) : Prop

A property is witnessed at an individual of its property extension [↓P].

Equations

• P.Witnessed a = Nonempty (P a)

def Cooper2023.SemPropName {E : Type} (a : E) : Quant E

SemPropName(a) (33) applies a property to the individual a.

Equations

• Cooper2023.SemPropName a P = P a

structure Cooper2023.ParticularWCExist {E : Type} (P Q : Ppty E) : Type

The particular witness condition for exist(P, Q) (Ch. 7, (63)) provides an individual with the first property and the second. Its x-field is what singular anaphora picks up in A dog is barking. It is right outside my window (Ch. 7, (64)).

• x : E
• pWit : P self.x
• qWit : Q self.x

structure Cooper2023.ParticularWCNo {E : Type} (P Q : Ppty E) : Type

The particular witness condition for no(P, Q) (Ch. 7, (70)) shows that every witness of the first property precludes the second, by a function into the negated type (69).

• f (a : E) : P a → Q a → Empty

theorem Cooper2023.nonempty_particularWCExist_iff {E : Type} {P Q : Ppty E} : Nonempty (ParticularWCExist P Q) ↔ ∃ (a : E), Nonempty (P a) ∧ Nonempty (Q a)

exist(P, Q) is witnessed iff the property extensions of P and Q overlap, (55).

theorem Cooper2023.some_of_particularWCExist {E : Type} {P Q : Ppty E} (w : ParticularWCExist P Q) : Quantifier.GQ.some P.Witnessed Q.Witnessed

theorem Cooper2023.no_of_particularWCNo {E : Type} {P Q : Ppty E} (w : ParticularWCNo P Q) : Quantifier.GQ.no P.Witnessed Q.Witnessed

def Cooper2023.SemIndefArt {E : Type} (restr : Ppty E) : Quant E

SemIndefArt (37) sends a restrictor property to the existential quantifier over it, whose witness under the particular condition of Ch. 7 (63) is an individual with the restrictor and the scope.

Equations

• Cooper2023.SemIndefArt restr = Cooper2023.ParticularWCExist restr

def Cooper2023.SemBe {E : Type} (Q : Quant E) : Ppty E

SemBe (78), Montague's copula, is the property of being the quantifier's witness.

Equations

• Cooper2023.SemBe Q x = Q fun (y : E) => PLift (x = y)

def Cooper2023.SemUniversal {E : Type} (restr scope : Ppty E) : Type

The universal quantifier is a function from the restrictor's witnesses to the scope's, the function witness of §7.2.4 after [Ran94], which, as Cooper notes at (27), yields no witness set for plural anaphora; the set-based condition (72) is GeneralWCIncr with CardRel.every.

Equations

• Cooper2023.SemUniversal restr scope = ((x : E) → restr x → scope x)

def Cooper2023.SemNo {E : Type} (restr scope : Ppty E) : Type

no(P, Q) under its particular witness condition (Ch. 7, (70)) holds when every witness of the restrictor precludes the scope.

Equations

• Cooper2023.SemNo restr scope = Cooper2023.ParticularWCNo restr scope

theorem Cooper2023.nonempty_semBe_semIndefArt_iff {E : Type} (P : Ppty E) (a : E) : Nonempty (SemBe (SemIndefArt P) a) ↔ Nonempty (P a)

a is a P, the copula over the indefinite article, is witnessed iff P(a) is (92), so the compositional content and the construction-based content of (86)–(87) are distinct but equivalent types.

theorem Cooper2023.nonempty_semIndefArt_semBe_semPropName_iff {E : Type} (P : Ppty E) (a : E) : Nonempty (SemIndefArt P (SemBe (SemPropName a))) ↔ Nonempty (P a)

a P is a, with the quantifiers in the other order, is witnessed iff P(a) is as well (94c); only the construction expresses P(a) itself, and (89) A conductor is Dudamel is odd.

def Cooper2023.Quant.IsMonIncr {E : Type} (Q : Quant E) : Prop

A quantifier is monotone increasing when a witness for a property gives one for any larger property.

Equations

• Q.IsMonIncr = ∀ (P P' : Cooper2023.Ppty E) (a : (x : E) → P x → P' x), Nonempty (Q P) → Nonempty (Q P')

theorem Cooper2023.isMonIncr_semIndefArt {E : Type} (restr : Ppty E) : (SemIndefArt restr).IsMonIncr

structure Cooper2023.Parametric (C : Type u_1) : Type (max 1 u_1)

A parametric content (§4.3, (14)) pairs a background type, the context it requires, with a foreground function from contexts of that type to contents.

• bg : Type
• fg : self.bg → C

Dudamel is a conductor (82c)

inductive Cooper2023.Dudamel.Ind : Type

• dudamel : Ind
• beethoven : Ind

@[instance_reducible]

instance Cooper2023.Dudamel.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023.Dudamel.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cooper2023.Dudamel.instReprInd : Repr Ind

Equations

• Cooper2023.Dudamel.instReprInd = { reprPrec := Cooper2023.Dudamel.instReprInd.repr }

def Cooper2023.Dudamel.instReprInd.repr : Ind → ℕ → Std.Format

Equations

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

inductive Cooper2023.Dudamel.Conductor : Ind → Type

• mk : Conductor Ind.dudamel

def Cooper2023.Dudamel.IsAConductor : Ppty Ind

is a conductor (81c) is the copula over the indefinite article.

Equations

• Cooper2023.Dudamel.IsAConductor = Cooper2023.SemBe (Cooper2023.SemIndefArt Cooper2023.Dudamel.Conductor)

def Cooper2023.Dudamel.dudamelIsAConductor : SemPropName Ind.dudamel IsAConductor

Equations

• Cooper2023.Dudamel.dudamelIsAConductor = { x := Cooper2023.Dudamel.Ind.dudamel, pWit := Cooper2023.Dudamel.Conductor.mk, qWit := { down := ⋯ } }

theorem Cooper2023.Dudamel.beethovenIsAConductor_isEmpty : IsEmpty (SemPropName Ind.beethoven IsAConductor)

Modality and intensionality without possible worlds (Ch. 6)

A modal type system is a family of possibilities over shared types, and modality and the attitudes compare witnesses across its possibilities.

Modal type systems (§6.3)

structure Cooper2023.Possibility (Ty Obj : Type) : Type

A possibility says which types occur in it and which objects witness them. Only a type of the possibility has witnesses in it.

• occurs : Ty → Prop
• witnesses : Ty → Obj → Prop
• occurs_of_witnesses ⦃T : Ty⦄ ⦃a : Obj⦄ : self.witnesses T a → self.occurs T

@[reducible, inline]

abbrev Cooper2023.ModalSystem (M Ty Obj : Type) : Type

A modal system of types (§1.4.3.5, (54)) is a family of possibilities over shared types.

Equations

• Cooper2023.ModalSystem M Ty Obj = (M → Cooper2023.Possibility Ty Obj)

def Cooper2023.ModalSystem.extension {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T : Ty) (p : M) : Set Obj

The extension of T (1a) gives its witnesses in each possibility.

Equations

• ms.extension T p = {a : Obj | (ms p).witnesses T a}

def Cooper2023.ModalSystem.Occurs {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (p : M) (T : Ty) : Prop

T occurs in the type system of the possibility p.

Equations

• ms.Occurs p T = (ms p).occurs T

def Cooper2023.ModalSystem.SubtypeR {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T₁ T₂ : Ty) : Prop

T₁ is a restrictive subtype of T₂ (1b) when its extension is included in that of T₂ in every possibility.

Equations

• ms.SubtypeR T₁ T₂ = (ms.extension T₁ ≤ ms.extension T₂)

def Cooper2023.ModalSystem.EquivR {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T₁ T₂ : Ty) : Prop

T₁ and T₂ are restrictively equivalent (1a) when they have the same extension in every possibility.

Equations

• ms.EquivR T₁ T₂ = (ms.extension T₁ = ms.extension T₂)

def Cooper2023.ModalSystem.NecR {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T : Ty) : Prop

T is restrictively necessary (1c) when it is witnessed in every possibility.

Equations

• ms.NecR T = ∀ (p : M), (ms.extension T p).Nonempty

def Cooper2023.ModalSystem.PossR {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T : Ty) : Prop

T is restrictively possible (1d) when it is witnessed in some possibility.

Equations

• ms.PossR T = ∃ (p : M), (ms.extension T p).Nonempty

def Cooper2023.ModalSystem.SubtypeI {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T₁ T₂ : Ty) : Prop

T₁ is an inclusive subtype of T₂ (2b; Ch. 1, (55)) when its extension is included in that of T₂ wherever both types occur.

Equations

• ms.SubtypeI T₁ T₂ = ∀ (p : M), ms.Occurs p T₁ → ms.Occurs p T₂ → ms.extension T₁ p ⊆ ms.extension T₂ p

def Cooper2023.ModalSystem.EquivI {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T₁ T₂ : Ty) : Prop

T₁ and T₂ are inclusively equivalent (2a) when they have the same extension wherever both occur.

Equations

• ms.EquivI T₁ T₂ = ∀ (p : M), ms.Occurs p T₁ → ms.Occurs p T₂ → ms.extension T₁ p = ms.extension T₂ p

def Cooper2023.ModalSystem.NecI {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T : Ty) : Prop

T is inclusively necessary, by the rule (4c), when it occurs in some possibility and is witnessed wherever it occurs.

Equations

• ms.NecI T = ((∃ (p : M), ms.Occurs p T) ∧ ∀ (p : M), ms.Occurs p T → (ms.extension T p).Nonempty)

def Cooper2023.ModalSystem.PossI {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T : Ty) : Prop

T is inclusively possible, by the rule (4d), when it is witnessed in a possibility in which it occurs. The definition (2d) prints the conjunction as an implication.

Equations

• ms.PossI T = ∃ (p : M), ms.Occurs p T ∧ (ms.extension T p).Nonempty

theorem Cooper2023.ModalSystem.equivR_iff {M Ty Obj : Type} {ms : ModalSystem M Ty Obj} {T₁ T₂ : Ty} : ms.EquivR T₁ T₂ ↔ ms.SubtypeR T₁ T₂ ∧ ms.SubtypeR T₂ T₁

Restrictive equivalence is subtyping both ways (3b).

theorem Cooper2023.ModalSystem.equivI_iff {M Ty Obj : Type} {ms : ModalSystem M Ty Obj} {T₁ T₂ : Ty} : ms.EquivI T₁ T₂ ↔ ms.SubtypeI T₁ T₂ ∧ ms.SubtypeI T₂ T₁

Inclusive equivalence is subtyping both ways (4b).

theorem Cooper2023.ModalSystem.SubtypeR.trans {M Ty Obj : Type} {ms : ModalSystem M Ty Obj} {T₁ T₂ T₃ : Ty} (h : ms.SubtypeR T₁ T₂) (h' : ms.SubtypeR T₂ T₃) : ms.SubtypeR T₁ T₃

theorem Cooper2023.ModalSystem.SubtypeR.subtypeI {M Ty Obj : Type} {ms : ModalSystem M Ty Obj} {T₁ T₂ : Ty} (h : ms.SubtypeR T₁ T₂) : ms.SubtypeI T₁ T₂

theorem Cooper2023.ModalSystem.EquivR.equivI {M Ty Obj : Type} {ms : ModalSystem M Ty Obj} {T₁ T₂ : Ty} (h : ms.EquivR T₁ T₂) : ms.EquivI T₁ T₂

theorem Cooper2023.ModalSystem.NecR.necI {M Ty Obj : Type} {ms : ModalSystem M Ty Obj} {T : Ty} [Nonempty M] (h : ms.NecR T) : ms.NecI T

theorem Cooper2023.ModalSystem.PossR.possI {M Ty Obj : Type} {ms : ModalSystem M Ty Obj} {T : Ty} (h : ms.PossR T) : ms.PossI T

theorem Cooper2023.ModalSystem.SubtypeI.comp {M M' Ty Obj : Type} {ms : ModalSystem M Ty Obj} {T₁ T₂ : Ty} (h : ms.SubtypeI T₁ T₂) (ι : M' → M) : SubtypeI (ms ∘ ι) T₁ T₂

Subtyping in a modal system holds in any restriction of it, and restricting attention to some of the possibilities is what a postulate does (p. 261).

Restrictive against inclusive necessity

Snow is possible but not necessary, and once it does not occur in the second possibility it is inclusively but not restrictively necessary.

inductive Cooper2023.Weather.Ty : Type

• rain : Ty
• snow : Ty

@[instance_reducible]

instance Cooper2023.Weather.instDecidableEqTy : DecidableEq Ty

Equations

• Cooper2023.Weather.instDecidableEqTy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Cooper2023.Weather.Obj : Type

• a : Obj
• b : Obj

@[instance_reducible]

instance Cooper2023.Weather.instDecidableEqObj : DecidableEq Obj

Equations

• Cooper2023.Weather.instDecidableEqObj x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023.Weather.system : ModalSystem (Fin 2) Ty Obj

Both types occur in both possibilities; rain is witnessed in both, snow in the first.

Equations

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

def Cooper2023.Weather.restricted : ModalSystem (Fin 2) Ty Obj

As system, but snow does not occur in the second possibility.

Equations

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

theorem Cooper2023.Weather.necR_rain : system.NecR Ty.rain

theorem Cooper2023.Weather.possR_snow : system.PossR Ty.snow

theorem Cooper2023.Weather.not_necR_snow : ¬system.NecR Ty.snow

theorem Cooper2023.Weather.restricted_necI_snow : restricted.NecI Ty.snow

theorem Cooper2023.Weather.restricted_not_necR_snow : ¬restricted.NecR Ty.snow

Modality with topoi (§6.4)

The last version of nec and poss, (23)–(24), takes a topos in place of Kratzer's ideal.

@[reducible, inline]

abbrev Cooper2023.Topos : Type 1

A topos (20) is a dependent type from situations of a background type to types.

Equations

• Cooper2023.Topos = Cooper2023.Parametric Type

def Cooper2023.Compatible (T₁ T₂ : Type) : Prop

Two types are compatible (17) when something is of both.

Equations

• Cooper2023.Compatible T₁ T₂ = Nonempty (T₁ × T₂)

structure Cooper2023.Nec (T B : Type) (τ : Topos) : Type

A witness of nec(T, B, τ) (23) is a situation of the background type B, with B a subtype of the topos's domain and the type the topos returns for the situation a subtype of T.

• sit : B
• sub : B → τ.bg
• incl : τ.fg (self.sub self.sit) → T

structure Cooper2023.Poss (T B : Type) (τ : Topos) : Type

A witness of poss(T, B, τ) (24) is as for Nec, with the returned type compatible with T.

• sit : B
• sub : B → τ.bg
• compat : Compatible (τ.fg (self.sub self.sit)) T

def Cooper2023.Nec.toPoss {T B : Type} {τ : Topos} (h : Nec T B τ) (hne : Nonempty (τ.fg (h.sub h.sit))) : Poss T B τ

Necessity yields possibility when the topos returns an inhabited type.

Equations

• h.toPoss hne = { sit := h.sit, sub := h.sub, compat := ⋯ }

Mary should eat her broccoli (25)–(31)

Eating the broccoli is necessary under the deontic topos and under the bouletic one, (29).

inductive Cooper2023.Dinner.Ind : Type

• broccoli : Ind
• mary : Ind
• plate : Ind

@[instance_reducible]

instance Cooper2023.Dinner.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023.Dinner.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cooper2023.Dinner.instReprInd : Repr Ind

Equations

• Cooper2023.Dinner.instReprInd = { reprPrec := Cooper2023.Dinner.instReprInd.repr }

def Cooper2023.Dinner.instReprInd.repr : Ind → ℕ → Std.Format

Equations

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

inductive Cooper2023.Dinner.Broccoli : Ind → Type

• mk : Broccoli Ind.broccoli

inductive Cooper2023.Dinner.Child : Ind → Type

• mk : Child Ind.mary

inductive Cooper2023.Dinner.Plate : Ind → Type

• mk : Plate Ind.plate

inductive Cooper2023.Dinner.Have : Ind → Ind → Type

• mk : Have Ind.mary Ind.plate

inductive Cooper2023.Dinner.On : Ind → Ind → Type

• mk : On Ind.broccoli Ind.plate

inductive Cooper2023.Dinner.Love : Ind → Ind → Type

• mk : Love Ind.mary Ind.broccoli

inductive Cooper2023.Dinner.Eat : Ind → Ind → Type

• mk : Eat Ind.mary Ind.broccoli

inductive Cooper2023.Dinner.Food : Ind → Type

Food, of which broccoli is a subtype (27), is witnessed by broccoli.

• ofBroccoli {x : Ind} : Broccoli x → Food x

structure Cooper2023.Dinner.Base : Type

The base situation type (26) has its manifest fields fixed here by the ptypes' witnesses.

• x : Ind
• c₁ : Broccoli self.x
• y : Ind
• c₂ : Child self.y
• z : Ind
• c₃ : Plate self.z
• e₁ : Have self.y self.z
• e₂ : On self.x self.z
• e₃ : Love self.y self.x

structure Cooper2023.Dinner.OnPlate : Type

The background of the deontic topos (28a) is a child with food on her plate.

• x : Ind
• c₁ : Food self.x
• y : Ind
• c₂ : Child self.y
• z : Ind
• c₃ : Plate self.z
• e₁ : Have self.y self.z
• e₂ : On self.x self.z

structure Cooper2023.Dinner.Loves : Type

The background of the bouletic topos (28b) is a child loving some food.

• x : Ind
• c₁ : Food self.x
• y : Ind
• c₂ : Child self.y
• e₃ : Love self.y self.x

def Cooper2023.Dinner.deontic : Topos

The deontic topos τ₁ (28a) sends a child with food on her plate to her eating it.

Equations

• Cooper2023.Dinner.deontic = { bg := Cooper2023.Dinner.OnPlate, fg := fun (r : Cooper2023.Dinner.OnPlate) => Cooper2023.Dinner.Eat r.y r.x }

def Cooper2023.Dinner.bouletic : Topos

The bouletic topos τ₂ (28b) sends a child loving some food to her eating it.

Equations

• Cooper2023.Dinner.bouletic = { bg := Cooper2023.Dinner.Loves, fg := fun (r : Cooper2023.Dinner.Loves) => Cooper2023.Dinner.Eat r.y r.x }

def Cooper2023.Dinner.base : Base

The base situation has the broccoli on Mary's plate, and Mary loving it.

Equations

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

def Cooper2023.Dinner.necDeontic : Nec (Eat Ind.mary Ind.broccoli) Base deontic

Eating the broccoli is necessary under the deontic topos (29a), the base type being a subtype of the topos's domain by (27) and the topos returning the type itself (30).

Equations

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

def Cooper2023.Dinner.necBouletic : Nec (Eat Ind.mary Ind.broccoli) Base bouletic

Eating the broccoli is necessary under the bouletic topos as well (29b).

Equations

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

Intensionality (§6.5)

An attitude matches its complement against a type of the agent's information state up to relabelling, so whose postulates restrict the possibilities decides the report (pp. 261–262).

def Cooper2023.ModalSystem.SubtypeRelabel {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (r : Setoid Ty) (T₁ T₂ : Ty) : Prop

T₁ ⊑⇝ T₂ (39) holds when T₁ is a subtype, in the sense of Ch. 1 (55), of some relabelling of T₂, the relabellings of a type being its class under r.

Equations

• ms.SubtypeRelabel r T₁ T₂ = ∃ (T : Ty), r T₂ T ∧ ms.SubtypeI T₁ T

theorem Cooper2023.ModalSystem.subtypeRelabel_congr {M Ty Obj : Type} {ms : ModalSystem M Ty Obj} {r : Setoid Ty} {T₁ T₂ T₂' : Ty} (h : r T₂ T₂') : ms.SubtypeRelabel r T₁ T₂ ↔ ms.SubtypeRelabel r T₁ T₂'

Matching is blind to the relabelling of the complement (41).

theorem Cooper2023.ModalSystem.SubtypeRelabel.comp {M M' Ty Obj : Type} {ms : ModalSystem M Ty Obj} {r : Setoid Ty} {T₁ T₂ : Ty} (h : ms.SubtypeRelabel r T₁ T₂) (ι : M' → M) : SubtypeRelabel (ms ∘ ι) r T₁ T₂

structure Cooper2023.InfoState (Agent Ty : Type) : Type

An agent's total information state (91) gives the types of each agent's long-term memory, religious beliefs and desires, and records which types are merges of a type with a complete point of view on it (55).

• ltm : Agent → Ty
• rbel : Agent → Ty
• des : Agent → Ty
• pov : Ty → Ty → Prop

  pov M T says that M is the asymmetric merge T ∧̣ T' of T with a complete point of view T' on it.

inductive Cooper2023.InfoState.Matches {M Agent Ty Obj : Type} (s : InfoState Agent Ty) (ms : ModalSystem M Ty Obj) (r : Setoid Ty) (I : Ty) : Ty → Prop

s.Matches ms r I T is the least relation closed under the two conditionals of (58), by which the information type I matches T when I ⊑⇝ T, or when I matches some T₁ whose merge with a point of view on it is a subtype of T up to relabelling. Belief (58) matches the long-term memory, worship (81) the religious beliefs against the quantifier exported over worship†, and want† (92) the desires.

• subtype {M Agent Ty Obj : Type} {s : InfoState Agent Ty} {ms : ModalSystem M Ty Obj} {r : Setoid Ty} {I T : Ty} : ms.SubtypeRelabel r I T → s.Matches ms r I T
• pov {M Agent Ty Obj : Type} {s : InfoState Agent Ty} {ms : ModalSystem M Ty Obj} {r : Setoid Ty} {I T₁ M✝ T : Ty} : s.Matches ms r I T₁ → s.pov M✝ T₁ → ms.SubtypeRelabel r M✝ T → s.Matches ms r I T

theorem Cooper2023.InfoState.Matches.congr {M Agent Ty Obj : Type} {s : InfoState Agent Ty} {ms : ModalSystem M Ty Obj} {r : Setoid Ty} {I T T' : Ty} (h : s.Matches ms r I T) (hT : r T T') : s.Matches ms r I T'

An attitude toward a type is one toward any relabelling of it (41).

theorem Cooper2023.InfoState.Matches.comp {M M' Agent Ty Obj : Type} {s : InfoState Agent Ty} {ms : ModalSystem M Ty Obj} {r : Setoid Ty} {I T : Ty} (h : s.Matches ms r I T) (ι : M' → M) : s.Matches (ms ∘ ι) r I T

An attitude computed with fewer postulates holds with more, the postulates restricting the possibilities.

Hesperus and Phosphorus, (52)–(53)

The ancients cannot exclude a possibility in which Phosphorus is another body than Venus; the reporter can (p. 262).

inductive Cooper2023.Venus.Body : Type

• venus : Body
• mars : Body

inductive Cooper2023.Venus.Ty : Type

The types are (52), and (53b), which identifies the second body with the first.

• twoStars : Ty
• oneStar : Ty

inductive Cooper2023.Venus.Possib : Type

In the actual possibility Phosphorus is Venus; in the other, which the ancients cannot exclude, it is Mars.

• actual : Possib
• alternative : Possib

def Cooper2023.Venus.phosphorus : Possib → Body

Equations

• Cooper2023.Venus.phosphorus Cooper2023.Venus.Possib.actual = Cooper2023.Venus.Body.venus
• Cooper2023.Venus.phosphorus Cooper2023.Venus.Possib.alternative = Cooper2023.Venus.Body.mars

def Cooper2023.Venus.system : ModalSystem Possib Ty (Body × Body)

In the modal system Hesperus is Venus throughout, and the records are the pairs of their two bodies.

Equations

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

def Cooper2023.Venus.ancients : InfoState Unit Ty

Before learning, the ancients' information state has (52) as its long-term memory.

Equations

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

theorem Cooper2023.Venus.oneStar_subtypeR : system.SubtypeR Ty.oneStar Ty.twoStars

(53b) is a structural subtype of (52), having its fields and one more.

theorem Cooper2023.Venus.not_twoStars_subtypeI : ¬system.SubtypeI Ty.twoStars Ty.oneStar

theorem Cooper2023.Venus.believe_twoStars : ancients.Matches system ⊥ (ancients.ltm ()) Ty.twoStars

theorem Cooper2023.Venus.not_believe_oneStar : ¬ancients.Matches system ⊥ (ancients.ltm ()) Ty.oneStar

Under their own postulates the ancients do not believe that Hesperus is Phosphorus.

theorem Cooper2023.Venus.believe_oneStar_reporter : ancients.Matches (system ∘ fun (x : Unit) => Possib.actual) ⊥ (ancients.ltm ()) Ty.oneStar

Under the reporter's postulates, which exclude the alternative, they do.

theorem Cooper2023.Venus.learned_believe_twoStars : (have __src := ancients; { ltm := fun (x : Unit) => Ty.oneStar, rbel := __src.rbel, des := __src.des, pov := __src.pov }).Matches system ⊥ Ty.oneStar Ty.twoStars

Learning (53) keeps the belief in (52).

Intensional transitive verbs, (63)–(68), (87)

Following Montague a transitive verb's predicate takes a quantifier (64), and postulates make it extensional (65), a successful search a finding (66), and booking require existence (87).

structure Cooper2023.TransVerb (E : Type) : Type 1

A transitive verb has a predicate taking a quantifier (64) and a variant p† between individuals.

• pred : E → Quant E → Type
• dagger : E → E → Type

def Cooper2023.TransVerb.IsExtensional {E : Type} (v : TransVerb E) : Prop

A verb is extensional (65) when its ptype is equivalent to the quantifier exported over p†.

Equations

• v.IsExtensional = ∀ (a : E) (Q : Cooper2023.Quant E), Nonempty (v.pred a Q ≃ Q (v.dagger a))

theorem Cooper2023.TransVerb.IsExtensional.exists_of_semIndefArt {E : Type} {v : TransVerb E} (hv : v.IsExtensional) {a : E} {P : Ppty E} (h : Nonempty (v.pred a (SemIndefArt P))) : ∃ (x : E), Nonempty (P x) ∧ Nonempty (v.dagger a x)

With (65), a finds a P is witnessed only by a P that is found.

structure Cooper2023.SuccessfulSeek (E : Type) (seek find : E → Quant E → Type) : Type 1

A successful search is a finding (66).

• successful : Type → Type
• findOfSuccessful (a : E) (Q : Quant E) : self.successful (seek a Q) → find a Q

theorem Cooper2023.SuccessfulSeek.exists_of_successful {E : Type} {seek : E → Quant E → Type} {find : TransVerb E} (hs : SuccessfulSeek E seek find.pred) (hf : find.IsExtensional) {a : E} {P : Ppty E} (h : Nonempty (hs.successful (seek a (SemIndefArt P)))) : ∃ (x : E), Nonempty (P x) ∧ Nonempty (find.dagger a x)

With (66), and (65) for find, a successful search for a unicorn finds one, so there is one (p. 268).

def Cooper2023.BookRequiresBeing {E : Type} (book : E → Quant E → Type) (be : Ppty E) : Prop

Booking a monotone increasing quantifier's worth of tables requires tables to be, without requiring a specific one (87).

Equations

• Cooper2023.BookRequiresBeing book be = ∀ (a : E) (Q : Cooper2023.Quant E), Q.IsMonIncr → Nonempty (book a Q) → Nonempty (Q be)

theorem Cooper2023.exists_of_book {E : Type} {book : E → Quant E → Type} {be : Ppty E} (h : BookRequiresBeing book be) {a : E} {Table : Ppty E} (hb : Nonempty (book a (SemIndefArt Table))) : ∃ (x : E), Nonempty (Table x)

Under (87), Kim booked a table but there were no tables is inconsistent (68a).

Witness-based quantification (Ch. 7)

Purification lowers a property's restriction into its body, and a quantified ptype is witnessed by a witness set with a function into or out of it.

structure Cooper2023.Restricted (E : Type) : Type 1

A restricted property (7b) places conditions on the individual in its domain and returns a body.

• restr : E → Type
• body (x : E) : self.restr x → Type

def Cooper2023.Restricted.IsPure {E : Type} (P : Restricted E) : Prop

A property is pure (7a) when its restriction is trivial.

Equations

• P.IsPure = ∀ (x : E), Nonempty (Unique (P.restr x))

def Cooper2023.Purify {E : Type} (P : Restricted E) : Ppty E

Purification 𝔓(P) (12) lowers the restriction into the body under the local context.

Equations

• Cooper2023.Purify P x = ((c : P.restr x) × P.body x c)

def Cooper2023.PurifyUniv {E : Type} (P : Restricted E) : Ppty E

Universal purification 𝔓∀(P) (13) requires the body under every way of meeting the restriction.

Equations

• Cooper2023.PurifyUniv P x = ((c : P.restr x) → P.body x c)

def Cooper2023.Restricted.align {E : Type} (P : Restricted E) (R : E → Type) (f : (x : E) → R x → P.restr x) : Restricted E

Aligning two paths in the domain by a manifest field (Ch. 8, (51)–(52)) is a further restriction of the domain, through which the body is read.

Equations

• P.align R f = { restr := R, body := fun (x : E) (c : R x) => P.body x (f x c) }

def Cooper2023.Restricted.restrictBy {E : Type} (P : Restricted E) (R : Ppty E) : Restricted E

Property restriction P|ℱ (Ch. 5, (98)) narrows the domain by a property, aligning along the projection.

Equations

• P.restrictBy R = P.align (fun (x : E) => R x × P.restr x) fun (x : E) => Prod.snd

theorem Cooper2023.nonempty_purify_iff {E : Type} (P : Restricted E) (x : E) : Nonempty (Purify P x) ↔ ∃ (c : P.restr x), Nonempty (P.body x c)

theorem Cooper2023.nonempty_purifyUniv_iff {E : Type} (P : Restricted E) (x : E) : Nonempty (PurifyUniv P x) ↔ ∀ (c : P.restr x), Nonempty (P.body x c)

theorem Cooper2023.Restricted.IsPure.nonempty_purify_iff_nonempty_purifyUniv {E : Type} {P : Restricted E} (h : P.IsPure) (x : E) : Nonempty (Purify P x) ↔ Nonempty (PurifyUniv P x)

For a pure property the two purifications agree, so 𝔓 and 𝔓∀ differ only under a non-trivial restriction.

Types of witness sets (§7.2.4)

A witness set of qʷ(P) is a subset of [↓P] whose cardinality stands in a relation to |[↓P]|, read on van Benthem's tree of numbers as Cooper reads determiners (p. 298).

@[reducible, inline]

abbrev Cooper2023.CardRel : Type

The cardinality clause of a type of witness sets is a relation between |X| and |[↓P]|.

Equations

• Cooper2023.CardRel = (ℕ → ℕ → Prop)

def Cooper2023.CardRel.exist : CardRel

existʷ (21) requires a singleton. Cooper notes the departure from [BC81], whose witness sets for a have at least one member.

Equations

• Cooper2023.CardRel.exist x x✝ = (x = 1)

def Cooper2023.CardRel.existPl : CardRel

exist_plʷ (22), plural some, requires at least two.

Equations

• Cooper2023.CardRel.existPl x x✝ = (2 ≤ x)

def Cooper2023.CardRel.no : CardRel

noʷ (23)–(24) requires the empty set.

Equations

• Cooper2023.CardRel.no x x✝ = (x = 0)

def Cooper2023.CardRel.every : CardRel

everyʷ (25)–(26) requires the whole extension.

Equations

• Cooper2023.CardRel.every x p = (x = p)

def Cooper2023.CardRel.atLeast (θ : ℕ) : CardRel

many_aʷ (30) requires at least θ, as does a_few_aʷ (34) at the threshold of few_aʷ.

Equations

• Cooper2023.CardRel.atLeast θ x x✝ = (θ ≤ x)

def Cooper2023.CardRel.atMost (θ : ℕ) : CardRel

few_aʷ (32) requires at most θ.

Equations

• Cooper2023.CardRel.atMost θ x x✝ = (x ≤ θ)

def Cooper2023.CardRel.propAtLeast (n d : ℕ) : CardRel

mostʷ (29), many_pʷ (31) and, at the threshold of few_pʷ, a_few_pʷ (35) require at least the proportion n / d of a nonempty extension, cross-multiplied.

Equations

• Cooper2023.CardRel.propAtLeast n d x p = (0 < p ∧ n * p ≤ d * x)

def Cooper2023.CardRel.propAtMost (n d : ℕ) : CardRel

few_pʷ (33) requires at most the proportion n / d of a nonempty extension.

Equations

• Cooper2023.CardRel.propAtMost n d x p = (0 < p ∧ d * x ≤ n * p)

def Cooper2023.CardRel.compAtMost (θ : ℕ) : CardRel

The complement witness sets of few_a (81b) hold all but at most θ of the extension.

Equations

• Cooper2023.CardRel.compAtMost θ x p = (p - θ ≤ x)

def Cooper2023.CardRel.compPropAtMost (n d : ℕ) : CardRel

The complement witness sets of few_p (82b) hold at least the proportion 1 - n / d of a nonempty extension.

Equations

• Cooper2023.CardRel.compPropAtMost n d x p = (0 < p ∧ (d - n) * p ≤ d * x)

theorem Cooper2023.CardRel.monotone_existPl (p : ℕ) : Monotone fun (x : ℕ) => existPl x p

theorem Cooper2023.CardRel.monotone_atLeast (θ p : ℕ) : Monotone fun (x : ℕ) => atLeast θ x p

theorem Cooper2023.CardRel.antitone_atMost (θ p : ℕ) : Antitone fun (x : ℕ) => atMost θ x p

theorem Cooper2023.CardRel.monotone_propAtLeast (n d p : ℕ) : Monotone fun (x : ℕ) => propAtLeast n d x p

theorem Cooper2023.CardRel.antitone_propAtMost (n d p : ℕ) : Antitone fun (x : ℕ) => propAtMost n d x p

theorem Cooper2023.CardRel.monotone_compAtMost (θ p : ℕ) : Monotone fun (x : ℕ) => compAtMost θ x p

theorem Cooper2023.CardRel.monotone_compPropAtMost (n d p : ℕ) : Monotone fun (x : ℕ) => compPropAtMost n d x p

theorem Cooper2023.CardRel.ofSizes_no : Quantifier.NumberTree.ofSizes no = Quantifier.NumberTree.no

theorem Cooper2023.CardRel.ofSizes_every : Quantifier.NumberTree.ofSizes every = Quantifier.NumberTree.all

theorem Cooper2023.CardRel.ofSizes_atLeast (θ : ℕ) : Quantifier.NumberTree.ofSizes (atLeast θ) = Quantifier.NumberTree.atLeast θ

theorem Cooper2023.CardRel.ofSizes_atMost (θ : ℕ) : Quantifier.NumberTree.ofSizes (atMost θ) = Quantifier.NumberTree.atMost θ

theorem Cooper2023.CardRel.innerNeg_ofSizes_compAtMost (θ : ℕ) : (Quantifier.NumberTree.ofSizes (compAtMost θ)).innerNeg = Quantifier.NumberTree.ofSizes (atMost θ)

The complement witness sets of few_a (81b), read on the tree of numbers, are the inner negation of few_aʷ.

theorem Cooper2023.CardRel.innerNeg_ofSizes_compPropAtMost (n d : ℕ) : (Quantifier.NumberTree.ofSizes (compPropAtMost n d)).innerNeg = Quantifier.NumberTree.ofSizes (propAtMost n d)

The complement witness sets of few_p (82b), read on the tree of numbers, are the inner negation of few_pʷ.

def Cooper2023.WitnessType {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (c : CardRel) (X : Finset E) : Prop

The type qʷ(P) of witness sets (20)–(35) holds the subsets of the extension [↓P] whose cardinality stands in the relation c to the extension's.

Equations

• Cooper2023.WitnessType P c X = (X ⊆ {x : E | P x} ∧ c X.card {x : E | P x}.card)

theorem Cooper2023.witnessType_iff_witness {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {X : Finset E} : WitnessType P c X ↔ Quantifier.NP.Witness ((Quantifier.NumberTree.ofSizes c).toGQ P) P fun (x : E) => x ∈ X

A witness set of qʷ(P) is a witness set over P, in the sense of [BC81] (20a), of the tree quantifier of qʷ's relation.

theorem Cooper2023.everyW_iff_witness {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {X : Finset E} : WitnessType P CardRel.every X ↔ Quantifier.NP.Witness (Quantifier.GQ.every P) P fun (x : E) => x ∈ X

theorem Cooper2023.noW_iff_witness {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {X : Finset E} : WitnessType P CardRel.no X ↔ Quantifier.NP.Witness (Quantifier.GQ.no P) P fun (x : E) => x ∈ X

theorem Cooper2023.existW_iff_minimal_witness {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {X : Finset E} [DecidableEq E] : WitnessType P CardRel.exist X ↔ Minimal (fun (Y : Finset E) => Quantifier.NP.Witness (Quantifier.GQ.some P) P fun (x : E) => x ∈ Y) X

Cooper's singleton witness sets for exist (21) are the minimal B&C witness sets of some P.

theorem Cooper2023.WitnessType.compAtMost_sdiff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {X : Finset E} [DecidableEq E] {θ : ℕ} (h : WitnessType P (CardRel.atMost θ) X) : WitnessType P (CardRel.compAtMost θ) ({x : E | P x} \ X)

The complement in [↓P] of a witness set of few_aʷ(P) is a complement witness set (81b).

Witness sets and probabilities (§7.3)

The probability (36) of a witness set within [↓P] is |X| / |[↓P]|, (51)–(52), so each probabilistic witness condition (41)–(58) is its cardinal one.

theorem Cooper2023.uniformOn_of_subset {E : Type} [MeasurableSpace E] [MeasurableSingletonClass E] {X P : Finset E} (h : X ⊆ P) : (ProbabilityTheory.uniformOn ↑P) ↑X = ↑X.card / ↑P.card

The probability of a witness set given the property is the proportion of the extension it takes, (51)–(52).

theorem Cooper2023.uniformOn_eq_zero_iff_of_subset {E : Type} [MeasurableSpace E] [MeasurableSingletonClass E] {X P : Finset E} (h : X ⊆ P) : (ProbabilityTheory.uniformOn ↑P) ↑X = 0 ↔ X = ∅

The probability is 0 exactly for the empty witness set (43).

theorem Cooper2023.uniformOn_eq_inv_iff_of_subset {E : Type} [MeasurableSpace E] [MeasurableSingletonClass E] {X P : Finset E} (h : X ⊆ P) (hP : P.Nonempty) : (ProbabilityTheory.uniformOn ↑P) ↑X = (↑P.card)⁻¹ ↔ X.card = 1

The probability is 1 / |[↓P]| exactly for a singleton witness set (41).

theorem Cooper2023.uniformOn_eq_one_iff_of_subset {E : Type} [MeasurableSpace E] [MeasurableSingletonClass E] {X P : Finset E} (h : X ⊆ P) (hP : P.Nonempty) : (ProbabilityTheory.uniformOn ↑P) ↑X = 1 ↔ X = P

The probability is 1 exactly for the whole extension (44).

theorem Cooper2023.witnessType_propAtLeast_iff {E : Type} [MeasurableSpace E] [MeasurableSingletonClass E] {X : Finset E} [Fintype E] {P : E → Prop} [DecidablePred P] {n d : ℕ} (hd : 0 < d) (hX : X ⊆ {x : E | P x}) (hP : 0 < {x : E | P x}.card) : WitnessType P (CardRel.propAtLeast n d) X ↔ ↑n / ↑d ≤ (ProbabilityTheory.uniformOn ↑{x : E | P x}) ↑X

The probabilistic witness condition for most (50) is the cardinal one (29).

@[reducible, inline]

abbrev Cooper2023.ExperienceBase (E Ty : Type) : Type

An experience base (37) holds the judgements [sit = a, type = T] an agent remembers.

Equations

• Cooper2023.ExperienceBase E Ty = Finset (E × Ty)

def Cooper2023.ExperienceBase.extension {E Ty : Type} [DecidableEq E] [DecidableEq Ty] (𝔍 : ExperienceBase E Ty) (T : Ty) : Finset E

The extension of a type with respect to the experience base (38) holds the situations judged of it. The estimate p_𝔍(T₁ ‖ T₂) (39) is the uniform measure on the extension of T₂ at that of T₁, the extension of T₁ ∧ T₂ being the intersection (37b).

Equations

• 𝔍.extension T = Finset.image Prod.fst ({x ∈ 𝔍 | x.2 = T})

Witness conditions for quantificational ptypes (§7.4)

The general conditions (59) are Barwise and Cooper's two procedures for monotone quantifiers (p. 298), so by their C11 each holds when the tree quantifier of qʷ does.

structure Cooper2023.GeneralWCIncr {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (c : CardRel) (Q : Ppty E) : Type

The general witness condition for monotone increasing quantifiers (59a) provides a witness set and a function from its members into the scope.

• X : Finset E
• witness : WitnessType P c self.X
• f (a : E) : a ∈ self.X → Q a

structure Cooper2023.GeneralWCDecr {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (c : CardRel) (Q : Ppty E) : Type

The general witness condition for monotone decreasing quantifiers (59b) provides a witness set and a function into it from the objects with both properties.

• X : Finset E
• witness : WitnessType P c self.X
• f (a : E) : P a → Q.Witnessed a → a ∈ self.X

@[reducible, inline]

abbrev Cooper2023.ParticularWCNeg {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (c : CardRel) (Q : Ppty E) : Type

The particular witness conditions for no over everyʷ(P) (70) and for few over its complement witness sets (85)–(86) provide a witness set of qʷ(P) whose members each preclude the scope, the negated type (69) being a function into Empty.

Equations

• Cooper2023.ParticularWCNeg P c Q = Cooper2023.GeneralWCIncr P c fun (a : E) => Q a → Empty

def Cooper2023.GeneralWCIncr.mapScope {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q Q' : Ppty E} (g : (a : E) → Q a → Q' a) (w : GeneralWCIncr P c Q) : GeneralWCIncr P c Q'

A witness for a scope is one for any larger scope, so (59a) is increasing in the scope.

Equations

• Cooper2023.GeneralWCIncr.mapScope g w = { X := w.X, witness := ⋯, f := fun (a : E) (ha : a ∈ w.X) => g a (w.f a ha) }

def Cooper2023.GeneralWCDecr.comapScope {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q Q' : Ppty E} (g : (a : E) → Q' a → Q a) (w : GeneralWCDecr P c Q) : GeneralWCDecr P c Q'

A witness for a scope is one for any smaller scope, so (59b) is decreasing in the scope.

Equations

• Cooper2023.GeneralWCDecr.comapScope g w = { X := w.X, witness := ⋯, f := ⋯ }

theorem Cooper2023.nonempty_generalWCIncr_iff_toGQ {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (hc : ∀ (p : ℕ), Monotone fun (x : ℕ) => c x p) : Nonempty (GeneralWCIncr P c Q) ↔ (Quantifier.NumberTree.ofSizes c).toGQ P Q.Witnessed

For a relation closed upwards in |X|, (59a) is witnessed exactly when the tree quantifier holds of P and Q, by Barwise and Cooper's C11(i).

theorem Cooper2023.nonempty_generalWCDecr_iff_toGQ {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (hc : ∀ (p : ℕ), Antitone fun (x : ℕ) => c x p) : Nonempty (GeneralWCDecr P c Q) ↔ (Quantifier.NumberTree.ofSizes c).toGQ P Q.Witnessed

For a relation closed downwards in |X|, (59b) is witnessed exactly when the tree quantifier holds of P and Q, by C11(ii).

theorem Cooper2023.GeneralWCIncr.X_subset {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (w : GeneralWCIncr P c Q) : w.X ⊆ {x : E | P x ∧ Q.Witnessed x}

theorem Cooper2023.ParticularWCNeg.X_subset {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (w : ParticularWCNeg P c Q) : w.X ⊆ {x : E | P x ∧ ¬Q.Witnessed x}

theorem Cooper2023.GeneralWCDecr.subset_X {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (w : GeneralWCDecr P c Q) : {x : E | P x ∧ Q.Witnessed x} ⊆ w.X

theorem Cooper2023.GeneralWCDecr.exists_X_eq {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (hc : ∀ (p : ℕ), Antitone fun (x : ℕ) => c x p) (w : GeneralWCDecr P c Q) : ∃ (w' : GeneralWCDecr P c Q), w'.X = {x : E | P x ∧ Q.Witnessed x}

Under (59b) with a relation closed downwards, a witness can be traded for one whose witness set is exactly the objects with both properties, which is the sense in which the general condition for few makes REFSET anaphora available (p. 315).

theorem Cooper2023.nonempty_generalWCIncr_every_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} : Nonempty (GeneralWCIncr P CardRel.every Q) ↔ Quantifier.GQ.every P Q.Witnessed

everyʷ is not closed upwards, but a witness set within [↓P] of its cardinality is all of it, which gives the truth condition of (72).

theorem Cooper2023.nonempty_generalWCIncr_exist_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} [DecidableEq E] : Nonempty (GeneralWCIncr P CardRel.exist Q) ↔ Quantifier.GQ.some P Q.Witnessed

A singleton set of an object with P all of whose members have Q exists just in case an object has both (62), so the truth condition of (60) is some.

theorem Cooper2023.nonempty_generalWCIncr_atLeast_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} {θ : ℕ} : Nonempty (GeneralWCIncr P (CardRel.atLeast θ) Q) ↔ Quantifier.GQ.atLeast θ P Q.Witnessed

many_a (77) and a_few_a (89) are the counting quantifier at least θ.

theorem Cooper2023.nonempty_generalWCDecr_atMost_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} {θ : ℕ} : Nonempty (GeneralWCDecr P (CardRel.atMost θ) Q) ↔ Quantifier.GQ.atMost θ P Q.Witnessed

few_a (79) is at most θ.

theorem Cooper2023.nonempty_generalWCIncr_propAtLeast_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} {n d : ℕ} : Nonempty (GeneralWCIncr P (CardRel.propAtLeast n d) Q) ↔ 0 < {x : E | P x}.ncard ∧ (Quantifier.NumberTree.threshold n d).toGQ P Q.Witnessed

most (74), many_p (78) and a_few_p (90) are the proportional threshold quantifier over a nonempty restrictor.

theorem Cooper2023.few_and_aFew_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} {θ : ℕ} : Nonempty (GeneralWCDecr P (CardRel.atMost θ) Q) ∧ Nonempty (GeneralWCIncr P (CardRel.atLeast θ) Q) ↔ Quantifier.GQ.exactly θ P Q.Witnessed

With the threshold few and a few share (34), few_a and a_few_a together are exactly θ.

theorem Cooper2023.nonempty_particularWCNeg_iff_toGQ {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (hc : ∀ (p : ℕ), Monotone fun (x : ℕ) => c x p) : Nonempty (ParticularWCNeg P c Q) ↔ (Quantifier.NumberTree.ofSizes c).innerNeg.toGQ P Q.Witnessed

theorem Cooper2023.nonempty_particularWCNeg_compAtMost_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} {θ : ℕ} : Nonempty (ParticularWCNeg P (CardRel.compAtMost θ) Q) ↔ Nonempty (GeneralWCDecr P (CardRel.atMost θ) Q)

The particular condition for few_a (85) is witnessed iff the general one (79) is, its complement witness sets being the inner negation of few_aʷ.

theorem Cooper2023.nonempty_particularWCNeg_compPropAtMost_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} {n d : ℕ} : Nonempty (ParticularWCNeg P (CardRel.compPropAtMost n d) Q) ↔ Nonempty (GeneralWCDecr P (CardRel.propAtMost n d) Q)

The particular condition for few_p (86) is witnessed iff the general one (80) is.

theorem Cooper2023.nonempty_particularWCNeg_every_iff {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} : Nonempty (ParticularWCNeg P CardRel.every Q) ↔ Nonempty (ParticularWCNo (fun (a : E) => PLift (P a)) Q)

The set-based no, the witness set of every object with P each precluding Q, is witnessed iff the particular condition (70) is.

def Cooper2023.ParticularWCExist.toGeneralWCIncr {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q : Ppty E} [DecidableEq E] {R : Ppty E} (w : ParticularWCExist R Q) (h : ∀ (a : E) (a_1 : R a), P a) : GeneralWCIncr P CardRel.exist Q

The particular condition for exist (63) gives the general one (60), with the singleton of its individual.

Equations

• w.toGeneralWCIncr h = { X := {w.x}, witness := ⋯, f := fun (x : E) (ha : x ∈ {w.x}) => ⋯ ▸ w.qWit }

def Cooper2023.ParticularWCNo.toGeneralWCDecr {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {Q R : Ppty E} (w : ParticularWCNo R Q) (h : (a : E) → P a → R a) : GeneralWCDecr P CardRel.no Q

The particular condition for no (70) gives the general one (67), with the empty witness set.

Equations

• w.toGeneralWCDecr h = { X := ∅, witness := ⋯, f := ⋯ }

Anaphora sets (§7.4.1)

REFSET, MAXSET and COMPSET ([MS87], p. 313) are read off the sets the witnesses carry, MAXSET being the content's restr path.

inductive Cooper2023.AnaphoraRef : Type

REFSET, MAXSET and COMPSET are the anaphora sets a quantified noun phrase can make available.

• refset : AnaphoraRef

  REFSET is the witness individual or set, as in A dog barked. It heard an intruder. (103d).

• maxset : AnaphoraRef

  MAXSET is the full extension, as in A dog barked. They do when they notice an intruder. (103a).

• compset : AnaphoraRef

  COMPSET is the complement witness set, as in Few dogs barked. They did not hear the intruder. (113d).

@[instance_reducible]

instance Cooper2023.instDecidableEqAnaphoraRef : DecidableEq AnaphoraRef

Equations

• Cooper2023.instDecidableEqAnaphoraRef x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023.instReprAnaphoraRef.repr : AnaphoraRef → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cooper2023.instReprAnaphoraRef : Repr AnaphoraRef

Equations

• Cooper2023.instReprAnaphoraRef = { reprPrec := Cooper2023.instReprAnaphoraRef.repr }

noncomputable def Cooper2023.AnaphoraRef.set {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (Q : Ppty E) : AnaphoraRef → Finset E

ref.set P Q is the set each anaphora-set kind names over the properties P and Q.

Equations

• Cooper2023.AnaphoraRef.set P Q Cooper2023.AnaphoraRef.refset = {x : E | P x ∧ Q.Witnessed x}
• Cooper2023.AnaphoraRef.set P Q Cooper2023.AnaphoraRef.maxset = {x : E | P x}
• Cooper2023.AnaphoraRef.set P Q Cooper2023.AnaphoraRef.compset = {x : E | P x ∧ ¬Q.Witnessed x}

theorem Cooper2023.AnaphoraRef.disjoint_set_refset_compset {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (Q : Ppty E) : Disjoint (set P Q refset) (set P Q compset)

REFSET and COMPSET are disjoint, so a nonempty witness set within the one is not within the other, and no witness of (59a) supplies COMPSET, as (76) and (92) show for most and a few.

inductive Cooper2023.WitnessCondition : Type

The witness conditions of §7.4 are told apart by the paths their witnesses provide.

• generalIncr : WitnessCondition

  The general condition (59a) provides a witness set and a function from it into the scope.

• generalDecr : WitnessCondition

  The general condition (59b) provides a witness set and a function into it from the objects with both properties.

• particularExist : WitnessCondition

  The particular condition for exist (63) provides an individual with both properties.

• particularNo : WitnessCondition

  The particular condition for no (70) provides the set of all objects with the first property, each precluding the scope.

• particularFewComp : WitnessCondition

  The particular conditions for few (85)–(86) provide a complement witness set, each member precluding the scope.

@[instance_reducible]

instance Cooper2023.instDecidableEqWitnessCondition : DecidableEq WitnessCondition

Equations

• Cooper2023.instDecidableEqWitnessCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023.instReprWitnessCondition.repr : WitnessCondition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Cooper2023.instReprWitnessCondition : Repr WitnessCondition

Equations

• Cooper2023.instReprWitnessCondition = { reprPrec := Cooper2023.instReprWitnessCondition.repr }

def Cooper2023.WitnessCondition.Witness {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (c : CardRel) (Q : Ppty E) : WitnessCondition → Type

wc.Witness P c Q is the type of witnesses of each condition over a restrictor P, a cardinality relation c and a scope Q, the condition for no (70) fixing everyʷ.

Equations

• Cooper2023.WitnessCondition.Witness P c Q Cooper2023.WitnessCondition.generalIncr = Cooper2023.GeneralWCIncr P c Q
• Cooper2023.WitnessCondition.Witness P c Q Cooper2023.WitnessCondition.generalDecr = Cooper2023.GeneralWCDecr P c Q
• Cooper2023.WitnessCondition.Witness P c Q Cooper2023.WitnessCondition.particularExist = Cooper2023.ParticularWCExist (fun (a : E) => PLift (P a)) Q
• Cooper2023.WitnessCondition.Witness P c Q Cooper2023.WitnessCondition.particularNo = Cooper2023.ParticularWCNeg P Cooper2023.CardRel.every Q
• Cooper2023.WitnessCondition.Witness P c Q Cooper2023.WitnessCondition.particularFewComp = Cooper2023.ParticularWCNeg P c Q

def Cooper2023.WitnessCondition.set {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (wc : WitnessCondition) : Witness P c Q wc → Finset E

A witness carries its witness set, or the singleton of its individual.

Equations

• Cooper2023.WitnessCondition.generalIncr.set w = w.X
• Cooper2023.WitnessCondition.generalDecr.set w = w.X
• Cooper2023.WitnessCondition.particularExist.set w = {w.x}
• Cooper2023.WitnessCondition.particularNo.set w = w.X
• Cooper2023.WitnessCondition.particularFewComp.set w = w.X

def Cooper2023.WitnessCondition.anaphora : WitnessCondition → AnaphoraRef

wc.anaphora is the anaphora set a condition's witness provides beyond the content's restr field.

Equations

• Cooper2023.WitnessCondition.generalIncr.anaphora = Cooper2023.AnaphoraRef.refset
• Cooper2023.WitnessCondition.generalDecr.anaphora = Cooper2023.AnaphoraRef.refset
• Cooper2023.WitnessCondition.particularExist.anaphora = Cooper2023.AnaphoraRef.refset
• Cooper2023.WitnessCondition.particularNo.anaphora = Cooper2023.AnaphoraRef.compset
• Cooper2023.WitnessCondition.particularFewComp.anaphora = Cooper2023.AnaphoraRef.compset

theorem Cooper2023.WitnessCondition.exists_set_subset {E : Type} [Fintype E] {P : E → Prop} [DecidablePred P] {c : CardRel} {Q : Ppty E} (wc : WitnessCondition) (hc : wc = generalDecr → ∀ (p : ℕ), Antitone fun (x : ℕ) => c x p) (w : Witness P c Q wc) : ∃ (w' : Witness P c Q wc), wc.set w' ⊆ AnaphoraRef.set P Q wc.anaphora

Every witnessed condition has a witness whose set lies in the condition's anaphora set, for (59b) under a relation closed downwards, so the anaphora set is read off the witnesses.

inductive Cooper2023.QuantName : Type

The English fragment names eight quantifier relations.

• exist : QuantName
• existPl : QuantName
• no : QuantName
• every : QuantName
• most : QuantName
• many : QuantName
• few : QuantName
• aFew : QuantName

@[instance_reducible]

instance Cooper2023.instDecidableEqQuantName : DecidableEq QuantName

Equations

• Cooper2023.instDecidableEqQuantName x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cooper2023.instReprQuantName : Repr QuantName

Equations

• Cooper2023.instReprQuantName = { reprPrec := Cooper2023.instReprQuantName.repr }

def Cooper2023.instReprQuantName.repr : QuantName → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cooper2023.instReprQuantName.repr Cooper2023.QuantName.no prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.QuantName.no")).group prec✝
• Cooper2023.instReprQuantName.repr Cooper2023.QuantName.most prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.QuantName.most")).group prec✝
• Cooper2023.instReprQuantName.repr Cooper2023.QuantName.many prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.QuantName.many")).group prec✝
• Cooper2023.instReprQuantName.repr Cooper2023.QuantName.few prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.QuantName.few")).group prec✝
• Cooper2023.instReprQuantName.repr Cooper2023.QuantName.aFew prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.QuantName.aFew")).group prec✝

def Cooper2023.QuantName.conditions : QuantName → List WitnessCondition

§7.4 assigns each quantifier relation its witness conditions, the particular ones for exist (63) and no (70), the general one elsewhere, and for few the general (79)–(80) and the particular (85)–(86) as alternatives.

Equations

• Cooper2023.QuantName.exist.conditions = [Cooper2023.WitnessCondition.particularExist]
• Cooper2023.QuantName.existPl.conditions = [Cooper2023.WitnessCondition.generalIncr]
• Cooper2023.QuantName.every.conditions = [Cooper2023.WitnessCondition.generalIncr]
• Cooper2023.QuantName.most.conditions = [Cooper2023.WitnessCondition.generalIncr]
• Cooper2023.QuantName.many.conditions = [Cooper2023.WitnessCondition.generalIncr]
• Cooper2023.QuantName.aFew.conditions = [Cooper2023.WitnessCondition.generalIncr]
• Cooper2023.QuantName.no.conditions = [Cooper2023.WitnessCondition.particularNo]
• Cooper2023.QuantName.few.conditions = [Cooper2023.WitnessCondition.generalDecr, Cooper2023.WitnessCondition.particularFewComp]

def Cooper2023.anaphoraAvailable (q : QuantName) : List AnaphoraRef

A quantified noun phrase makes available MAXSET, from the content's restr field, and the set of each of its witness conditions.

Equations

• Cooper2023.anaphoraAvailable q = Cooper2023.AnaphoraRef.maxset :: List.map Cooper2023.WitnessCondition.anaphora q.conditions

The dogs fragment

Three dogs, two of them barking, witness a dog barks (63), most dogs bark (74) and few dogs barked (87), and refute no dog barks.

inductive Cooper2023.Dogs.Ind : Type

• fido : Ind
• rex : Ind
• spot : Ind
• luna : Ind

@[instance_reducible]

instance Cooper2023.Dogs.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023.Dogs.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cooper2023.Dogs.instReprInd : Repr Ind

Equations

• Cooper2023.Dogs.instReprInd = { reprPrec := Cooper2023.Dogs.instReprInd.repr }

def Cooper2023.Dogs.instReprInd.repr : Ind → ℕ → Std.Format

Equations

• Cooper2023.Dogs.instReprInd.repr Cooper2023.Dogs.Ind.fido prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.Dogs.Ind.fido")).group prec✝
• Cooper2023.Dogs.instReprInd.repr Cooper2023.Dogs.Ind.rex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.Dogs.Ind.rex")).group prec✝
• Cooper2023.Dogs.instReprInd.repr Cooper2023.Dogs.Ind.spot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.Dogs.Ind.spot")).group prec✝
• Cooper2023.Dogs.instReprInd.repr Cooper2023.Dogs.Ind.luna prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.Dogs.Ind.luna")).group prec✝

@[instance_reducible]

instance Cooper2023.Dogs.instFintypeInd : Fintype Ind

Equations

• Cooper2023.Dogs.instFintypeInd = { elems := { val := ↑Cooper2023.Dogs.Ind.enumList, nodup := Cooper2023.Dogs.Ind.enumList_nodup }, complete := Cooper2023.Dogs.instFintypeInd._proof_1 }

@[instance_reducible]

instance Cooper2023.Dogs.instMeasurableSpaceInd : MeasurableSpace Ind

Equations

• Cooper2023.Dogs.instMeasurableSpaceInd = ⊤

instance Cooper2023.Dogs.instMeasurableSingletonClassInd : MeasurableSingletonClass Ind

def Cooper2023.Dogs.IsDog (x : Ind) : Prop

Equations

• Cooper2023.Dogs.IsDog x = (x ≠ Cooper2023.Dogs.Ind.luna)

@[instance_reducible]

instance Cooper2023.Dogs.instDecidablePredIndIsDog : DecidablePred IsDog

Equations

• Cooper2023.Dogs.instDecidablePredIndIsDog x✝ = id inferInstance

def Cooper2023.Dogs.Bark (x : Ind) : Prop

Equations

• Cooper2023.Dogs.Bark x = (x = Cooper2023.Dogs.Ind.fido ∨ x = Cooper2023.Dogs.Ind.spot)

@[instance_reducible]

instance Cooper2023.Dogs.instDecidablePredIndBark : DecidablePred Bark

Equations

• Cooper2023.Dogs.instDecidablePredIndBark x✝ = id inferInstance

def Cooper2023.Dogs.dog : Ppty Ind

The property dog' (61a) lifts being a dog to a type.

Equations

• Cooper2023.Dogs.dog x = PLift (Cooper2023.Dogs.IsDog x)

def Cooper2023.Dogs.bark : Ppty Ind

The property bark' (61b) lifts barking to a type.

Equations

• Cooper2023.Dogs.bark x = PLift (Cooper2023.Dogs.Bark x)

def Cooper2023.Dogs.aDogBarks : SemIndefArt dog bark

A dog barks (63) is witnessed by Fido.

Equations

• Cooper2023.Dogs.aDogBarks = { x := Cooper2023.Dogs.Ind.fido, pWit := { down := Cooper2023.Dogs.aDogBarks._proof_1 }, qWit := { down := Cooper2023.Dogs.aDogBarks._proof_2 } }

theorem Cooper2023.Dogs.noDogBarks_isEmpty : IsEmpty (SemNo dog bark)

theorem Cooper2023.Dogs.noDogBarksSet_isEmpty : IsEmpty (ParticularWCNeg IsDog CardRel.every bark)

No dog barks with the witness set of every dog, whose members they picks up in (71), is false as well.

def Cooper2023.Dogs.mostDogsBark : GeneralWCIncr IsDog (CardRel.propAtLeast 3 5) bark

Most dogs bark (74) is witnessed by the set of Fido and Spot, two of the three dogs, each barking, which they picks up in (75). The threshold 3 / 5 lies in the range .5 < θ_most(P) < 1 of the book's appendix type list.

Equations

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

theorem Cooper2023.Dogs.mostDogsBark_uniformOn : 3 / 5 ≤ (ProbabilityTheory.uniformOn ↑{x : Ind | IsDog x}) ↑mostDogsBark.X

By its probability (50), the same witness set holds at least three fifths of the dogs.

def Cooper2023.Dogs.fewDogsBark : ParticularWCNeg IsDog (CardRel.compPropAtMost 2 3) bark

Few dogs barked. They didn't hear the intruder (87) is witnessed under the particular condition for few_p (86), with θ_fewp = 2 / 3, by the complement witness set of Rex, who does not bark.

Equations

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

theorem Cooper2023.Dogs.fewDogsBark_general : Nonempty (GeneralWCDecr IsDog (CardRel.propAtMost 2 3) bark)

Under the general condition (80) the same content says that at most two thirds of the dogs bark.

inductive Cooper2023.Dogs.Ty : Type

• dog : Ty
• bark : Ty

@[instance_reducible]

instance Cooper2023.Dogs.instDecidableEqTy : DecidableEq Ty

Equations

• Cooper2023.Dogs.instDecidableEqTy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cooper2023.Dogs.instReprTy : Repr Ty

Equations

• Cooper2023.Dogs.instReprTy = { reprPrec := Cooper2023.Dogs.instReprTy.repr }

def Cooper2023.Dogs.instReprTy.repr : Ty → ℕ → Std.Format

Equations

• Cooper2023.Dogs.instReprTy.repr Cooper2023.Dogs.Ty.dog prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.Dogs.Ty.dog")).group prec✝
• Cooper2023.Dogs.instReprTy.repr Cooper2023.Dogs.Ty.bark prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023.Dogs.Ty.bark")).group prec✝

def Cooper2023.Dogs.experience : ExperienceBase Ind Ty

An experience base of three dogs, two of which were judged to bark.

Equations

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

theorem Cooper2023.Dogs.bark_given_dog : (ProbabilityTheory.uniformOn ↑(experience.extension Ty.dog)) ↑(experience.extension Ty.bark) = 2 / 3

The estimate p_𝔍(bark ‖ dog) (39) is two thirds.

Type-based underspecification (Ch. 8)

Storage and retrieval give scope ambiguity (17)–(19), locality marking constrains anaphoric combination (28)–(88), and localisation with purification gives the donkey readings (49)–(66).

Parametric contents and their context types (§8.2–8.3)

structure Cooper2023.CntxtType (E : Type) : Type 1

A context type (§4.3, (16); §8.2, (10); §8.3, (82)) says what a content requires of the context, namely the quantifiers in the store 𝔮 (11) under their labels and the labels of pronouns, 𝔰, among them those marked local, 𝔩, and reflexive, 𝔯.

• store : ℕ → Option ((ℕ → E) → Quant E)
• pronouns : Finset ℕ
• locals : Finset ℕ
• reflexives : Finset ℕ

@[instance_reducible]

instance Cooper2023.CntxtType.instEmptyCollection {E : Type} : EmptyCollection (CntxtType E)

The empty context type requires nothing.

Equations

• Cooper2023.CntxtType.instEmptyCollection = { emptyCollection := { store := fun (x : ℕ) => none, pronouns := ∅, locals := ∅, reflexives := ∅ } }

def Cooper2023.CntxtType.merge {E : Type} (a b : CntxtType E) : CntxtType E

The merge ∧̣ of two context types joins their fields, the first's store taking precedence.

Equations

• a.merge b = { store := fun (i : ℕ) => (a.store i).or (b.store i), pronouns := a.pronouns ∪ b.pronouns, locals := a.locals ∪ b.locals, reflexives := a.reflexives ∪ b.reflexives }

def Cooper2023.CntxtType.erase {E : Type} (T : CntxtType E) (i : ℕ) : CntxtType E

T ⊖ xᵢ (18) removes the label from the store and the pronouns, with the markings that depend on it (19).

Equations

• T.erase i = { store := Function.update T.store i none, pronouns := T.pronouns.erase i, locals := T.locals.erase i, reflexives := T.reflexives.erase i }

structure Cooper2023.Content (E : Type) (C : Type u_1) : Type (max 1 u_1)

A parametric content (14) over the contexts of Ch. 8, which assign individuals to labels, pairs a background context type with a foreground giving a content for each assignment.

• bg : CntxtType E
• fg : (ℕ → E) → C

def Cooper2023.Content.app {E : Type} {C : Type u_1} {D : Type u_2} (α : Content E (C → D)) (β : Content E C) : Content E D

Application α @ β applies a functor content to an argument, merging the backgrounds.

Equations

• α.app β = { bg := α.bg.merge β.bg, fg := fun (g : ℕ → E) => α.fg g (β.fg g) }

def Cooper2023.Content.given {E : Type} {C : Type u_1} (α : Content E C) (i : ℕ) (a : E) : Content E C

α.given i a is the content given the value a for the label i, the context specification c[𝔰.xᵢ = a] behind retrieval (19), reflexivisation (84) and the alignment of a pronoun with its antecedent (42)–(44).

Equations

• α.given i a = { bg := α.bg.erase i, fg := fun (g : ℕ → E) => α.fg (Function.update g i a) }

def Cooper2023.Content.IsPlugged {E : Type} {C : Type u_1} (α : Content E C) : Prop

A content is plugged (16) when it requires nothing in the store.

Equations

• α.IsPlugged = ∀ (i : ℕ), α.bg.store i = none

def Cooper2023.Content.store {E : Type} (i : ℕ) (𝒬 : Content E (Quant E)) : Content E (Quant E)

Storage (17) puts the quantifier into the store under i, and the content of the label's value takes its place.

Equations

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

def Cooper2023.Content.pronoun {E : Type} (i : ℕ) : Content E (Quant E)

A pronoun (75) has the content of its label's value, marked local.

Equations

• Cooper2023.Content.pronoun i = { bg := { store := fun (x : ℕ) => none, pronouns := {i}, locals := {i}, reflexives := ∅ }, fg := fun (g : ℕ → E) => Cooper2023.SemPropName (g i) }

def Cooper2023.Content.reflexive {E : Type} (i : ℕ) : Content E (Quant E)

A reflexive (83) has the content of its label's value, marked reflexive.

Equations

• Cooper2023.Content.reflexive i = { bg := { store := fun (x : ℕ) => none, pronouns := {i}, locals := ∅, reflexives := {i} }, fg := fun (g : ℕ → E) => Cooper2023.SemPropName (g i) }

def Cooper2023.Content.retrieve {E : Type} (i : ℕ) (α : Content E Type) : Content E Type

Retrieval (19) gives the quantifier stored under i scope over the content as a property of the label's value, and removes it from the store; with nothing stored there the content is unchanged. The purification that (19) applies to the property is the identity here, the foreground being total in the assignment.

Equations

• Cooper2023.Content.retrieve i α = match α.bg.store i with | some 𝒬 => { bg := α.bg.erase i, fg := fun (g : ℕ → E) => 𝒬 g fun (a : E) => (α.given i a).fg g } | none => α

def Cooper2023.Content.relabel {E : Type} {C : Type u_1} (α : Content E C) (j i : ℕ) : Content E C

The relabelling [α]𝔰.xⱼ ⇝ 𝔰.xᵢ reads the label j as i, and drops j from the background.

Equations

• α.relabel j i = { bg := α.bg.erase j, fg := fun (g : ℕ → E) => α.fg (Function.update g j (g i)) }

def Cooper2023.Content.AnaphoricDefined {E : Type} {C : Type u_1} {D : Type u_2} (α : Content E (C → D)) (i j : ℕ) (β : Content E C) : Prop

Anaphoric combination α @ᵢ,ⱼ β (28), (76) is defined when the functor requires the label i and the argument requires j as a pronoun that is neither a stored quantifier's nor marked local.

Equations

• α.AnaphoricDefined i j β = (i ∈ α.bg.pronouns ∧ j ∈ β.bg.pronouns ∧ β.bg.store j = none ∧ j ∉ β.bg.locals)

@[instance_reducible]

instance Cooper2023.Content.instDecidableAnaphoricDefined {E : Type} {C : Type u_1} {D : Type u_2} (α : Content E (C → D)) (i j : ℕ) (β : Content E C) : Decidable (α.AnaphoricDefined i j β)

Equations

• α.instDecidableAnaphoricDefined i j β = id inferInstance

def Cooper2023.Content.anaphoricApp {E : Type} {C : Type u_1} {D : Type u_2} (α : Content E (C → D)) (i j : ℕ) (β : Content E C) : Content E D

Anaphoric combination α @ᵢ,ⱼ β (28) is the application with j relabelled to i.

Equations

• α.anaphoricApp i j β = (α.app β).relabel j i

def Cooper2023.Content.boundary {E : Type} {C : Type u_1} (α : Content E C) : Content E C

The boundary operation B (77) clears the local marking at the sentence.

Equations

• α.boundary = { bg := have __src := α.bg; { store := __src.store, pronouns := __src.pronouns, locals := ∅, reflexives := __src.reflexives }, fg := α.fg }

def Cooper2023.Content.reflexivize {E : Type} (P : Content E (Ppty E)) (i : ℕ) : Content E (Ppty E)

Reflexivisation ℜ (84) binds the reflexive i to the property's argument, discharging its label and clearing all reflexive marking.

Equations

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

def Cooper2023.Content.IsAnaphorFree {E : Type} {C : Type u_1} (α : Content E C) : Prop

Principle A (85) excludes at the verb phrase (88) a content with a reflexive still marked.

Equations

• α.IsAnaphorFree = (α.bg.reflexives = ∅)

@[instance_reducible]

instance Cooper2023.Content.instDecidableIsAnaphorFree {E : Type} {C : Type u_1} (α : Content E C) : Decidable α.IsAnaphorFree

Equations

• α.instDecidableIsAnaphorFree = id inferInstance

Every boy hugged a dog (§8.1, (1))

With each boy hugging a different dog, the surface reading (1a) is witnessed and the inverse reading (1b) is not.

inductive Cooper2023.Hugging.Ind : Type

• tom : Ind
• bill : Ind
• fido : Ind
• rex : Ind

@[instance_reducible]

instance Cooper2023.Hugging.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023.Hugging.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023.Hugging.Boy : Ppty Ind

Equations

• Cooper2023.Hugging.Boy Cooper2023.Hugging.Ind.tom = PUnit.{1}
• Cooper2023.Hugging.Boy Cooper2023.Hugging.Ind.bill = PUnit.{1}
• Cooper2023.Hugging.Boy x✝ = Empty

def Cooper2023.Hugging.Dog : Ppty Ind

Equations

• Cooper2023.Hugging.Dog Cooper2023.Hugging.Ind.fido = PUnit.{1}
• Cooper2023.Hugging.Dog Cooper2023.Hugging.Ind.rex = PUnit.{1}
• Cooper2023.Hugging.Dog x✝ = Empty

def Cooper2023.Hugging.Hug : Ind → Ind → Type

Equations

• Cooper2023.Hugging.Hug Cooper2023.Hugging.Ind.tom Cooper2023.Hugging.Ind.fido = PUnit.{1}
• Cooper2023.Hugging.Hug Cooper2023.Hugging.Ind.bill Cooper2023.Hugging.Ind.rex = PUnit.{1}
• Cooper2023.Hugging.Hug x✝¹ x✝ = Empty

def Cooper2023.Hugging.everyBoy : Content Ind (Quant Ind)

Equations

• Cooper2023.Hugging.everyBoy = { bg := ∅, fg := fun (x : ℕ → Cooper2023.Hugging.Ind) => Cooper2023.SemUniversal Cooper2023.Hugging.Boy }

def Cooper2023.Hugging.aDog : Content Ind (Quant Ind)

Equations

• Cooper2023.Hugging.aDog = { bg := ∅, fg := fun (x : ℕ → Cooper2023.Hugging.Ind) => Cooper2023.SemIndefArt Cooper2023.Hugging.Dog }

def Cooper2023.Hugging.hugged : Content Ind (Quant Ind → Ppty Ind)

hugged is a transitive verb over its object quantifier (Ch. 6, (63)).

Equations

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

def Cooper2023.Hugging.surface : Content Ind Type

Reading (1a) keeps the quantifiers in surface order.

Equations

• Cooper2023.Hugging.surface = Cooper2023.Hugging.everyBoy.app (Cooper2023.Hugging.hugged.app Cooper2023.Hugging.aDog)

def Cooper2023.Hugging.inverse : Content Ind Type

Reading (1b) stores the object quantifier (17) and retrieves it (19) over the sentence.

Equations

• Cooper2023.Hugging.inverse = Cooper2023.Content.retrieve 0 (Cooper2023.Hugging.everyBoy.app (Cooper2023.Hugging.hugged.app (Cooper2023.Content.store 0 Cooper2023.Hugging.aDog)))

theorem Cooper2023.Hugging.not_isPlugged_stored : ¬(everyBoy.app (hugged.app (Content.store 0 aDog))).IsPlugged

theorem Cooper2023.Hugging.isPlugged_inverse : inverse.IsPlugged

theorem Cooper2023.Hugging.inverse_fg (g : ℕ → Ind) : inverse.fg g = SemIndefArt Dog fun (y : Ind) => SemUniversal Boy fun (x : Ind) => Hug x y

(1b) is the indefinite over the universal.

def Cooper2023.Hugging.surfaceWitness (g : ℕ → Ind) : surface.fg g

Reading (1a) is witnessed, every boy having hugged a dog.

Equations

• Cooper2023.Hugging.surfaceWitness g Cooper2023.Hugging.Ind.tom x_2 = { x := Cooper2023.Hugging.Ind.fido, pWit := PUnit.unit, qWit := PUnit.unit }
• Cooper2023.Hugging.surfaceWitness g Cooper2023.Hugging.Ind.bill x_2 = { x := Cooper2023.Hugging.Ind.rex, pWit := PUnit.unit, qWit := PUnit.unit }

theorem Cooper2023.Hugging.inverse_isEmpty (g : ℕ → Ind) : IsEmpty (inverse.fg g)

Reading (1b) is not, no dog having been hugged by every boy.

Localisation and donkey anaphora (§8.3)

def Cooper2023.localize {E : Type} (P : Content E (Ppty E)) : Restricted E

Localisation ℒ (49) folds the assignment a content requires into the property's domain under the label 𝔠, giving a restricted property.

Equations

• Cooper2023.localize P = { restr := fun (x : E) => ℕ → E, body := fun (x : E) (g : ℕ → E) => P.fg g x }

No dog which chases a cat catches it (46a)

Under the particular condition for no, (55) says that no dog which chases a cat catches the cat it chases.

inductive Cooper2023.Chasing.Ind : Type

• dog₁ : Ind
• dog₂ : Ind
• cat₁ : Ind
• cat₂ : Ind

@[instance_reducible]

instance Cooper2023.Chasing.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023.Chasing.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023.Chasing.Dog : Ppty Ind

Equations

• Cooper2023.Chasing.Dog Cooper2023.Chasing.Ind.dog₁ = PUnit.{1}
• Cooper2023.Chasing.Dog Cooper2023.Chasing.Ind.dog₂ = PUnit.{1}
• Cooper2023.Chasing.Dog x✝ = Empty

def Cooper2023.Chasing.Cat : Ppty Ind

Equations

• Cooper2023.Chasing.Cat Cooper2023.Chasing.Ind.cat₁ = PUnit.{1}
• Cooper2023.Chasing.Cat Cooper2023.Chasing.Ind.cat₂ = PUnit.{1}
• Cooper2023.Chasing.Cat x✝ = Empty

def Cooper2023.Chasing.Chase : Ind → Ind → Type

Equations

• Cooper2023.Chasing.Chase Cooper2023.Chasing.Ind.dog₁ Cooper2023.Chasing.Ind.cat₁ = PUnit.{1}
• Cooper2023.Chasing.Chase Cooper2023.Chasing.Ind.dog₂ Cooper2023.Chasing.Ind.cat₂ = PUnit.{1}
• Cooper2023.Chasing.Chase x✝¹ x✝ = Empty

def Cooper2023.Chasing.catches (Catch : Ind → Ind → Type) : Content Ind (Quant Ind → Ppty Ind)

catches is a transitive verb over its object quantifier (Ch. 6, (63)).

Equations

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

def Cooper2023.Chasing.catchesIt (Catch : Ind → Ind → Type) : Content Ind (Ppty Ind)

In catches it (47) the context supplies the referent of the pronoun's label.

Equations

• Cooper2023.Chasing.catchesIt Catch = (Cooper2023.Chasing.catches Catch).app (Cooper2023.Content.pronoun 1)

def Cooper2023.Chasing.DogChasesACat : Ppty Ind

The restrictor dog which chases a cat, as the domain of (50), holds a dog with a cat it chases.

Equations

• Cooper2023.Chasing.DogChasesACat x = (Cooper2023.Chasing.Dog x × (c : Cooper2023.Chasing.Ind) × Cooper2023.Chasing.Cat c × Cooper2023.Chasing.Chase x c)

def Cooper2023.Chasing.scope (Catch : Ind → Ind → Type) : Restricted Ind

The scope (51) is catches it localised, restricted by the restrictor and aligned so that the pronoun's label is the chased cat.

Equations

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

def Cooper2023.Chasing.Sentence (Catch : Ind → Ind → Type) : Type

The sentence (55) is no(restr, scope) with the scope purified.

Equations

• Cooper2023.Chasing.Sentence Catch = Cooper2023.SemNo Cooper2023.Chasing.DogChasesACat (Cooper2023.Purify (Cooper2023.Chasing.scope Catch))

def Cooper2023.Chasing.noCatching : Sentence fun (x x_1 : Ind) => Empty

The sentence is true when no dog catches anything.

Equations

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

theorem Cooper2023.Chasing.sentence_isEmpty : IsEmpty (Sentence Chase)

The sentence is false when every dog catches the cat it chases.

Every farmer who owns a donkey likes it (58)–(66)

𝔓 gives the weak reading and 𝔓∀ the strong one of [Kan94], separated by a farmer who owns two donkeys and likes one.

inductive Cooper2023.Donkeys.Ind : Type

• farmer₁ : Ind
• farmer₂ : Ind
• donkey₁ : Ind
• donkey₂ : Ind

@[instance_reducible]

instance Cooper2023.Donkeys.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023.Donkeys.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023.Donkeys.Farmer : Ppty Ind

Equations

• Cooper2023.Donkeys.Farmer Cooper2023.Donkeys.Ind.farmer₁ = PUnit.{1}
• Cooper2023.Donkeys.Farmer Cooper2023.Donkeys.Ind.farmer₂ = PUnit.{1}
• Cooper2023.Donkeys.Farmer x✝ = Empty

def Cooper2023.Donkeys.Donkey : Ppty Ind

Equations

• Cooper2023.Donkeys.Donkey Cooper2023.Donkeys.Ind.donkey₁ = PUnit.{1}
• Cooper2023.Donkeys.Donkey Cooper2023.Donkeys.Ind.donkey₂ = PUnit.{1}
• Cooper2023.Donkeys.Donkey x✝ = Empty

def Cooper2023.Donkeys.Own : Ind → Ind → Type

The first farmer owns both donkeys, the second the second.

Equations

• Cooper2023.Donkeys.Own Cooper2023.Donkeys.Ind.farmer₁ Cooper2023.Donkeys.Ind.donkey₁ = PUnit.{1}
• Cooper2023.Donkeys.Own Cooper2023.Donkeys.Ind.farmer₁ Cooper2023.Donkeys.Ind.donkey₂ = PUnit.{1}
• Cooper2023.Donkeys.Own Cooper2023.Donkeys.Ind.farmer₂ Cooper2023.Donkeys.Ind.donkey₂ = PUnit.{1}
• Cooper2023.Donkeys.Own x✝¹ x✝ = Empty

def Cooper2023.Donkeys.Like : Ind → Ind → Type

Equations

• Cooper2023.Donkeys.Like Cooper2023.Donkeys.Ind.farmer₁ Cooper2023.Donkeys.Ind.donkey₁ = PUnit.{1}
• Cooper2023.Donkeys.Like Cooper2023.Donkeys.Ind.farmer₂ Cooper2023.Donkeys.Ind.donkey₂ = PUnit.{1}
• Cooper2023.Donkeys.Like x✝¹ x✝ = Empty

def Cooper2023.Donkeys.FarmerOwnsADonkey : Ppty Ind

farmer who owns a donkey holds a farmer with a donkey she owns.

Equations

• Cooper2023.Donkeys.FarmerOwnsADonkey x = (Cooper2023.Donkeys.Farmer x × (d : Cooper2023.Donkeys.Ind) × Cooper2023.Donkeys.Donkey d × Cooper2023.Donkeys.Own x d)

def Cooper2023.Donkeys.likes : Content Ind (Quant Ind → Ppty Ind)

likes is a transitive verb over its object quantifier (Ch. 6, (63)).

Equations

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

def Cooper2023.Donkeys.likesIt : Restricted Ind

likes it (61) is localised (62)–(63), restricted (64) and aligned (65), the pronoun's label being the owned donkey.

Equations

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

def Cooper2023.Donkeys.weak : SemUniversal FarmerOwnsADonkey (Purify likesIt)

The weak reading (59) holds, every farmer who owns a donkey liking some donkey she owns.

Equations

• Cooper2023.Donkeys.weak Cooper2023.Donkeys.Ind.farmer₁ x_2 = ⟨(PUnit.unit, ⟨Cooper2023.Donkeys.Ind.donkey₁, (PUnit.unit, PUnit.unit)⟩), PUnit.unit⟩
• Cooper2023.Donkeys.weak Cooper2023.Donkeys.Ind.farmer₂ x_2 = ⟨(PUnit.unit, ⟨Cooper2023.Donkeys.Ind.donkey₂, (PUnit.unit, PUnit.unit)⟩), PUnit.unit⟩

theorem Cooper2023.Donkeys.strong_isEmpty : IsEmpty (SemUniversal FarmerOwnsADonkey (PurifyUniv likesIt))

The strong reading (60), (66) fails, since the first farmer does not like the second donkey.

Pronouns, locality and reflexives (30)–(36), (67)–(88)

A stored no girl binds she past the embedded boundary, the local him of Sam likes him cannot combine with Sam (Principle B), and himself is bound by reflexivisation.

inductive Cooper2023.Binding.Ind : Type

• sam : Ind
• kim : Ind
• ann : Ind

@[instance_reducible]

instance Cooper2023.Binding.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023.Binding.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023.Binding.Girl : Ppty Ind

Equations

• Cooper2023.Binding.Girl Cooper2023.Binding.Ind.ann = PUnit.{1}
• Cooper2023.Binding.Girl x✝ = Empty

inductive Cooper2023.Binding.Fail : Ind → Type

inductive Cooper2023.Binding.Like : Ind → Ind → Type

• mk : Like Ind.sam Ind.sam

structure Cooper2023.Binding.Think (x : Ind) (T : Type) : Type

A witness of think(x, T) is a thought with the type's witness.

• thought : T

def Cooper2023.Binding.sam : Content Ind (Quant Ind)

Equations

• Cooper2023.Binding.sam = { bg := ∅, fg := fun (x : ℕ → Cooper2023.Binding.Ind) => Cooper2023.SemPropName Cooper2023.Binding.Ind.sam }

def Cooper2023.Binding.noGirl : Content Ind (Quant Ind)

Equations

• Cooper2023.Binding.noGirl = { bg := ∅, fg := fun (x : ℕ → Cooper2023.Binding.Ind) => Cooper2023.SemNo Cooper2023.Binding.Girl }

def Cooper2023.Binding.failed : Content Ind (Ppty Ind)

Equations

• Cooper2023.Binding.failed = { bg := ∅, fg := fun (x : ℕ → Cooper2023.Binding.Ind) => Cooper2023.Binding.Fail }

def Cooper2023.Binding.thinks : Content Ind (Type → Ppty Ind)

thinks takes a ptype of thinking.

Equations

• Cooper2023.Binding.thinks = { bg := ∅, fg := fun (x : ℕ → Cooper2023.Binding.Ind) (T : Type) (x_1 : Cooper2023.Binding.Ind) => Cooper2023.Binding.Think x_1 T }

def Cooper2023.Binding.likes : Content Ind (Quant Ind → Ppty Ind)

likes is a transitive verb over its object quantifier (Ch. 6, (63)).

Equations

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

def Cooper2023.Binding.thinksSheFailed : Content Ind (Ppty Ind)

In thinks she failed (31) the embedded she failed is a sentence, so its pronoun is no longer local past the boundary.

Equations

• Cooper2023.Binding.thinksSheFailed = Cooper2023.Binding.thinks.app ((Cooper2023.Content.pronoun 1).app Cooper2023.Binding.failed).boundary

theorem Cooper2023.Binding.anaphoricDefined_thinksSheFailed : (Content.store 0 noGirl).AnaphoricDefined 0 1 thinksSheFailed

The stored subject (34) combines anaphorically with the pronoun, (35).

theorem Cooper2023.Binding.not_anaphoricDefined_of_no_boundary : ¬(Content.store 0 noGirl).AnaphoricDefined 0 1 (thinks.app ((Content.pronoun 1).app failed))

theorem Cooper2023.Binding.noGirlThinksSheFailed (g : ℕ → Ind) : (Content.retrieve 0 ((Content.store 0 noGirl).anaphoricApp 0 1 thinksSheFailed)).fg g = SemNo Girl fun (x : Ind) => Think x (Fail x)

No girl thinks she failed (36), the stored no girl retrieved over the anaphoric combination, is no(girl', λx. think(x, fail(x))).

def Cooper2023.Binding.likesHim : Content Ind (Ppty Ind)

In likes him (69) the pronoun is marked local.

Equations

• Cooper2023.Binding.likesHim = Cooper2023.Binding.likes.app (Cooper2023.Content.pronoun 1)

theorem Cooper2023.Binding.not_anaphoricDefined_likesHim : ¬(Content.store 0 sam).AnaphoricDefined 0 1 likesHim

Within the clause him cannot be related to the stored Sam (71), which is Principle B, (72)–(73).

def Cooper2023.Binding.likesHimself : Content Ind (Ppty Ind)

likes himself is reflexivised (84).

Equations

• Cooper2023.Binding.likesHimself = (Cooper2023.Binding.likes.app (Cooper2023.Content.reflexive 1)).reflexivize 1

theorem Cooper2023.Binding.likesHimself_fg (g : ℕ → Ind) (x : Ind) : likesHimself.fg g x = Like x x

The reflexivised property is like(x, x) (68c).

theorem Cooper2023.Binding.isAnaphorFree_likesHimself : likesHimself.IsAnaphorFree

Reflexivisation clears the marking for the verb phrase's filter (88).

theorem Cooper2023.Binding.not_isAnaphorFree_likesReflexive : ¬(likes.app (Content.reflexive 1)).IsAnaphorFree

def Cooper2023.Binding.samLikesHimself (g : ℕ → Ind) : (Content.retrieve 0 ((Content.store 0 sam).app likesHimself)).fg g

Sam likes himself (73), the stored Sam retrieved, is witnessed by Sam's liking himself.

Equations

• Cooper2023.Binding.samLikesHimself g = Cooper2023.Binding.Like.mk

A man walked. He whistled. (37)–(44)

The pronoun's label is given the man of the previous utterance's witness (42)–(44).

inductive Cooper2023.Whistling.Ind : Type

• john : Ind
• mary : Ind

@[instance_reducible]

instance Cooper2023.Whistling.instDecidableEqInd : DecidableEq Ind

Equations

• Cooper2023.Whistling.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023.Whistling.Man : Ppty Ind

Equations

• Cooper2023.Whistling.Man Cooper2023.Whistling.Ind.john = PUnit.{1}
• Cooper2023.Whistling.Man Cooper2023.Whistling.Ind.mary = Empty

def Cooper2023.Whistling.Walk : Ppty Ind

Equations

• Cooper2023.Whistling.Walk Cooper2023.Whistling.Ind.john = PUnit.{1}
• Cooper2023.Whistling.Walk Cooper2023.Whistling.Ind.mary = Empty

def Cooper2023.Whistling.Whistle : Ppty Ind

Equations

• Cooper2023.Whistling.Whistle Cooper2023.Whistling.Ind.john = PUnit.{1}
• Cooper2023.Whistling.Whistle Cooper2023.Whistling.Ind.mary = Empty

def Cooper2023.Whistling.AManWalked : Type

The content of a man walked (38) is the particular condition for exist.

Equations

• Cooper2023.Whistling.AManWalked = Cooper2023.SemIndefArt Cooper2023.Whistling.Man Cooper2023.Whistling.Walk

def Cooper2023.Whistling.aManWalked : AManWalked

John walked.

Equations

• Cooper2023.Whistling.aManWalked = { x := Cooper2023.Whistling.Ind.john, pWit := PUnit.unit, qWit := PUnit.unit }

def Cooper2023.Whistling.heWhistled : Content Ind Type

he whistled (39) requires the pronoun's label of the context.

Equations

• Cooper2023.Whistling.heWhistled = ((Cooper2023.Content.pronoun 0).app { bg := ∅, fg := fun (x : ℕ → Cooper2023.Whistling.Ind) => Cooper2023.Whistling.Whistle }).boundary

theorem Cooper2023.Whistling.heWhistled_given (w : AManWalked) (g : ℕ → Ind) : (heWhistled.given 0 w.x).bg.pronouns = ∅ ∧ (heWhistled.given 0 w.x).fg g = Whistle w.x

Given the previous utterance's witness, the pronoun's label is no longer required and the content is that the man whistled, (42)–(44).

def Cooper2023.Whistling.heWhistledWitness (g : ℕ → Ind) : (heWhistled.given 0 aManWalked.x).fg g

Equations

• Cooper2023.Whistling.heWhistledWitness g = PUnit.unit

The book's examples

The rows of Data/Examples/Cooper2023.json with a quantifier feature are the anaphora examples of §7.4, §7.4.1 and §8.3, each reading named by the anaphora set its pronoun picks up.

def Cooper2023.quantNames : List (String × QuantName)

quantNames pairs each row's determiner with the quantifier relation it names.

Equations

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

def Cooper2023.anaphoraRefs : List (String × AnaphoraRef)

anaphoraRefs pairs each reading's name with the anaphora set it names.

Equations

• Cooper2023.anaphoraRefs = [("refset", Cooper2023.AnaphoraRef.refset), ("maxset", Cooper2023.AnaphoraRef.maxset), ("compset", Cooper2023.AnaphoraRef.compset)]

theorem Cooper2023.anaphora_rows (row : Datum) : row ∈ Examples.all → ∀ v ∈ row.feature? "quantifier", ∃ q ∈ List.lookup v quantNames, ∀ r ∈ row.readings, ∃ ref ∈ List.lookup r.1 anaphoraRefs, r.2 = Judgment.acceptable ↔ ref ∈ anaphoraAvailable q

A reading of a pronoun with a quantified antecedent is acceptable exactly when a witness for the content provides a path to its anaphora set.