Elliott (2020): Towards a principled logic of anaphora

In Elliott's Dynamic Alternative Semantics a sentence maps a partial assignment to pairs of a strong Kleene truth value and an output assignment. Each connective lifts its strong Kleene truth function, passing assignments from left to right, and an existential is the positive closure of the DPL existential, which keeps the true outputs and otherwise returns the input. The DPL existential is a random reset bound to its scope, but positive closure is not a bind, so the existential is not monadic in Charlow's sense. Negation swaps the positive and negative outputs, so double negation and de Morgan's laws hold, bathroom sentences and Stone disjunctions license anaphora, and updating a set of world–assignment pairs makes a disjunction look externally static until one disjunct is ruled out.

Main statements

• neg_neg, neg_disj, neg_conj: double negation and de Morgan's laws as equations.
• not_exists_bind_eq_positiveClosure: positive closure is not a bind.
• egli, not_egli_negative: Egli's theorem for positive extensions, and its failure for negative ones.
• extension_true_bathroom, familiar_update_stone: anaphora in bathroom sentences and Stone disjunctions.
• not_familiar_update_disj, familiar_update_update_disj: the apparent external staticity of disjunction and Rothschild's observation.

Implementation notes

• A sentence denotes a StateSet D SignType, a map from assignments to sets of truth value and output pairs (Def. A.1), as in the paper's appendix; there is no syntax. Its relation at 1 (StateT.rel) is the positive extension as a DPL relation. Atoms are monadic, and a constant atom is pure of its truth value.
• The existentials of Defs. 2.3 and 3.3 are one definition with a parameter; the destructive one overwrites a valued variable, and the guarded one is undefined there.
• Every output values what its input values (Expanding), for both existentials; the familiarity results rest on it.
• The dynamic Hurford constraint (70) is read as validity, over every model and input. Read pointwise, it would mark every disjunction with a bivalent first disjunct odd.

TODO

The paper says (70) rules out (65) and rules in bathroom sentences. Neither existential does both. With the guarded one, (65) and the bathroom sentence are both odd (hurfordOdd_someone_or_they, hurfordOdd_bathroom); with the destructive one, neither is (not_hurfordOdd_someone_or_they_destructive, not_hurfordOdd_bathroom_destructive).

The universal readings of App. B, by innocent inclusion over subdomain alternatives, are not formalized.

References

• [Ell20b]
• [GS91a]
• [Cha14b]
• [Bea01]
• [vdB96]
• [Rot17a]
• [Sto92]

Dynamic propositions

@[reducible, inline]

abbrev Elliott2020.StateSet (D α : Type) : Type

The State.Set applicative over partial assignments (Def. A.3).

Equations

• Elliott2020.StateSet D = StateT (PartialAssign ℕ D) Set

Atomic sentences

noncomputable def Elliott2020.valueAt {D : Type} (P : Set D) (g : PartialAssign ℕ D) (n : ℕ) : SignType

The value of P n at g, ∂ (n ∈ dom g) ∧ gₙ ∈ P, with Beaver's ∂ and a weak Kleene conjunction (Def. 2.2 and fn. 10).

Equations

• Elliott2020.valueAt P g n = (max (SignType.ofProp (g n ≠ ⊥)) 0).meetWeak (SignType.ofProp (∃ (d : D), g n = ↑d ∧ d ∈ P))

@[simp]

theorem Elliott2020.valueAt_of_eq_bot {D : Type} (P : Set D) {g : PartialAssign ℕ D} {n : ℕ} (h : g n = ⊥) : valueAt P g n = 0

@[simp]

theorem Elliott2020.valueAt_of_eq_coe {D : Type} (P : Set D) {g : PartialAssign ℕ D} {n : ℕ} {d : D} (h : g n = ↑d) : valueAt P g n = SignType.ofProp (d ∈ P)

noncomputable def Elliott2020.atom {D : Type} (P : Set D) (n : ℕ) : StateSet D SignType

A monadic predicate of a variable (Def. 2.2).

Equations

• Elliott2020.atom P n g = {(Elliott2020.valueAt P g n, g)}

noncomputable def Elliott2020.atomConst {D : Type} (P : Set D) (c : D) : StateSet D SignType

A monadic predicate of an individual constant (Def. 2.2), whose value does not depend on the assignment.

Equations

• Elliott2020.atomConst P c = pure (SignType.ofProp (c ∈ P))

@[simp]

theorem Elliott2020.mem_atom {D : Type} {P : Set D} {n : ℕ} {g : PartialAssign ℕ D} {p : SignType × PartialAssign ℕ D} : p ∈ atom P n g ↔ p = (valueAt P g n, g)

@[simp]

theorem Elliott2020.mem_atomConst {D : Type} {P : Set D} {c : D} {g : PartialAssign ℕ D} {p : SignType × PartialAssign ℕ D} : p ∈ atomConst P c g ↔ p = (SignType.ofProp (c ∈ P), g)

Connectives

Each connective lifts its strong Kleene truth function, passing the output of its first argument to its second (Def. 2.9); in the applicative a binary one is η R ⊛ m ⊛ n (Def. A.3).

def Elliott2020.neg {D : Type} (m : StateSet D SignType) : StateSet D SignType

Negation lifts strong Kleene negation (Def. 2.4).

Equations

• Elliott2020.neg m = Neg.neg <$> m

def Elliott2020.conj {D : Type} (m n : StateSet D SignType) : StateSet D SignType

Conjunction lifts strong Kleene conjunction (Def. 2.10).

Equations

• Elliott2020.conj m n = (fun (x1 x2 : SignType) => min x1 x2) <$> m <*> n

def Elliott2020.disj {D : Type} (m n : StateSet D SignType) : StateSet D SignType

Disjunction lifts strong Kleene disjunction (Def. 2.11).

Equations

• Elliott2020.disj m n = (fun (x1 x2 : SignType) => max x1 x2) <$> m <*> n

def Elliott2020.imp {D : Type} (m n : StateSet D SignType) : StateSet D SignType

Material implication lifts strong Kleene ¬t ∨ u (§2.9).

Equations

• Elliott2020.imp m n = (fun (t u : SignType) => max (-t) u) <$> m <*> n

Extensions and truth

def Elliott2020.extension {D : Type} (v : SignType) (m : StateSet D SignType) (g : PartialAssign ℕ D) : Set (PartialAssign ℕ D)

extension v m g is the set of outputs of m at g tagged v; at 1, (-1) and 0 these are the positive, negative and maybe extensions (Def. 2.5).

Equations

• Elliott2020.extension v m g = {h : PartialAssign ℕ D | (v, h) ∈ m g}

@[simp]

theorem Elliott2020.mem_extension {D : Type} {v : SignType} {m : StateSet D SignType} {g h : PartialAssign ℕ D} : h ∈ extension v m g ↔ (v, h) ∈ m g

def Elliott2020.IsTrue {D : Type} (m : StateSet D SignType) (g : PartialAssign ℕ D) : Prop

m is true at g when its positive extension is nonempty (Def. 2.6).

Equations

• Elliott2020.IsTrue m g = (Elliott2020.extension 1 m g).Nonempty

def Elliott2020.IsFalse {D : Type} (m : StateSet D SignType) (g : PartialAssign ℕ D) : Prop

m is false at g when it has no positive output and some negative one (Def. 2.6).

Equations

• Elliott2020.IsFalse m g = (Elliott2020.extension 1 m g = ∅ ∧ (Elliott2020.extension (-1) m g).Nonempty)

def Elliott2020.IsIndet {D : Type} (m : StateSet D SignType) (g : PartialAssign ℕ D) : Prop

m is maybe at g when all its outputs are tagged maybe (Def. 2.6).

Equations

• Elliott2020.IsIndet m g = (Elliott2020.extension 1 m g = ∅ ∧ Elliott2020.extension (-1) m g = ∅ ∧ (Elliott2020.extension 0 m g).Nonempty)

theorem Elliott2020.isTrue_or_isFalse_iff {D : Type} {m : StateSet D SignType} {g : PartialAssign ℕ D} : IsTrue m g ∨ IsFalse m g ↔ (extension 1 m g).Nonempty ∨ (extension (-1) m g).Nonempty

m is true or false at g when it has a positive or a negative output, the condition Stalnaker's bridge puts on every point of a state (Def. 3.2).

theorem Elliott2020.rel_neg {D : Type} (v : SignType) (m : StateSet D SignType) : StateT.rel (neg m) v = StateT.rel m (-v)

theorem Elliott2020.extension_neg {D : Type} (v : SignType) (m : StateSet D SignType) (g : PartialAssign ℕ D) : extension v (neg m) g = extension (-v) m g

Negation permutes the extensions by strong Kleene negation (Obs. 2.1).

theorem Elliott2020.neg_neg {D : Type} (m : StateSet D SignType) : neg (neg m) = m

Double negation is the identity (Obs. 2.2).

theorem Elliott2020.neg_disj {D : Type} (m n : StateSet D SignType) : neg (disj m n) = conj (neg m) (neg n)

de Morgan's law for disjunction (Obs. 2.6).

theorem Elliott2020.neg_conj {D : Type} (m n : StateSet D SignType) : neg (conj m n) = disj (neg m) (neg n)

de Morgan's law for conjunction (Obs. 2.6).

theorem Elliott2020.imp_eq_disj_neg {D : Type} (m n : StateSet D SignType) : imp m n = disj (neg m) n

Material implication is the disjunction of the negated antecedent with the consequent.

Existential quantification

inductive Elliott2020.Existential : Type

A DPL existential either overwrites a valued variable, as in Def. 2.3, or is undefined there, as in Def. 3.3.

• destructive : Existential

  The existential of Def. 2.3 resets the variable whether or not it is valued.

• guarded : Existential

  The existential of Def. 3.3 resets only an unvalued variable.

@[instance_reducible]

instance Elliott2020.instDecidableEqExistential : DecidableEq Existential

Equations

• Elliott2020.instDecidableEqExistential x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Elliott2020.instReprExistential : Repr Existential

Equations

• Elliott2020.instReprExistential = { reprPrec := Elliott2020.instReprExistential.repr }

def Elliott2020.instReprExistential.repr : Existential → ℕ → Std.Format

Equations

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

def Elliott2020.Existential.Fresh {D : Type} : Existential → PartialAssign ℕ D → ℕ → Prop

When an existential may reset n at g.

Equations

• Elliott2020.Existential.destructive.Fresh x✝¹ x✝ = True
• Elliott2020.Existential.guarded.Fresh x✝¹ x✝ = (x✝¹ x✝ = ⊥)

@[simp]

theorem Elliott2020.Existential.fresh_destructive {D : Type} (g : PartialAssign ℕ D) (n : ℕ) : destructive.Fresh g n

@[simp]

theorem Elliott2020.Existential.fresh_guarded_iff {D : Type} (g : PartialAssign ℕ D) (n : ℕ) : guarded.Fresh g n ↔ g n = ⊥

def Elliott2020.dplExists {D : Type} (e : Existential) (n : ℕ) (m : StateSet D SignType) : StateSet D SignType

The DPL existential takes the union of m over the resets of n when it may reset n, and is maybe otherwise (Defs. 2.3 and 3.3).

Equations

• Elliott2020.dplExists e n m g = {p : SignType × PartialAssign ℕ D | e.Fresh g n ∧ ∃ (x : D), p ∈ m (g.update n x)} ∪ {p : SignType × PartialAssign ℕ D | ¬e.Fresh g n ∧ p = (0, g)}

def Elliott2020.positiveClosure {D : Type} (m : StateSet D SignType) : StateSet D SignType

Positive closure keeps the true outputs, or else returns the input tagged false or maybe (Def. 2.7).

Equations

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

def Elliott2020.exists_ {D : Type} (e : Existential) (n : ℕ) (m : StateSet D SignType) : StateSet D SignType

Existential quantification, the positive closure of the DPL existential (Def. 2.8).

Equations

• Elliott2020.exists_ e n m = Elliott2020.positiveClosure (Elliott2020.dplExists e n m)

@[simp]

theorem Elliott2020.mem_dplExists {D : Type} {e : Existential} {n : ℕ} {m : StateSet D SignType} {g : PartialAssign ℕ D} {p : SignType × PartialAssign ℕ D} : p ∈ dplExists e n m g ↔ (e.Fresh g n ∧ ∃ (x : D), p ∈ m (g.update n x)) ∨ ¬e.Fresh g n ∧ p = (0, g)

@[simp]

theorem Elliott2020.mem_positiveClosure {D : Type} {m : StateSet D SignType} {g : PartialAssign ℕ D} {p : SignType × PartialAssign ℕ D} : p ∈ positiveClosure m g ↔ p.1 = 1 ∧ p ∈ m g ∨ IsFalse m g ∧ p = (-1, g) ∨ IsIndet m g ∧ p = (0, g)

@[simp]

theorem Elliott2020.extension_true_positiveClosure {D : Type} (m : StateSet D SignType) (g : PartialAssign ℕ D) : extension 1 (positiveClosure m) g = extension 1 m g

Positive closure keeps the positive extension ((19a)).

theorem Elliott2020.extension_false_positiveClosure {D : Type} (m : StateSet D SignType) (g : PartialAssign ℕ D) : extension (-1) (positiveClosure m) g = {h : PartialAssign ℕ D | IsFalse m g ∧ h = g}

The negative extension of a positive closure is the input, when m is false ((19b)).

theorem Elliott2020.dplExists_neg {D : Type} (e : Existential) (n : ℕ) (m : StateSet D SignType) : dplExists e n (neg m) = neg (dplExists e n m)

The DPL existential and negation commute (Obs. 2.3).

theorem Elliott2020.exists_guarded_of_ne_bot {D : Type} {n : ℕ} {m : StateSet D SignType} {g : PartialAssign ℕ D} (hg : g n ≠ ⊥) : exists_ Existential.guarded n m g = {(0, g)}

A guarded existential over a valued variable is maybe at the input.

The existential and bind

Charlow decomposes the DPL existential into bind applied to a set of alternatives; Elliott's existential is not straightforwardly compatible with that decomposition (App. A). The DPL existential decomposes, a random reset bound to its scope, but positive closure is not a bind.

def Elliott2020.reset {D : Type} (n : ℕ) : StateSet D PUnit.{1}

Random assignment, resetting n to any individual.

Equations

• Elliott2020.reset n g = {q : PUnit.{1} × PartialAssign ℕ D | ∃ (x : D), q = ((), g.update n x)}

theorem Elliott2020.dplExists_destructive {D : Type} (n : ℕ) (m : StateSet D SignType) : dplExists Existential.destructive n m = do reset n m

The destructive DPL existential is a random reset bound to its scope.

theorem Elliott2020.not_exists_bind_eq_positiveClosure {D : Type} : ¬∃ (k : SignType → StateSet D SignType), ∀ (m : StateSet D SignType), positiveClosure m = m >>= k

Positive closure is not a bind, since a bind treats each output separately while closure drops the false outputs exactly when a true one exists (App. A).

Positive extensions and DPL

At 1 the relation a sentence induces (StateT.rel) is its positive extension, a DPL relation between assignments.

theorem Elliott2020.rel_true_conj {D : Type} (m n : StateSet D SignType) : StateT.rel (conj m n) 1 = (StateT.rel m 1).comp (StateT.rel n 1)

The positive extension of a conjunction is the DPL composition of its conjuncts' ((26a)).

theorem Elliott2020.rel_false_disj {D : Type} (m n : StateSet D SignType) : StateT.rel (disj m n) (-1) = (StateT.rel m (-1)).comp (StateT.rel n (-1))

The negative extension of a disjunction is the DPL composition of its disjuncts' ((32b)).

theorem Elliott2020.isTest_rel_true_neg_exists {D : Type} (e : Existential) (n : ℕ) (m : StateSet D SignType) : DynamicSemantics.Update.IsTest (StateT.rel (neg (exists_ e n m)) 1)

A negated existential is a test, by positive closure ((22a)).

theorem Elliott2020.not_isTest_rel_true_neg_dplExists {D : Type} [Nonempty D] : ¬DynamicSemantics.Update.IsTest (StateT.rel (neg (dplExists Existential.destructive 1 (atom ∅ 1))) 1)

A negated DPL existential is not a test, since it resets its variable to the individuals its scope is false of ((18)).

The extensions of the connectives

theorem Elliott2020.mem_extension_true_disj {D : Type} {m n : StateSet D SignType} {g i : PartialAssign ℕ D} : i ∈ extension 1 (disj m n) g ↔ (∃ h ∈ extension 1 m g, ∃ (u : SignType), (u, i) ∈ n h) ∨ ∃ (t : SignType) (h : PartialAssign ℕ D), (t, h) ∈ m g ∧ i ∈ extension 1 n h

An output verifies m ∨ n when m is verified and n has any output from there, or m has any output from which n is verified ((32a)).

theorem Elliott2020.mem_extension_false_disj {D : Type} {m n : StateSet D SignType} {g i : PartialAssign ℕ D} : i ∈ extension (-1) (disj m n) g ↔ ∃ h ∈ extension (-1) m g, i ∈ extension (-1) n h

An output falsifies m ∨ n when it falsifies n after an output falsifying m ((32b)).

theorem Elliott2020.mem_extension_true_imp {D : Type} {m n : StateSet D SignType} {g i : PartialAssign ℕ D} : i ∈ extension 1 (imp m n) g ↔ (∃ h ∈ extension (-1) m g, ∃ (u : SignType), (u, i) ∈ n h) ∨ ∃ (t : SignType) (h : PartialAssign ℕ D), (t, h) ∈ m g ∧ i ∈ extension 1 n h

An output verifies m → n when m is falsified and n has any output from there, or m has any output from which n is verified ((38a)).

theorem Elliott2020.mem_extension_false_conj {D : Type} {m n : StateSet D SignType} {g i : PartialAssign ℕ D} : i ∈ extension (-1) (conj m n) g ↔ (∃ h ∈ extension (-1) m g, ∃ (u : SignType), (u, i) ∈ n h) ∨ ∃ (t : SignType) (h : PartialAssign ℕ D), (t, h) ∈ m g ∧ i ∈ extension (-1) n h

An output falsifies m ∧ n when m is falsified and n has any output from there, or m has any output from which n is falsified ((26b)).

Egli's theorem

theorem Elliott2020.mem_extension_true_conj {D : Type} {m n : StateSet D SignType} {g i : PartialAssign ℕ D} : i ∈ extension 1 (conj m n) g ↔ ∃ h ∈ extension 1 m g, i ∈ extension 1 n h

A conjunction's positive extension, from rel_true_conj.

theorem Elliott2020.egli {D : Type} (e : Existential) (n : ℕ) (m k : StateSet D SignType) (g : PartialAssign ℕ D) : extension 1 (exists_ e n (conj m k)) g = extension 1 (conj (exists_ e n m) k) g

Egli's theorem for positive extensions, for either existential (Obs. 2.4).

Existentials over atoms

theorem Elliott2020.mem_atom_update {D : Type} (W : Set D) {n : ℕ} {g : PartialAssign ℕ D} (x : D) {v : SignType} {h : PartialAssign ℕ D} : (v, h) ∈ atom W n (g.update n x) ↔ v = SignType.ofProp (x ∈ W) ∧ h = g.update n x

theorem Elliott2020.neg_atom {D : Type} (W : Set D) (n : ℕ) : neg (atom W n) = atom Wᶜ n

The negation of an atom is the atom of the complement.

theorem Elliott2020.extension_true_dplExists_atom {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} (hf : e.Fresh g n) : extension 1 (dplExists e n (atom W n)) g = {h : PartialAssign ℕ D | ∃ x ∈ W, h = g.update n x}

The positive extension of εₙ W n consists of the resets of n to a W ((17a)).

theorem Elliott2020.extension_false_dplExists_atom {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} (hf : e.Fresh g n) : extension (-1) (dplExists e n (atom W n)) g = {h : PartialAssign ℕ D | ∃ x ∉ W, h = g.update n x}

The negative extension of εₙ W n consists of the resets of n to a non-W ((17b)).

theorem Elliott2020.extension_indet_dplExists_atom {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} (hf : e.Fresh g n) : extension 0 (dplExists e n (atom W n)) g = ∅

theorem Elliott2020.extension_true_exists_atom {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} (hf : e.Fresh g n) : extension 1 (exists_ e n (atom W n)) g = {h : PartialAssign ℕ D | ∃ x ∈ W, h = g.update n x}

The positive extension of ∃ₙ W n ((20a)).

theorem Elliott2020.isFalse_dplExists_atom_iff {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} [Nonempty D] (hf : e.Fresh g n) : IsFalse (dplExists e n (atom W n)) g ↔ W = ∅

theorem Elliott2020.extension_false_exists_atom {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} [Nonempty D] (hf : e.Fresh g n) : extension (-1) (exists_ e n (atom W n)) g = {h : PartialAssign ℕ D | h = g ∧ W = ∅}

The negative extension of ∃ₙ W n is the input, when nothing is a W.

theorem Elliott2020.extension_true_neg_exists_atom {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} [Nonempty D] (hf : e.Fresh g n) : extension 1 (neg (exists_ e n (atom W n))) g = {h : PartialAssign ℕ D | h = g ∧ W = ∅}

The negation of an existential is a test, whose positive extension is the input when nothing is a W ((22a)).

theorem Elliott2020.extension_false_neg_exists_atom {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} (hf : e.Fresh g n) : extension (-1) (neg (exists_ e n (atom W n))) g = {h : PartialAssign ℕ D | ∃ x ∈ W, h = g.update n x}

The negative extension of ¬ ∃ₙ W n resets n to the Ws, the outputs double negation passes on ((22b)).

theorem Elliott2020.extension_indet_neg_exists_atom {D : Type} (W : Set D) {e : Existential} {n : ℕ} {g : PartialAssign ℕ D} (hf : e.Fresh g n) : extension 0 (neg (exists_ e n (atom W n))) g = ∅

theorem Elliott2020.extension_true_bathroom {D : Type} (B U : Set D) {e : Existential} {g : PartialAssign ℕ D} [Nonempty D] (hf : e.Fresh g 1) : extension 1 (disj (neg (exists_ e 1 (atom B 1))) (atom U 1)) g = {h : PartialAssign ℕ D | h = g ∧ B = ∅} ∪ {h : PartialAssign ℕ D | ∃ x ∈ B, x ∈ U ∧ h = g.update 1 x}

The bathroom sentence ¬ ∃₁ B 1 ∨ U 1, either there is no bathroom, or it's upstairs, is verified by the input when there is no bathroom, and by the resets of 1 to the bathrooms upstairs ((35)).

theorem Elliott2020.extension_false_bathroom {D : Type} (B U : Set D) {e : Existential} {g : PartialAssign ℕ D} (hf : e.Fresh g 1) : extension (-1) (disj (neg (exists_ e 1 (atom B 1))) (atom U 1)) g = {h : PartialAssign ℕ D | ∃ x ∈ B, x ∉ U ∧ h = g.update 1 x}

The bathroom sentence is falsified by the resets of 1 to a bathroom that is not upstairs.

theorem Elliott2020.extension_true_donkey {D : Type} (B U : Set D) {e : Existential} {g : PartialAssign ℕ D} [Nonempty D] (hf : e.Fresh g 1) : extension 1 (imp (exists_ e 1 (atom B 1)) (atom U 1)) g = {h : PartialAssign ℕ D | h = g ∧ B = ∅} ∪ {h : PartialAssign ℕ D | ∃ x ∈ B, x ∈ U ∧ h = g.update 1 x}

The donkey conditional ∃₁ B 1 → U 1, if anyone is outside, they are happy, has the same positive extension as the bathroom sentence, so its truth conditions are existential ((42)).

theorem Elliott2020.extension_false_donkey {D : Type} (B U : Set D) {e : Existential} {g : PartialAssign ℕ D} (hf : e.Fresh g 1) : extension (-1) (imp (exists_ e 1 (atom B 1)) (atom U 1)) g = {h : PartialAssign ℕ D | ∃ x ∈ B, x ∉ U ∧ h = g.update 1 x}

The donkey conditional is falsified by the resets of 1 to someone outside and unhappy ((43)).

theorem Elliott2020.extension_true_conj_atom_exists {D : Type} {e : Existential} {g : PartialAssign ℕ D} (P Q : Set D) (hg : g 1 = ⊥) : extension 1 (conj (atom P 1) (exists_ e 1 (atom Q 1))) g = ∅

A pronoun before its indefinite, P 1 ∧ ∃₁ Q 1, is never verified at an input not valuing 1 ((27)).

theorem Elliott2020.extension_true_conj_exists_atom {D : Type} {e : Existential} {g : PartialAssign ℕ D} (P Q : Set D) (hf : e.Fresh g 1) : extension 1 (conj (exists_ e 1 (atom P 1)) (atom Q 1)) g = {h : PartialAssign ℕ D | ∃ x ∈ P, x ∈ Q ∧ h = g.update 1 x}

An indefinite before its pronoun, ∃₁ P 1 ∧ Q 1, is verified by the resets of 1 to a P that is a Q, as in DPL.

theorem Elliott2020.extension_false_conj_exists_atom {D : Type} {e : Existential} {g : PartialAssign ℕ D} [Nonempty D] (P Q : Set D) (hf : e.Fresh g 1) : extension (-1) (conj (exists_ e 1 (atom P 1)) (atom Q 1)) g = {h : PartialAssign ℕ D | h = g ∧ P = ∅} ∪ {h : PartialAssign ℕ D | ∃ x ∈ P, x ∉ Q ∧ h = g.update 1 x}

∃₁ P 1 ∧ Q 1 is falsified by the input when nothing is a P, and by the resets of 1 to a P that is not a Q ((30)). By de Morgan's law these are the outputs verifying the bathroom sentence ¬ ∃₁ P 1 ∨ ¬ Q 1 ((31)).

theorem Elliott2020.not_egli_negative {D : Type} [Nonempty D] : extension (-1) (exists_ Existential.destructive 1 (conj (atom Set.univ 1) (atom ∅ 1))) ⊥ ≠ extension (-1) (conj (exists_ Existential.destructive 1 (atom Set.univ 1)) (atom ∅ 1)) ⊥

Egli's theorem fails for negative extensions (Obs. 2.5). When everyone walked in and nobody sat down, the input falsifies ∃₁ (W 1 ∧ S 1) but only its resets falsify ∃₁ W 1 ∧ S 1.

Outputs value what their inputs value

def Elliott2020.domainLE {D : Type} : SetRel (PartialAssign ℕ D) (PartialAssign ℕ D)

An assignment's relation to the assignments that value every variable it values.

Equations

• Elliott2020.domainLE = {p : PartialAssign ℕ D × PartialAssign ℕ D | p.1.domain ⊆ p.2.domain}

instance Elliott2020.instIsReflPartialAssignNatDomainLE {D : Type} : domainLE.IsRefl

instance Elliott2020.instIsTransPartialAssignNatDomainLE {D : Type} : domainLE.IsTrans

def Elliott2020.Expanding {D : Type} (m : StateSet D SignType) : Prop

Every output of m values the variables its input values.

Equations

• Elliott2020.Expanding m = ∀ (t : SignType), StateT.rel m t ⊆ Elliott2020.domainLE

theorem Elliott2020.Expanding.domain_subset {D : Type} {m : StateSet D SignType} (hm : Expanding m) {g h : PartialAssign ℕ D} {t : SignType} (hh : (t, h) ∈ m g) : g.domain ⊆ h.domain

theorem Elliott2020.expanding_atom {D : Type} (P : Set D) (n : ℕ) : Expanding (atom P n)

theorem Elliott2020.expanding_atomConst {D : Type} (P : Set D) (c : D) : Expanding (atomConst P c)

theorem Elliott2020.Expanding.map {D : Type} {f : SignType → SignType} {m : StateSet D SignType} (hm : Expanding m) : Expanding (f <$> m)

theorem Elliott2020.Expanding.map_seq {D : Type} {R : SignType → SignType → SignType} {m n : StateSet D SignType} (hm : Expanding m) (hn : Expanding n) : Expanding (R <$> m <*> n)

theorem Elliott2020.Expanding.neg {D : Type} {m : StateSet D SignType} (hm : Expanding m) : Expanding (Elliott2020.neg m)

theorem Elliott2020.Expanding.conj {D : Type} {m n : StateSet D SignType} (hm : Expanding m) (hn : Expanding n) : Expanding (Elliott2020.conj m n)

theorem Elliott2020.Expanding.disj {D : Type} {m n : StateSet D SignType} (hm : Expanding m) (hn : Expanding n) : Expanding (Elliott2020.disj m n)

theorem Elliott2020.Expanding.imp {D : Type} {m n : StateSet D SignType} (hm : Expanding m) (hn : Expanding n) : Expanding (Elliott2020.imp m n)

theorem Elliott2020.Expanding.dplExists {D : Type} {e : Existential} {n : ℕ} {m : StateSet D SignType} (hm : Expanding m) : Expanding (Elliott2020.dplExists e n m)

theorem Elliott2020.Expanding.positiveClosure {D : Type} {m : StateSet D SignType} (hm : Expanding m) : Expanding (Elliott2020.positiveClosure m)

theorem Elliott2020.Expanding.exists_ {D : Type} {e : Existential} {n : ℕ} {m : StateSet D SignType} (hm : Expanding m) : Expanding (Elliott2020.exists_ e n m)

theorem Elliott2020.ne_bot_of_mem_extension_true_exists {D : Type} {e : Existential} {n : ℕ} {m : StateSet D SignType} (hm : Expanding m) {g h : PartialAssign ℕ D} (hh : h ∈ extension 1 (exists_ e n m) g) : h n ≠ ⊥

Every positive output of an existential values its variable.

The guarded existential and the dynamic Hurford constraint

theorem Elliott2020.extension_true_conj_exists_guarded {D : Type} (L P : Set D) (g : PartialAssign ℕ D) : extension 1 (conj (exists_ Existential.guarded 1 (atom L 1)) (exists_ Existential.guarded 1 (atom P 1))) g = ∅

With the guarded existential, a linguist is here and a philosopher is here with one index is never true, since the second indefinite finds its variable valued (fn. 26 and (61)).

def Elliott2020.HurfordOdd {D : Type} {M : Type u_1} (φ ψ : M → StateSet D SignType) : Prop

The dynamic Hurford constraint (70), read as validity, marks a disjunction of φ and ψ odd when, in every model and at every input, ¬φ ∧ ψ has no positive output, or φ ∧ ¬ψ has none.

Equations

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

theorem Elliott2020.eq_and_isFalse_of_mem_extension_true_neg_exists {D : Type} {e : Existential} {n : ℕ} {m : StateSet D SignType} {g h : PartialAssign ℕ D} (hh : h ∈ extension 1 (neg (exists_ e n m)) g) : h = g ∧ IsFalse (dplExists e n m) g

An output making ¬ ∃ₙ φ true is the input, which ∃ₙ φ found false.

theorem Elliott2020.fresh_of_isFalse_dplExists {D : Type} {e : Existential} {n : ℕ} {m : StateSet D SignType} {g : PartialAssign ℕ D} (h : IsFalse (dplExists e n m) g) : e.Fresh g n

A false DPL existential found its variable fresh.

theorem Elliott2020.hurfordOdd_someone_or_they {D : Type} : HurfordOdd (fun (M : Set D × Set D) => exists_ Existential.guarded 1 (atom M.1 1)) fun (M : Set D × Set D) => atom M.2 1

With the guarded existential, (70) marks either someone is in the audience, or they're sitting down odd, since its first test ¬ ∃₁ A 1 ∧ S 1 is never verified ((65)).

theorem Elliott2020.hurfordOdd_bathroom {D : Type} : HurfordOdd (fun (M : Set D × Set D) => neg (exists_ Existential.guarded 1 (atom M.1 1))) fun (M : Set D × Set D) => atom M.2 1

With the guarded existential, (70) also marks the bathroom sentence either there is no bathroom, or it's upstairs odd, since its second test ¬ ∃₁ B 1 ∧ ¬ U 1 is never verified.

theorem Elliott2020.not_hurfordOdd_someone_or_they_destructive : ¬HurfordOdd (fun (M : Set Bool × Set Bool) => exists_ Existential.destructive 1 (atom M.1 1)) fun (M : Set Bool × Set Bool) => atom M.2 1

With the destructive existential, (70) does not mark (65) odd, because its first test is verified where 1 is already valued.

theorem Elliott2020.not_hurfordOdd_bathroom_destructive : ¬HurfordOdd (fun (M : Set Bool × Set Bool) => neg (exists_ Existential.destructive 1 (atom M.1 1))) fun (M : Set Bool × Set Bool) => atom M.2 1

With the destructive existential, (70) does not mark the bathroom sentence odd.

theorem Elliott2020.hurfordOdd_someone_or_someone_sitting {D : Type} [Nonempty D] (e : Existential) : HurfordOdd (fun (M : Set D × Set D) => exists_ e 1 (atom M.1 1)) fun (M : Set D × Set D) => exists_ e 2 (conj (atom M.1 2) (atom M.2 2))

(70) marks the Hurford disjunction either someone is in the audience, or someone in the audience is sitting down odd, for either existential ((68)).

Information states and update

Information states are the substrate's State W ℕ D, sets of world–assignment points (Def. 3.1); the initial state ⊤ pairs every world with the empty assignment.

def Elliott2020.Defined {D W : Type} (c : DynamicSemantics.State W ℕ D) (φ : W → StateSet D SignType) : Prop

Stalnaker's bridge requires a sentence to be true or false at every point of the state (Def. 3.2).

Equations

• Elliott2020.Defined c φ = ∀ p ∈ c, Elliott2020.IsTrue (φ p.world) p.assignment ∨ Elliott2020.IsFalse (φ p.world) p.assignment

def Elliott2020.update {D W : Type} (c : DynamicSemantics.State W ℕ D) (φ : W → StateSet D SignType) : DynamicSemantics.State W ℕ D

Update gathers the positive outputs at every point when the bridge holds, and is absurd otherwise (Def. 3.2).

Equations

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

theorem Elliott2020.Existential.fresh_of_eq_bot {D : Type} {e : Existential} {g : PartialAssign ℕ D} {n : ℕ} (h : g n = ⊥) : e.Fresh g n

theorem Elliott2020.familiar_update_exists {D W : Type} (e : Existential) (n : ℕ) (c : DynamicSemantics.State W ℕ D) (φ : W → StateSet D SignType) (hφ : ∀ (w : W), Expanding (φ w)) : (update c fun (w : W) => exists_ e n (φ w)).Familiar n

After an existential its variable is familiar, so the familiarity presupposition of a later pronoun is satisfied (§3.5).

theorem Elliott2020.familiar_update {D W : Type} {c : DynamicSemantics.State W ℕ D} {n : ℕ} (h : c.Familiar n) {φ : W → StateSet D SignType} (hφ : ∀ (w : W), Expanding (φ w)) : (update c φ).Familiar n

Familiarity persists through the update with any sentence whose outputs value what their inputs value (§3.5).

theorem Elliott2020.not_defined_initial_atom {D W : Type} [Nonempty W] (P : W → Set D) : ¬Defined ⊤ fun (w : W) => atom (P w) 1

A pronoun out of the blue is neither true nor false, so the initial state does not admit it ((11a)).

theorem Elliott2020.conj_atom_atom {D : Type} (L H : Set D) (n : ℕ) : conj (atom L n) (atom H n) = atom (L ∩ H) n

A conjunction of atoms of one variable is the atom of their intersection.

theorem Elliott2020.nonempty_exists_atom {D : Type} [Nonempty D] (e : Existential) (W : Set D) (n : ℕ) (g : PartialAssign ℕ D) : (exists_ e n (atom W n) g).Nonempty

An existential over an atom has an output at every input.

theorem Elliott2020.mem_atomConst_iff {D : Type} {g : PartialAssign ℕ D} {P : Set D} {c : D} {v : SignType} {h : PartialAssign ℕ D} : (v, h) ∈ atomConst P c g ↔ v = SignType.ofProp (c ∈ P) ∧ h = g

theorem Elliott2020.isTrue_or_isFalse_neg_exists_atom {D : Type} {e : Existential} {g : PartialAssign ℕ D} [Nonempty D] (W : Set D) {n : ℕ} (hf : e.Fresh g n) : IsTrue (neg (exists_ e n (atom W n))) g ∨ IsFalse (neg (exists_ e n (atom W n))) g

A negated existential over an atom is true or false at an input not valuing its variable.

theorem Elliott2020.isTrue_or_isFalse_conj_exists_atom {D : Type} {e : Existential} {g : PartialAssign ℕ D} [Nonempty D] (P Q : Set D) (hf : e.Fresh g 1) : IsTrue (conj (exists_ e 1 (atom P 1)) (atom Q 1)) g ∨ IsFalse (conj (exists_ e 1 (atom P 1)) (atom Q 1)) g

An indefinite before its pronoun is true or false at an input not valuing the variable.

theorem Elliott2020.defined_initial_someone_and_they {D W : Type} {e : Existential} [Nonempty D] (P Q : W → Set D) : Defined ⊤ fun (w : W) => conj (exists_ e 1 (atom (P w) 1)) (atom (Q w) 1)

The initial state admits a philosopher₁ is attending this talk and she₁'s sitting in the back, since the indefinite values 1 on every output the pronoun is read at ((10a)).

theorem Elliott2020.isTrue_or_isFalse_bathroom {D : Type} {e : Existential} {g : PartialAssign ℕ D} [Nonempty D] (B U : Set D) (hf : e.Fresh g 1) : IsTrue (disj (neg (exists_ e 1 (atom B 1))) (atom U 1)) g ∨ IsFalse (disj (neg (exists_ e 1 (atom B 1))) (atom U 1)) g

The bathroom sentence is true or false at an input not valuing the variable.

theorem Elliott2020.defined_initial_bathroom {D W : Type} {e : Existential} [Nonempty D] (B U : W → Set D) : Defined ⊤ fun (w : W) => disj (neg (exists_ e 1 (atom (B w) 1))) (atom (U w) 1)

The initial state admits the bathroom sentence either there is no₁ bathroom, or it₁'s upstairs, although its pronoun follows a negated indefinite ((33)).

theorem Elliott2020.not_familiar_update_neg_exists {D W : Type} {e : Existential} [Nonempty D] (P : W → Set D) {w : W} (hw : P w = ∅) : ¬(update ⊤ fun (w : W) => neg (exists_ e 1 (atom (P w) 1))).Familiar 1

After nobody is here, in a state with a world where nobody is here, 1 is not familiar, so a pronoun cannot follow a negated indefinite ((4), (5)).

theorem Elliott2020.isTrue_or_isFalse_disj_exists_atomConst {D : Type} {e : Existential} {g : PartialAssign ℕ D} [Nonempty D] (A P : Set D) (c : D) (hf : e.Fresh g 1) : IsTrue (disj (exists_ e 1 (atom A 1)) (atomConst P c)) g ∨ IsFalse (disj (exists_ e 1 (atom A 1)) (atomConst P c)) g

A disjunction of an existential and a constant atom is true or false at an input not valuing the existential's variable.

theorem Elliott2020.not_familiar_update_disj {D W : Type} {e : Existential} [Nonempty D] (A Dis : W → Set D) (ev : D) {w : W} (hA : A w = ∅) (hDis : ev ∈ Dis w) : ¬(update ⊤ fun (w : W) => disj (exists_ e 1 (atom (A w) 1)) (atomConst (Dis w) ev)).Familiar 1

After either someone₁ was in the audience, or the event was a disaster, in a state with a world where nobody was there and the event was a disaster, 1 is not familiar, so the disjunction looks externally static ((54), (55)).

theorem Elliott2020.familiar_update_update_disj {D W : Type} {e : Existential} (A Dis : W → Set D) (ev : D) : (update (update ⊤ fun (w : W) => disj (exists_ e 1 (atom (A w) 1)) (atomConst (Dis w) ev)) fun (w : W) => neg (atomConst (Dis w) ev)).Familiar 1

Once the event wasn't a disaster follows the disjunction, 1 is familiar and a pronoun can pick up the indefinite, which is Rothschild's observation ((48), (56)).

theorem Elliott2020.mem_update_update_disj {D W : Type} {e : Existential} [Nonempty D] (A Dis : W → Set D) (ev : D) {w : W} {x : D} (hx : x ∈ A w) (hev : ev ∉ Dis w) : { world := w, assignment := ⊥.update 1 x } ∈ update (update ⊤ fun (w : W) => disj (exists_ e 1 (atom (A w) 1)) (atomConst (Dis w) ev)) fun (w : W) => neg (atomConst (Dis w) ev)

In a world where someone was in the audience and the event was no disaster, the witness survives both updates of Rothschild's discourse, so its final state is not empty.

theorem Elliott2020.familiar_update_stone {D W : Type} {e : Existential} (L P H : W → Set D) : (update ⊤ fun (w : W) => disj (exists_ e 1 (conj (atom (L w) 1) (atom (H w) 1))) (exists_ e 1 (conj (atom (P w) 1) (atom (H w) 1)))).Familiar 1

The positive outputs of a Stone disjunction value its variable, so after either a linguist is here, or a philosopher is with one index, 1 is familiar, for either existential ((58)–(64)).

theorem Elliott2020.snd_eq_of_mem_exists_atom {D : Type} {e : Existential} {g : PartialAssign ℕ D} {W : Set D} {n : ℕ} (hW : W = ∅) (hf : e.Fresh g n) {p : SignType × PartialAssign ℕ D} (hp : p ∈ exists_ e n (atom W n) g) : p.2 = g

When nothing is a W, every output of ∃ₙ W n is the input.

theorem Elliott2020.isTrue_or_isFalse_disj_exists_atom {D : Type} {e : Existential} {g : PartialAssign ℕ D} [Nonempty D] (A B : Set D) (hg : g 1 = ⊥) : IsTrue (disj (exists_ e 1 (atom A 1)) (exists_ e 1 (atom B 1))) g ∨ IsFalse (disj (exists_ e 1 (atom A 1)) (exists_ e 1 (atom B 1))) g

A disjunction of two existentials over atoms is true or false at an input not valuing the variable.

theorem Elliott2020.exists_mem_update_stone {D W : Type} {e : Existential} [Nonempty D] (L P H : W → Set D) {w : W} {x : D} (hx : x ∈ L w ∩ H w) : ∃ (i : ℕ → Flat D), { world := w, assignment := i } ∈ update ⊤ fun (w : W) => disj (exists_ e 1 (conj (atom (L w) 1) (atom (H w) 1))) (exists_ e 1 (conj (atom (P w) 1) (atom (H w) 1)))

In a world with a linguist here a Stone disjunction has an output, so the state after it is not empty.