@[reducible, inline]

abbrev Semantics.Dynamic.PLA.GQRel (α : Type u_1) : Type u_1

A Generalized quantifier relation: determines truth based on two sets.

GQRel α = Set α → Set α → Prop

Examples:

• every A B = A ⊆ B
• some A B = (A ∩ B).Nonempty
• no A B = A ∩ B = ∅

Equations

• Semantics.Dynamic.PLA.GQRel α = (Set α → Set α → Prop)

def Semantics.Dynamic.PLA.GQRel.every {α : Type u_1} : GQRel α

Every: All A's are B's

Equations

• Semantics.Dynamic.PLA.GQRel.every A B = (A ⊆ B)

def Semantics.Dynamic.PLA.GQRel.some {α : Type u_1} : GQRel α

Some: At least one A is a B

Equations

• Semantics.Dynamic.PLA.GQRel.some A B = (A ∩ B).Nonempty

def Semantics.Dynamic.PLA.GQRel.no {α : Type u_1} : GQRel α

No: No A is a B

Equations

• Semantics.Dynamic.PLA.GQRel.no A B = (A ∩ B = ∅)

def Semantics.Dynamic.PLA.GQRel.most {α : Type u_1} [Fintype α] : GQRel α

Most: More than half of the A's are B's (requires finite)

Equations

• Semantics.Dynamic.PLA.GQRel.most A B = (2 * ⋯.toFinset.card > ⋯.toFinset.card)

def Semantics.Dynamic.PLA.GQRel.atLeast {α : Type u_1} (n : ℕ) : GQRel α

At least n: At least n A's are B's

Equations

• Semantics.Dynamic.PLA.GQRel.atLeast n A B = ∃ (s : Finset α), s.card ≥ n ∧ ↑s ⊆ A ∩ B

def Semantics.Dynamic.PLA.GQRel.exactly {α : Type u_1} [Fintype α] (n : ℕ) : GQRel α

Exactly n: Exactly n A's are B's

Equations

• Semantics.Dynamic.PLA.GQRel.exactly n A B = (⋯.toFinset.card = n)

def Semantics.Dynamic.PLA.GQRel.IsConservative {α : Type u_1} (D : GQRel α) : Prop

A quantifier is conservative if D(A)(B) ↔ D(A)(A ∩ B).

This is the key semantic universal: determiners only care about the A's when determining the relation to B.

"Every student passed" ↔ "Every student is a student who passed"

Equations

• D.IsConservative = ∀ (A B : Set α), D A B ↔ D A (A ∩ B)

theorem Semantics.Dynamic.PLA.GQRel.every_conservative {α : Type u_1} : every.IsConservative

theorem Semantics.Dynamic.PLA.GQRel.some_conservative {α : Type u_1} : some.IsConservative

theorem Semantics.Dynamic.PLA.GQRel.no_conservative {α : Type u_1} : no.IsConservative

def Semantics.Dynamic.PLA.GQRel.IsUpwardMono {α : Type u_1} (D : GQRel α) : Prop

A quantifier is upward monotone in the second argument if D(A)(B) and B ⊆ C implies D(A)(C).

Equations

• D.IsUpwardMono = ∀ (A B C : Set α), B ⊆ C → D A B → D A C

def Semantics.Dynamic.PLA.GQRel.IsDownwardMono {α : Type u_1} (D : GQRel α) : Prop

A quantifier is downward monotone in the second argument if D(A)(B) and C ⊆ B implies D(A)(C).

Equations

• D.IsDownwardMono = ∀ (A B C : Set α), C ⊆ B → D A B → D A C

theorem Semantics.Dynamic.PLA.GQRel.every_upward_mono {α : Type u_1} : every.IsUpwardMono

theorem Semantics.Dynamic.PLA.GQRel.some_upward_mono {α : Type u_1} : some.IsUpwardMono

theorem Semantics.Dynamic.PLA.GQRel.no_downward_mono {α : Type u_1} : no.IsDownwardMono

def Semantics.Dynamic.PLA.GQRel.IsTruthful {α : Type u_1} (D : GQRel α) : Prop

A quantifier is truthful (has existential import) if D(A)(B) implies A ∩ B ≠ ∅.

Truthful quantifiers: some, every (presuppositionally), most Non-truthful: no, at most n

Equations

• D.IsTruthful = ∀ (A B : Set α), D A B → (A ∩ B).Nonempty

theorem Semantics.Dynamic.PLA.GQRel.some_truthful {α : Type u_1} : some.IsTruthful

theorem Semantics.Dynamic.PLA.GQRel.every_not_truthful {α : Type u_1} : ¬every.IsTruthful

Note: every is only truthful if we assume existential presupposition. Standard logic treats "every A is B" as vacuously true when A = ∅.

Bridge to Quantification

PLA's GQRel α = Set α → Set α → Prop and Core's GQ α = (α → Prop) → (α → Prop) → Prop carry the same content (Set α is defined as α → Prop). The property predicates align via the A ∩ B = {x | A x ∧ B x} set-vs-predicate shift. toCoreGQ is the canonical bridge; the bridges below let PLA consumers cash in Core's [BC81] / [PW06] / [vB84] theorems instead of reproving them.

def Semantics.Dynamic.PLA.GQRel.toCoreGQ {α : Type u_1} (D : GQRel α) : Quantification.GQ α

Bridge: a GQRel viewed as a Quantification.GQ.

Equations

• D.toCoreGQ R S = D (setOf R) (setOf S)

theorem Semantics.Dynamic.PLA.GQRel.isConservative_iff_Core_Conservative {α : Type u_1} (D : GQRel α) : D.IsConservative ↔ Quantification.Conservative D.toCoreGQ

A GQRel is conservative iff its Core.GQ projection is.

theorem Semantics.Dynamic.PLA.GQRel.isUpwardMono_iff_Core_ScopeUpwardMono {α : Type u_1} (D : GQRel α) : D.IsUpwardMono ↔ Quantification.ScopeUpwardMono D.toCoreGQ

A GQRel is scope-upward-monotone iff its Core.GQ projection is.

theorem Semantics.Dynamic.PLA.GQRel.isDownwardMono_iff_Core_ScopeDownwardMono {α : Type u_1} (D : GQRel α) : D.IsDownwardMono ↔ Quantification.ScopeDownwardMono D.toCoreGQ

A GQRel is scope-downward-monotone iff its Core.GQ projection is.

theorem Semantics.Dynamic.PLA.GQRel.toCoreGQ_every {α : Type u_1} : every.toCoreGQ = Quantification.every_sem

GQRel.every projects to Quantification.every_sem.

theorem Semantics.Dynamic.PLA.GQRel.toCoreGQ_some {α : Type u_1} : some.toCoreGQ = Quantification.some_sem

GQRel.some projects to Quantification.some_sem.

theorem Semantics.Dynamic.PLA.GQRel.toCoreGQ_no {α : Type u_1} : no.toCoreGQ = Quantification.no_sem

GQRel.no projects to Quantification.no_sem.

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.WitnessFn (α : Type u_1) : Type u_1

A witness function selects, for each entity in the restrictor satisfying some condition, a witnessing entity.

For "Every farmer who owns a donkey beats it":

• For each farmer f who owns a donkey, wit f is a donkey that f owns

This is [Dek12]'s solution to donkey anaphora with universal quantifiers.

Equations

• Semantics.Dynamic.PLA.WitnessFn α = (α → α)

def Semantics.Dynamic.PLA.ValidWitness {α : Type u_1} (R : α → α → Prop) (A B : Set α) (wit : WitnessFn α) : Prop

A witness function is valid for sets A and R if: for all x ∈ A, the witness wit(x) is related to x by R.

For "owns a donkey": valid_witness owns farmers donkeys wit means ∀ f ∈ farmers, owns f (wit f) ∧ wit f ∈ donkeys

Equations

• Semantics.Dynamic.PLA.ValidWitness R A B wit = ∀ x ∈ A, R x (wit x) ∧ wit x ∈ B

theorem Semantics.Dynamic.PLA.truthful_has_witness {α : Type u_1} [Nonempty α] (D : GQRel α) (hT : D.IsTruthful) (A B : Set α) (h : D A B) : ∃ x ∈ A ∩ B, True

Truthful existence: For truthful quantifiers, if D(A)(B) holds, there exists a valid witness function.

This is the key to dynamic binding: truthful quantifiers "export" witnesses that can be referenced anaphorically.

def Semantics.Dynamic.PLA.Formula.gqUpdate {E : Type u_1} [Nonempty E] (M : Model E) (D : GQRel E) (x : VarIdx) (φ ψ : Formula) : Update E

Dynamic quantifier update: Dx(φ)(ψ) where D is a generalized quantifier.

Semantics: D(restrictor)(scope) where:

• restrictor = {e | M, g[x↦e], ê ⊨ φ}
• scope = {e | M, g[x↦e], ê ⊨ ψ}

This generalizes ∃x.φ (which is some(univ)(φ)).

Equations

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

theorem Semantics.Dynamic.PLA.exists_as_gq {E : Type u_1} [Nonempty E] (M : Model E) (x : VarIdx) (φ : Formula) (s : InfoState E) : Formula.update M (Formula.exists_ x φ) s = {p : Assignment E × WitnessSeq E | p ∈ s ∧ ∃ (e : E), Formula.sat M (p.1[x ↦ e]) p.2 φ}

Standard existential is some(univ)(φ), but we use the standard definition which also updates the assignment.

def Semantics.Dynamic.PLA.Formula.forallGQ {E : Type u_1} [Nonempty E] (M : Model E) (x : VarIdx) (φ : Formula) : Update E

Universal quantifier as GQ: ∀x.φ = every(univ)(φ)

Equations

• Semantics.Dynamic.PLA.Formula.forallGQ M x φ = Semantics.Dynamic.PLA.Formula.gqUpdate M Semantics.Dynamic.PLA.GQRel.every x (Semantics.Dynamic.PLA.Formula.atom "⊤" []) φ

def Semantics.Dynamic.PLA.donkeyUpdate {E : Type u_1} (M : Model E) (farmer donkey : VarIdx) (pron_it : PronIdx) (owns beats : String) : Update E

Donkey update: For "Every farmer who owns a donkey beats it".

This captures the dependency between the universally quantified farmer and the existentially introduced donkey.

We need to track, for each farmer f, which donkey witnesses the "owns a donkey" part, and that donkey is what "it" refers to.

Equations

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

def Semantics.Dynamic.PLA.etypeApproach {E : Type u_1} (M : Model E) (farmer donkey owns beats : String) : Prop

The E-type approach (Evans): pronouns pick out the unique/salient entity.

For "Every farmer who owns a donkey beats it": "it" = the unique donkey that the farmer owns (if unique), or a contextually salient one (if multiple).

This differs from the witness-function approach in requiring uniqueness or salience.

Equations

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

theorem Semantics.Dynamic.PLA.gqUpdate_eliminative {E : Type u_1} [Nonempty E] (M : Model E) (D : GQRel E) (x : VarIdx) (φ ψ : Formula) (s : InfoState E) : Formula.gqUpdate M D x φ ψ s ⊆ s

GQ updates are eliminative: They never add possibilities.

theorem Semantics.Dynamic.PLA.gqUpdate_conservative {E : Type u_1} [Nonempty E] (M : Model E) (D : GQRel E) (hC : D.IsConservative) (x : VarIdx) (φ ψ : Formula) (s : InfoState E) (p : Poss E) : p ∈ Formula.gqUpdate M D x φ ψ s ↔ p ∈ s ∧ D {e : E | Formula.sat M (p.1[x ↦ e]) p.2 φ} {e : E | Formula.sat M (p.1[x ↦ e]) p.2 φ ∧ Formula.sat M (p.1[x ↦ e]) p.2 ψ}

Conservativity transfers: If D is conservative, so is the dynamic version (in a suitable sense).

theorem Semantics.Dynamic.PLA.indefinite_wide_scope {E : Type u_1} [Nonempty E] (M : Model E) (x : VarIdx) (φ ψ : Formula) (s : InfoState E) (p : Poss E) : p ∈ Formula.update M (Formula.exists_ x φ) s → ∃ (e : E), Formula.sat M (p.1[x ↦ e]) p.2 φ

Indefinites take wide scope (in dynamic semantics).

"If a farmer owns a donkey, he beats it." The indefinites "a farmer" and "a donkey" can bind pronouns in the consequent.

This is modeled by having the existential update extend the assignment globally, not just locally.

theorem Semantics.Dynamic.PLA.universal_no_export {E : Type u_1} [Nonempty E] (M : Model E) (x : VarIdx) (φ : Formula) (s : InfoState E) : Formula.forallGQ M x φ s ⊆ s

Universals don't export: "Every farmer owns a donkey" doesn't make "the donkey" available for subsequent anaphora (without special mechanisms).