Cooper's type theory with records

Cooper's theory of types with records has Lean's own type theory as its metatheory: the judgement a : T is the ambient typing, a type is true when inhabited, a record type is a structure whose structural subtypes are the structures with more fields, and the intensionality of types with the same witnesses is the ambient theory's as well. On this basis the file follows the book's chapters: the contents of proper names, the indefinite article and the copula, with a is a P witnessed exactly when P(a) is (Ch. 3), and parametric content (Ch. 4); modal type systems with their restrictive and inclusive notions, necessity and possibility relative to a background type and a topos in place of an accessibility relation, and intensionality as the matching of types against an agent's long-term memory, religious beliefs and desires through points of view (Ch. 6); restricted properties and their two purifications, the frequentist probability of a witness set and its estimate from an experience base, and the witness conditions whose witnesses carry what discourse anaphora picks up (Ch. 7); and parametric contents over a context type of pronoun labels, on which storage and retrieval derive the scope readings, anaphoric combination with the sentence boundary and reflexivisation derive Principles B and A, and localisation derives the weak and strong donkey readings (Ch. 8). A selection of the book's English examples are the rows of Data/Examples/Cooper2023.json, against which the anaphora sets the substrate derives for each quantifier are checked.

Implementation notes

• A property is E → Type with Cooper's record [x : Ind] collapsed to its individual, and a ptype p(a) a type of situations, so the common-noun content is the identity and unnamed. Relabelling is absorbed into the function witnessing a subtyping, and compatibility and the topos conditions are read in the ambient possibility.
• The indefinite article and no are the particular witness conditions of Semantics/Quantification/Witness.lean, and the dogs fragment uses its set-based conditions over decidable predicates; modal type systems and Breitholtz's topoi stay here, having no second consumer.
• A context type records the labels a content requires of the assignments to stored quantifiers, pronouns, local pronouns and reflexives; the wh-phrase and gap assignments of (82) and the incrementation of labels at combination are omitted, labels being chosen distinct by hand. Context specification c[𝔰.xᵢ = a] is the one primitive behind retrieval, reflexivisation and cross-sentential resolution.
• Restriction and alignment of a property's domain (Ch. 8, (51)–(52)) are further restrictions through which the body is read, so purification applies to them uniformly.

TODO

• Inclusive possibility is stated as the book prints (2d), an implication under an existential, which any possibility in which the type does not occur satisfies; the intended clause is presumably a conjunction.
• 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 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 [denic-sudo-2022] 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)
• [A. Kratzer, What 'must' and 'can' must and can mean (1977)][kratzer-1977]
• [A. Kratzer, The Notional Category of Modality (1981)][kratzer-1981]
• E. Breitholtz, Enthymemes and Topoi in Dialogue (2020)
• [G. Chierchia, Dynamics of Meaning (1995)][chierchia-1995b]
• M. Kanazawa, Weak vs. Strong Readings of Donkey Sentences (1994)
• [A. Ranta, Type-Theoretical Grammar (1994)][ranta-1994]
• R. Montague, The Proper Treatment of Quantification in Ordinary English (1973)
• [M. Denić, Y. Sudo, Donkey Anaphora in Non-Monotonic Environments (2022)][denic-sudo-2022]
• L. Champollion, D. Bumford, R. Henderson, Donkeys under Discussion (2019)

Types, properties and contents (Chs. 1, 3, 4)

Structural subtyping (§1.4.3.5)

structure Cooper2023.BoyAndDog (E : Type) (Boy Dog : E → Type) : Type

The type of situations with a boy and a dog, (53a).

• x : E
• c₁ : Boy self.x
• y : E
• c₂ : Dog self.y

structure Cooper2023.BoyHugsDog (E : Type) (Boy Dog : E → Type) (Hug : E → E → Type) extends Cooper2023.BoyAndDog E Boy Dog : Type

The type of situations in which the boy hugs the dog, (53b): a subtype of (53a) by having more fields, the projection being toBoyAndDog.

• x : E
• c₁ : Boy self.x
• y : E
• c₂ : Dog self.y
• e : Hug self.x self.y

Properties, quantifiers and their contents (§3.4)

@[reducible, inline]

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

A property (30): the individuals' types of situations.

Equations

• Cooper2023.Ppty E = (E → Type)

@[reducible, inline]

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

A quantifier: a function from properties to types, Montague's ⟨⟨e,t⟩,t⟩.

Equations

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

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

SemPropName(a) (33): the quantifier applying its property to the individual.

Equations

• Cooper2023.SemPropName a P = P a

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

SemIndefArt (37): 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 = Quantification.ParticularWC_Exist restr

theorem Cooper2023.nonempty_semIndefArt_iff {E : Type} (restr scope : Ppty E) : Nonempty (SemIndefArt restr scope) ↔ ∃ (a : E), Nonempty (restr a) ∧ Nonempty (scope a)

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

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

SemBe (78), Montague's copula: 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 as a function from the restrictor's witnesses to the scope's, the function witness of §7.2.4 after [ranta-1994], which, as Cooper notes at (27), yields no witness set for plural anaphora; the set-based condition (72) is GeneralWC_Incr with IsEveryW.

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)): every witness of the restrictor precludes the scope.

Equations

• Cooper2023.SemNo restr scope = Quantification.ParticularWC_No restr scope

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

(92): a is a P, the copula over the indefinite article, is witnessed iff P(a) is, 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)

(94c): a P is a, the quantifiers in the other order, is witnessed iff P(a) is as well; 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 monotone increasing quantifier.

Equations

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

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

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

• bg : Type

  The background: the type of contexts the content requires.

• fg : self.bg → C

  The foreground: the content in each such context.

@[reducible, inline]

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

A parametric property.

Equations

• Cooper2023.PPpty E = Cooper2023.Parametric (Cooper2023.Ppty E)

The Dudamel fragment

Dudamel is a conductor (82c), the existential quantifier under the copula, is witnessed by Dudamel's conducting, and Beethoven is a conductor is not.

inductive Cooper2023.Dudamel.Ind : Type

The individuals.

• 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 ⋯

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

Equations

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

@[instance_reducible]

instance Cooper2023.Dudamel.instReprInd : Repr Ind

Equations

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

inductive Cooper2023.Dudamel.Conductor : Ind → Type

The ptype conductor(x): Dudamel conducts.

• mk : Conductor Ind.dudamel

def Cooper2023.Dudamel.IsAConductor : Ppty Ind

is a conductor (81c).

Equations

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

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

Dudamel is a conductor is true.

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)

Beethoven is a conductor is false.

Modality and intensionality without possible worlds (Ch. 6)

A modal type system (§1.4.3.5, (54); §6.3) is a family of possibilities sharing their types but differing in which objects witness them; equivalence, subtyping, necessity and possibility are defined over all possibilities, (1), or over those in which the types occur, (2). Necessity and possibility in language are relativised, as in Kratzer's semantics, to a background type and a topos, a dependent type from situations to types standing in for the accessibility relation, (20)–(24). Intensionality replaces sets of worlds by types (§6.5): an attitude holds when the type of the agent's long-term memory, religious beliefs or desires matches its complement modulo relabelling, directly or through a point of view, (39)–(92).

Modal type systems (§6.3)

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

A possibility: which types occur in it and which objects witness them.

• occurs : Ty → Prop

  The types of the possibility's type system.

• witnesses : Ty → Obj → Prop

  The objects witnessing each type in the possibility.

@[reducible, inline]

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

A modal system of types (§1.4.3.5, (54)): 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) (p : M) (T : Ty) : Set Obj

The extension of T in the possibility p, (1a).

Equations

• ms.extension p T = {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.EquivR {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) (T₁ T₂ : Ty) : Prop

Restrictive equivalence (1a): the same extension in every possibility.

Equations

• ms.EquivR T₁ T₂ = ∀ (p : M), ms.extension p T₁ = ms.extension p T₂

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

Restrictive subtyping (1b).

Equations

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

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

Restrictive necessity (1c): witnessed in every possibility.

Equations

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

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

Restrictive possibility (1d): witnessed in some possibility.

Equations

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

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

Inclusive equivalence (2a): the same extension wherever both types occur.

Equations

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

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

Inclusive subtyping (2b).

Equations

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

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

Inclusive necessity (2c): witnessed wherever the type occurs.

Equations

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

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

Inclusive possibility (2d), as the book prints it.

Equations

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

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

The restrictive notions entail the inclusive ones (§6.3).

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

theorem Cooper2023.ModalSystem.necI_of_necR {M Ty Obj : Type} (ms : ModalSystem M Ty Obj) {T : Ty} (h : ms.NecR T) : ms.NecI T

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

Modality with topoi (§6.4)

The witness conditions for nec and poss go through four versions; the last, (23)–(24), takes a topos in place of Kratzer's ideal, and, as Cooper notes, has no counterpart of the ordering source.

@[reducible, inline]

abbrev Cooper2023.Topos : Type 1

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

Equations

• Cooper2023.Topos = Cooper2023.Parametric Type

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

Compatibility (17): something is of both types.

Equations

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

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

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

• sit : B

  The situation.

• sub : B → τ.bg

  The background type as a subtype of the topos's domain.

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

  The type the topos returns as a subtype of T.

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

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

• sit : B

  The situation.

• sub : B → τ.bg

  The background type as a subtype of the topos's domain.

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

  The type the topos returns is compatible with 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)

The base situation (26) has the broccoli on Mary's plate and Mary loving it; the deontic topos (28a) sends a situation of a child with food on her plate to her eating it, the bouletic topos (28b) a situation of a child loving some food to her eating it, and nec([e:eat(m,b)], T_broc, τ) is witnessed by either, (29)–(30).

inductive Cooper2023.Dinner.Ind : Type

The individuals.

• 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

The ptypes of the base situation (26), each witnessed by its fact.

• mk : Broccoli Ind.broccoli

inductive Cooper2023.Dinner.Child : Ind → Type

Mary is a child.

• mk : Child Ind.mary

inductive Cooper2023.Dinner.Plate : Ind → Type

The plate is a plate.

• mk : Plate Ind.plate

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

Mary has the plate.

• mk : Have Ind.mary Ind.plate

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

The broccoli is on the plate.

• mk : On Ind.broccoli Ind.plate

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

Mary loves the broccoli.

• mk : Love Ind.mary Ind.broccoli

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

Mary eats the broccoli.

• mk : Eat Ind.mary Ind.broccoli

inductive Cooper2023.Dinner.Food : Ind → Type

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

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

structure Cooper2023.Dinner.Base : Type

The base situation type (26), 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): 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): 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).

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).

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: the broccoli on Mary's plate, which she loves.

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

(29a): eating the broccoli is necessary under the deontic topos, the base type 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

(29b): and under the bouletic topos.

Equations

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

Intensionality (§6.5)

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

Subtyping modulo relabelling (39), T₁ ⊑⇝ T₂.

Equations

• Cooper2023.RelabeledSubtype T₁ T₂ = Nonempty (T₁ → T₂)

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

An agent's total information state (91), long-term memory, religious beliefs and desires as types, with the point-of-view relation on types, (55), (80).

• ltm : Agent → Type

  The type of the agent's long-term memory.

• rbel : Agent → Type

  The type of the agent's religious beliefs.

• des : Agent → Type

  The type of the agent's desires.

• pov : Type → Type → Prop

  pov M T: M is a complete point of view on T, the asymmetric merge of T with an alternative type on some of its labels.

def Cooper2023.InfoState.Matches {Agent : Type} (s : InfoState Agent) (I T : Type) : Prop

An information type I matches T directly, or through a complete point of view M on a type I matches, M matching T, (58), (80), (92).

Equations

• s.Matches I T = (Cooper2023.RelabeledSubtype I T ∨ ∃ (T₁ : Type) (M : Type), Cooper2023.RelabeledSubtype I T₁ ∧ s.pov M T₁ ∧ Cooper2023.RelabeledSubtype M T)

Postulated subtyping: buying and selling, (35), (44)–(47), (50)

structure Cooper2023.SellEvent (E : Type) : Type

A selling situation.

• seller : E
• thing : E
• buyer : E

structure Cooper2023.BuyEvent (E : Type) : Type

A buying situation.

• buyer : E
• thing : E
• seller : E

def Cooper2023.SellEvent.toBuyEvent {E : Type} (e : SellEvent E) : BuyEvent E

The postulate (50b), sell(a, b, c) ⊑ buy(c, b, a), holding only in the possibilities the postulate restricts attention to, unlike the structural (50a), BoyHugsDog.toBoyAndDog.

Equations

• e.toBuyEvent = { buyer := e.buyer, thing := e.thing, seller := e.seller }

def Cooper2023.BuyEvent.toSellEvent {E : Type} (e : BuyEvent E) : SellEvent E

Its converse (47).

Equations

• e.toSellEvent = { seller := e.seller, thing := e.thing, buyer := e.buyer }

def Cooper2023.Believe {Agent : Type} (s : InfoState Agent) (a : Agent) (T : Type) : Prop

believe(a, T) (40): the type of a's long-term memory matches T.

Equations

• Cooper2023.Believe s a T = Cooper2023.RelabeledSubtype (s.ltm a) T

theorem Cooper2023.believe_equiv {Agent : Type} (s : InfoState Agent) (a : Agent) {T T' : Type} (h : Believe s a T) (e : T ≃ T') : Believe s a T'

(41): belief is closed under relabelling.

theorem Cooper2023.believe_of_subtype {Agent : Type} (s : InfoState Agent) (a : Agent) {T₁ T₂ : Type} (h : Believe s a T₁) (f : T₁ → T₂) : Believe s a T₂

Belief is closed under subtyping, structural or postulated.

theorem Cooper2023.believe_sell_of_believe_buy {E Agent : Type} (s : InfoState Agent) (a : Agent) (h : Believe s a (BuyEvent E)) : Believe s a (SellEvent E)

(44)–(47): whoever believes that Kim bought sex from Sam believes that Sam sold sex to Kim, the postulate holding across belief.

def Cooper2023.BelievePov {Agent : Type} (s : InfoState Agent) (a : Agent) (T : Type) : Prop

believe(a, T) with a point of view (58).

Equations

• Cooper2023.BelievePov s a T = s.Matches (s.ltm a) T

def Cooper2023.RBelieve {Agent : Type} (s : InfoState Agent) (a : Agent) (T : Type) : Prop

rbelieve(a, T), characterised after (74): the type of a's religious beliefs matches T.

Equations

• Cooper2023.RBelieve s a T = Cooper2023.RelabeledSubtype (s.rbel a) T

def Cooper2023.WantDagger {Agent : Type} (s : InfoState Agent) (a : Agent) (T : Type) : Prop

want†(a, T) (92): a's desires match T.

Equations

• Cooper2023.WantDagger s a T = s.Matches (s.des a) T

def Cooper2023.Worship {E : Type} (s : InfoState E) (dagger : E → E → Type) (a : E) (Q : Quant E) : Prop

worship(a, Q) (75), (81): a's religious beliefs match the quantifier exported over worship†, intentionality and specificity without existence.

Equations

• Cooper2023.Worship s dagger a Q = s.Matches (s.rbel a) (Q (dagger a))

def Cooper2023.WantP {E : Type} (s : InfoState E) (a : E) (P : Ppty E) : Prop

want_P(a, P) (90a): wanting to have a property.

Equations

• Cooper2023.WantP s a P = Cooper2023.WantDagger s a (P a)

def Cooper2023.WantQ {E : Type} (s : InfoState E) (have_ : E → E → Type) (a : E) (Q : Quant E) : Prop

want_Q(a, Q) (90b): wanting a quantifier's worth of things is wanting to have them.

Equations

• Cooper2023.WantQ s have_ a Q = Cooper2023.WantDagger s a (Q (have_ a))

Hesperus and Phosphorus, (52)–(53)

structure Cooper2023.TwoStars (E : Type) (Hesperus Phosphorus Evening Morning : E → Type) : Type

The ancients' long-term memory (52): a body named Hesperus rising in the evening and a body named Phosphorus rising in the morning.

• x : E
• c₁ : Hesperus self.x
• e₁ : Evening self.x
• y : E
• c₂ : Phosphorus self.y
• e₂ : Morning self.y

structure Cooper2023.OneStar (E : Type) (Hesperus Phosphorus Evening Morning : E → Type) extends Cooper2023.TwoStars E Hesperus Phosphorus Evening Morning : Type

After learning that they are one body (53): the manifest field, a subtype of (52) by the projection toTwoStars.

• x : E
• c₁ : Hesperus self.x
• e₁ : Evening self.x
• y : E
• c₂ : Phosphorus self.y
• e₂ : Morning self.y
• same : self.y = self.x

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

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

A transitive verb whose predicate takes a quantifier (64), with the variant p† between individuals.

• pred : E → Quant E → Type

  The ptype of the verb over an individual and a quantifier.

• dagger : E → E → Type

  The variant p† over two individuals.

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

(65): an extensional verb's 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))

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

(66): a successful search is a finding.

• successful : Type → Type

  The ptype of an event's success.

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

  The subtyping successful(seek(a, Q)) ⊑ find(a, Q).

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

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

Equations

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

Restrictive against inclusive necessity

Two possibilities over the types rain and snow: snow is witnessed only in the first, so it is possible but not necessary; and when snow does not occur in the second at all, it is inclusively but not restrictively necessary, so the entailment of §6.3 does not reverse.

inductive Cooper2023.Weather.Ty : Type

The types.

• 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

The objects.

• 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 Bool 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 Bool 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

Witness-based quantification (Ch. 7)

A property may be restricted by conditions in its domain beyond the required x-field, (7b), and purification lowers the restriction into the body existentially, 𝔓 (12), or universally, 𝔓∀ (13). The cardinality conditions on witness sets (20)–(35) have frequentist probabilistic forms (41)–(58), estimable from an agent's experience base of remembered judgements (37)–(40). The particular witness conditions for exist (63) and no (70) are types equivalent to the general ones (59) whose witnesses carry what discourse anaphora picks up.

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

A restricted property (7b): conditions on the individual in the domain, and the body.

• restr : E → Type

  The restriction: the conditions the domain places on the individual.

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

  The body: the type returned for an individual meeting the restriction.

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): the restriction lowered 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): 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

Alignment of paths in the domain (Ch. 8, (51)–(52)): a manifest field identifying two paths 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)): the domain narrowed by a property, the alignment 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: 𝔓 and 𝔓∀ differ only under a non-trivial restriction.

Witness sets and probabilities (§7.3)

def Cooper2023.condProb {E : Type} [DecidableEq E] (A B : Finset E) : ℚ

The frequentist conditional probability (36) of one extension given another, 0 when the condition is unwitnessed.

Equations

• Cooper2023.condProb A B = ↑(A ∩ B).card / ↑B.card

theorem Cooper2023.condProb_of_subset {E : Type} [DecidableEq E] {X P : Finset E} (h : X ⊆ P) : condProb X P = ↑X.card / ↑P.card

(51)–(52): for a witness set X of objects with the property, the probability of 𝔗(X) given 𝔗(P) is the proportion |X| / |[↓P]|.

theorem Cooper2023.isMostW_iff {E : Type} [Fintype E] [DecidableEq E] {P : E → Prop} [DecidablePred P] {θ_num θ_denom : ℕ} (hθ : 0 < θ_denom) {X : Finset E} (hX : Quantification.WitnessSet P X) (hP : 0 < (Quantification.fullExtFinset P).card) : Quantification.IsMostW P θ_num θ_denom X ↔ ↑θ_num / ↑θ_denom ≤ condProb X (Quantification.fullExtFinset P)

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

@[reducible, inline]

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

An experience base (37): 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).

Equations

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

def Cooper2023.ExperienceBase.estimate {E Ty : Type} [DecidableEq E] [DecidableEq Ty] (𝔍 : ExperienceBase E Ty) (T₁ T₂ : Ty) : ℚ

The estimate p_𝔍(T₁ ‖ T₂) (39) of the probability (36) from the experience base.

Equations

• 𝔍.estimate T₁ T₂ = Cooper2023.condProb (𝔍.extension T₁) (𝔍.extension T₂)

Witness conditions and anaphora (§7.4)

With dog' and bark' the properties (61a–b), a witness for exist(dog', bark') under the particular condition (63) is a dog that barks, whose x-field is what it picks up in A dog is barking. It is right outside my window (64); under the particular condition for no (70), No dog barked. They were all busy gnawing on a bone (71) has they pick up the witness set of every dog, complement set anaphora; and under the general condition for most (74), they in (75) picks up the witness set of most dogs. The properties are decidable predicates lifted to types, as the set-based conditions require.

inductive Cooper2023.Dogs.Ind : Type

The individuals.

• 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 ⋯

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.instReprInd : Repr Ind

Equations

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

@[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 }

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

Fido, Rex and Spot are dogs.

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

Fido and Spot bark.

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).

Equations

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

def Cooper2023.Dogs.bark : Ppty Ind

The property bark' (61b).

Equations

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

def Cooper2023.Dogs.aDogBarks : SemIndefArt dog bark

A dog barks (63): 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)

No dog barks is false: Fido is a dog that barks.

def Cooper2023.Dogs.mostDogsBark : Quantification.GeneralWC_Incr dog bark (Quantification.IsMostW IsDog 1 2)

Most dogs bark (74): the witness set of Fido and Spot, more than half of the dogs, each barking, which they picks up in (75).

Equations

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

theorem Cooper2023.Dogs.mostDogsBark_condProb : 1 / 2 ≤ condProb mostDogsBark.X (Quantification.fullExtFinset IsDog)

(50): the same witness set by its probability, two thirds of the dogs.

inductive Cooper2023.Dogs.Ty : Type

The types judged.

• 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 : experience.estimate Ty.bark Ty.dog = 2 / 3

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

Type-based underspecification (Ch. 8)

The content of an utterance is raised to a type of contents, the readings being the closure of the compositional content under the operations of this section. Storage puts a parametric quantifier into the context's store, leaving in its place the content of a label's value (17), and retrieval quantifies it back in over the content as a property of that value (19). Anaphoric combination identifies a pronoun's label with an antecedent's (28) unless the pronoun is marked local, the marking cleared at the sentence boundary (77); reflexives are marked (83), bound by reflexivisation (84) and required to be bound at the verb phrase (85)–(88). Donkey anaphora goes through localisation (49), which folds the context into the property's domain so that the indefinite's witness in the restrictor can be aligned with the pronoun (51)–(52); 𝔓 then gives the weak reading (55)–(59) and 𝔓∀ the strong one (60)–(66), quantifying over farmers and not farmer–donkey pairs.

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

structure Cooper2023.CntxtType : Type

A context type (§4.3, (16); §8.3, (82)): the labels a content requires the context to assign to stored quantifiers, 𝔮, and to pronouns, 𝔰, and among the latter those marked local, 𝔩, and reflexive, 𝔯.

• stored : Finset ℕ

  The labels of stored quantifiers, 𝔮.

• pronouns : Finset ℕ

  The labels of pronouns, 𝔰.

• locals : Finset ℕ

  The labels of pronouns marked local, 𝔩.

• reflexives : Finset ℕ

  The labels of reflexives, 𝔯.

def Cooper2023.instDecidableEqCntxtType.decEq (x✝ x✝¹ : CntxtType) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Cooper2023.instDecidableEqCntxtType : DecidableEq CntxtType

Equations

• Cooper2023.instDecidableEqCntxtType = Cooper2023.instDecidableEqCntxtType.decEq

@[instance_reducible]

instance Cooper2023.CntxtType.instMax : Max CntxtType

The merge of two context types.

Equations

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

@[instance_reducible]

instance Cooper2023.CntxtType.instBot : Bot CntxtType

The context type requiring nothing.

Equations

• Cooper2023.CntxtType.instBot = { bot := { stored := ∅, pronouns := ∅, locals := ∅, reflexives := ∅ } }

def Cooper2023.CntxtType.erase (T : CntxtType) (i : ℕ) : CntxtType

T ⊖ xᵢ (18): the label removed from every field.

Equations

• T.erase i = { stored := T.stored.erase i, 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 u_1

A parametric content (14) over the contexts of Ch. 8, assignments of individuals to labels: its background context type and its foreground, a content for each assignment.

• bg : CntxtType

  The background: the context type the content requires.

• fg : (ℕ → E) → C

  The foreground: the content under each assignment.

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 α @ β of a functor content to an argument, the backgrounds merged.

Equations

• α.app β = { bg := α.bg ⊔ β.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

The content given a value for a label, 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.store {E : Type} (i : ℕ) : Content E (Quant E)

Storage (17): a stored quantifier leaves in its place the content of its label's value, required of the store and of the pronoun assignment.

Equations

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

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

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

Equations

• Cooper2023.Content.pronoun i = { bg := { stored := ∅, 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): the content of its label's value, marked reflexive.

Equations

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

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

Retrieval (19): the stored quantifier takes scope over the content as a property of the label's value, the label discharged.

Equations

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

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

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

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 ∧ j ∉ β.bg.stored ∧ 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): 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): the local marking is cleared at the sentence.

Equations

• α.boundary = { bg := have __src := α.bg; { stored := __src.stored, 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): the reflexive i is bound to the property's argument, its label discharged and all reflexive marking cleared.

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): a content with a reflexive still marked is excluded at the verb phrase (88).

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))

Two boys each hugging a different dog: the reading (1a) with the quantifiers in surface order is witnessed, and the reading (1b), the object quantifier stored and retrieved over the sentence, is not.

inductive Cooper2023.Hugging.Ind : Type

The individuals.

• 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

Tom and Bill are boys.

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

Fido and Rex are dogs.

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

Tom hugs Fido, Bill hugs Rex.

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)

every boy, requiring nothing of the context.

Equations

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

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

a dog, requiring nothing of the context.

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, 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

(1a): 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

(1b): the object quantifier stored (17) and retrieved (19) over the sentence.

Equations

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

theorem Cooper2023.Hugging.surface_bg : surface.bg = ⊥

Neither reading depends on the context.

theorem Cooper2023.Hugging.inverse_bg : inverse.bg = ⊥

Retrieval discharges what storage required.

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

(1a) is witnessed: every boy is such that there is a dog he hugged.

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)

(1b) is not: there is no dog every boy hugged.

Localisation and donkey anaphora (§8.3)

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

Localisation ℒ (49): the context a parametric property requires is folded into the property's domain under the label 𝔠, giving a restricted property.

Equations

• Cooper2023.localize P = { restr := fun (x : E) => P.bg, body := fun (x : E) (c : P.bg) => P.fg c x }

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

The scope is the localised catches it restricted by the restrictor and aligned so that the caught cat is the chased one (50)–(51); under the particular condition for no the sentence (55) says that every dog which chases a cat fails to be a dog which chases a cat and catches it.

inductive Cooper2023.Chasing.Ind : Type

The individuals.

• 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

The dogs.

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

The cats.

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

Each dog chases one cat.

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.catchesIt (Catch : Ind → Ind → Type) : PPpty Ind

catches it (47): the pronoun's referent supplied by the context.

Equations

• Cooper2023.Chasing.catchesIt Catch = { bg := Cooper2023.Chasing.Ind, fg := fun (y x : Cooper2023.Chasing.Ind) => Catch x y }

def Cooper2023.Chasing.DogChasesACat : Ppty Ind

dog which chases a cat, the restrictor, as the domain of (50): 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): catches it localised, restricted by the restrictor and aligned so that it 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

(55): 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

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)

False when every dog catches the cat it chases.

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

The localised likes it restricted by farmer who owns a donkey and aligned (65) is the property of being a farmer who owns a donkey and likes that donkey; its purification 𝔓 gives the weak reading, some donkey she owns, and 𝔓∀ (66) the strong one, every donkey she owns, the readings of [Kan94]. A farmer who owns two donkeys and likes one separates them.

inductive Cooper2023.Donkeys.Ind : Type

The individuals.

• 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

The farmers.

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

The donkeys.

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

Each farmer likes one donkey.

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.

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.likesIt : Restricted Ind

likes it (61), localised (62)–(63), restricted (64) and aligned (65).

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): every farmer who owns a donkey likes 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: the first farmer does not like the second donkey.

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

With the subject stored, its label is available for anaphoric combination with the pronoun of thinks she failed, whose local marking the embedded sentence's boundary has cleared; retrieval then quantifies over the property of being a girl who thinks she failed, (36c). In Sam likes him the pronoun is still marked local when the subject combines, so the combination is undefined, Principle B; likes himself reflexivised is like(x, x), its marking cleared for the verb phrase's filter, which excludes the reflexive left unbound, Principle A.

inductive Cooper2023.Binding.Ind : Type

The individuals.

• 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

Ann is the girl.

Equations

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

inductive Cooper2023.Binding.Fail : Ind → Type

Nobody failed.

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

Sam likes himself.

• mk : Like Ind.sam Ind.sam

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

think(x, T): a thought with the type's witness.

• thought : T

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

Sam (70), requiring nothing of the context.

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)

no girl (33).

Equations

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

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

failed.

Equations

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

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

thinks, over 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, 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)

thinks she failed (31): she failed a sentence, its pronoun 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).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).AnaphoricDefined 0 1 (thinks.app ((Content.pronoun 1).app failed))

Without the boundary of the embedded sentence the pronoun would still be local.

theorem Cooper2023.Binding.noGirlThinksSheFailed (g : ℕ → Ind) : (noGirl.retrieve 0 ((Content.store 0).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)

likes him (69), the pronoun marked local.

Equations

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

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

(72)–(73): him cannot be related to the stored Sam (71) within the clause, Principle B.

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

likes himself 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

(68c): the reflexivised property is like(x, x).

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

The filter excludes the reflexive left unbound.

def Cooper2023.Binding.samLikesHimself (g : ℕ → Ind) : (sam.retrieve 0 ((Content.store 0).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 identified with the man of the previous utterance's witness (42) and the dependency on the label replaced by one on the man (43)–(44).

inductive Cooper2023.Whistling.Ind : Type

The individuals.

• 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

John is a man.

Equations

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

def Cooper2023.Whistling.Walk : Ppty Ind

John walks.

Equations

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

def Cooper2023.Whistling.Whistle : Ppty Ind

John whistles.

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 under the particular condition for exist (38).

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): the pronoun's label required 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 = ⊥ ∧ (heWhistled.given 0 w.x).fg g = Whistle w.x

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

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

The man of the previous utterance whistled.

Equations

• Cooper2023.Whistling.heWhistledWitness g = PUnit.unit

The book's examples

A selection of the English examples of Chs. 3, 6, 7 and 8 are the rows of Data/Examples/Cooper2023.json. The rows with a quantifier feature are the discourse-anaphora examples of §7.4, §7.4.1 and §8.3, each reading named by the anaphora set the pronoun picks up.

def Cooper2023.quantNames : List (String × Quantification.QuantName)

The quantifier relation a row's determiner names.

Equations

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

def Cooper2023.anaphoraRefs : List (String × Quantification.AnaphoraRef)

The anaphora set a reading names.

Equations

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

theorem Cooper2023.anaphora_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → ∀ v ∈ row.feature? "quantifier", ∃ q ∈ List.lookup v quantNames, ∀ r ∈ row.readings, ∃ ref ∈ List.lookup r.1 anaphoraRefs, r.2 = Features.Judgment.acceptable ↔ ref ∈ Quantification.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.