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

Discourse referent export: existential update makes witnesses available for anaphora.

theorem Semantics.Dynamic.PLA.exists_update_characterization {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 φ}

Existential update output characterization.

theorem Semantics.Dynamic.PLA.cross_sentential_binding {E : Type u_1} [Nonempty E] (M : Model E) (x : VarIdx) (φ ψ : Formula) (s : InfoState E) (p : Poss E) (hp : p ∈ (Formula.update M (Formula.exists_ x φ) ;; Formula.update M ψ) s) : p ∈ Formula.update M (Formula.exists_ x φ) s ∧ Formula.sat M p.1 p.2 ψ

Cross-sentential binding: existentials in first sentence bind variables in second.

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

Cross-sentential binding gives access to the witness.

theorem Semantics.Dynamic.PLA.neg_domain (φ : Formula) : (∼φ).domain = φ.domain

Domain passes through negation.

theorem Semantics.Dynamic.PLA.dne_domain_same (φ : Formula) : (∼∼φ).domain = φ.domain

Double negation preserves domain.

theorem Semantics.Dynamic.PLA.dne_range_same (φ : Formula) : (∼∼φ).range = φ.range

Double negation preserves range.

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

Existential introduces witness unlike double-negated existential.

theorem Semantics.Dynamic.PLA.exists_domain_nonempty (x : VarIdx) (φ : Formula) : (Formula.exists_ x φ).domain.Nonempty

Existential domain is nonempty.

theorem Semantics.Dynamic.PLA.seq_update_mem {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) (p : Poss E) : p ∈ (Formula.update M φ ;; Formula.update M ψ) s ↔ p ∈ s ∧ Formula.sat M p.1 p.2 φ ∧ Formula.sat M p.1 p.2 ψ

Sequential update composition membership.

theorem Semantics.Dynamic.PLA.seq_update_eq {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) : (Formula.update M φ ;; Formula.update M ψ) s = {p : Assignment E × WitnessSeq E | p ∈ s ∧ Formula.sat M p.1 p.2 φ ∧ Formula.sat M p.1 p.2 ψ}

Sequential update as set comprehension.

theorem Semantics.Dynamic.PLA.static_conjunction_commutes {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) (_hφ : φ.domain = ∅) (_hψ : ψ.domain = ∅) : (Formula.update M φ ;; Formula.update M ψ) s = (Formula.update M ψ ;; Formula.update M φ) s

Dref-free formulas have commutative conjunction.

theorem Semantics.Dynamic.PLA.dyn_eq_static_when_no_drefs {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) (_hφ : φ.domain = ∅) (_hψ : ψ.domain = ∅) : (Formula.update M φ ;; Formula.update M ψ) s = Formula.update M (φ ⋀ ψ) s

Dynamic conjunction equals static for dref-free formulas.

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

Existential extends scope rightward in dynamic conjunction.

theorem Semantics.Dynamic.PLA.static_existential_local_scope (x : VarIdx) (φ ψ : Formula) : x ∈ (Formula.exists_ x φ).domain ∧ (Formula.exists_ x φ ⋀ ψ).domain = (Formula.exists_ x φ).domain ∪ ψ.domain

Static existential has local scope.

def Semantics.Dynamic.PLA.bathroomSentence : Formula

Bathroom sentence: pronoun binding from negated existential (Partee).

Equations

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

theorem Semantics.Dynamic.PLA.bathroom_range_has_pronoun : 0 ∈ bathroomSentence.range

Bathroom sentence has unbound pronoun in PLA.

theorem Semantics.Dynamic.PLA.bathroom_domain_nonempty : bathroomSentence.domain.Nonempty

Bathroom sentence domain is nonempty despite negated existential.