def Semantics.Dynamic.DPL.DPLRel (E : Type u_1) : Type u_1

DPL semantic type: relation between assignments.

⟦φ⟧(g, h) means: starting from assignment g, the formula φ can update to assignment h.

Equations

• Semantics.Dynamic.DPL.DPLRel E = ((ℕ → E) → (ℕ → E) → Prop)

def Semantics.Dynamic.DPL.DPLRel.atom {E : Type u_1} (p : (ℕ → E) → Prop) : DPLRel E

Atomic predicate in DPL: tests without changing assignment.

Equations

• Semantics.Dynamic.DPL.DPLRel.atom p g h = (g = h ∧ p g)

def Semantics.Dynamic.DPL.DPLRel.conj {E : Type u_1} (φ ψ : DPLRel E) : DPLRel E

DPL conjunction: relation composition.

⟦φ ∧ ψ⟧(g, h) iff ∃k. ⟦φ⟧(g, k) ∧ ⟦ψ⟧(k, h)

Equations

• φ.conj ψ g h = ∃ (k : ℕ → E), φ g k ∧ ψ k h

def Semantics.Dynamic.DPL.DPLRel.exists_ {E : Type u_1} (x : ℕ) (φ : DPLRel E) : DPLRel E

DPL existential: random assignment then scope.

⟦∃x.φ⟧(g, h) iff ∃d. ⟦φ⟧(g[x↦d], h)

Equations

• Semantics.Dynamic.DPL.DPLRel.exists_ x φ g h = ∃ (d : E), φ (fun (n : ℕ) => if n = x then d else g n) h

def Semantics.Dynamic.DPL.DPLRel.neg {E : Type u_1} (φ : DPLRel E) : DPLRel E

DPL negation: test without changing assignment.

⟦¬φ⟧(g, h) iff g = h ∧ ¬∃k. ⟦φ⟧(g, k)

Note: this does not validate DNE.

Equations

• φ.neg g h = (g = h ∧ ¬∃ (k : ℕ → E), φ g k)

theorem Semantics.Dynamic.DPL.dpl_dne_fails_anaphora {E : Type u_1} [Nontrivial E] : ∃ (x : ℕ), ∃ (φ : DPLRel E), (DPLRel.exists_ x φ).neg.neg ≠ DPLRel.exists_ x φ

DPL does not validate DNE for anaphora.

¬¬∃x.φ is not equivalent to ∃x.φ because negation resets the output assignment: neg(neg(exists_ x φ)) g h forces g = h (it's a test), while exists_ x φ can change the assignment to export a witness.

Requires Nontrivial E (at least 2 elements): for Unit, all assignments are identical and DNE holds vacuously.

theorem Semantics.Dynamic.DPL.scope_extension {E : Type u_1} (x : ℕ) (φ ψ : DPLRel E) (_hfree : ∀ (g h : ℕ → E) (d : E), ψ g h ↔ ψ (fun (n : ℕ) => if n = x then d else g n) fun (n : ℕ) => if n = x then d else h n) : DPLRel.exists_ x (φ.conj ψ) = (DPLRel.exists_ x φ).conj ψ

Scope extension theorem: ∃x(φ ∧ ψ) ≡ (∃xφ) ∧ ψ when x not free in ψ.

"Not free in ψ" means ψ is invariant under reassigning x in both input and output assignments. Under this condition, the existential can scope out past conjunction.

TODO: Prove by extensionality and reordering existential quantifiers.

def Semantics.Dynamic.DPL.DPLRel.impl {E : Type u_1} (φ ψ : DPLRel E) : DPLRel E

DPL implication: internally dynamic, externally static.

⟦φ → ψ⟧(g, h) iff g = h and every output of φ from g can be extended by ψ. Implication passes on bindings from its antecedent to its consequent (internally dynamic), but the implication as a whole is a test (externally static). This gives existential quantifiers in the antecedent universal force — the key to donkey sentences.

Equations

• φ.impl ψ g h = (g = h ∧ ∀ (k : ℕ → E), φ g k → ∃ (j : ℕ → E), ψ k j)

def Semantics.Dynamic.DPL.DPLRel.disj {E : Type u_1} (φ ψ : DPLRel E) : DPLRel E

DPL disjunction: externally and internally static.

⟦φ ∨ ψ⟧(g, h) iff g = h and at least one disjunct can be successfully processed from g. No anaphoric relations are possible between or across disjuncts.

Equations

• φ.disj ψ g h = (g = h ∧ ∃ (k : ℕ → E), φ g k ∨ ψ g k)

def Semantics.Dynamic.DPL.DPLRel.forall_ {E : Type u_1} (x : ℕ) (φ : DPLRel E) : DPLRel E

DPL universal quantification: a test.

⟦∀x.φ⟧(g, h) iff g = h and for every value d at position x, φ can be successfully processed. Like negation, implication, and disjunction, the universal quantifier is externally static.

Equations

• Semantics.Dynamic.DPL.DPLRel.forall_ x φ g h = (g = h ∧ ∀ (d : E), ∃ (m : ℕ → E), φ (fun (n : ℕ) => if n = x then d else g n) m)

def Semantics.Dynamic.DPL.DPLRel.close {E : Type u_1} (φ : DPLRel E) : DPLRel E

DPL closure (the ◇ operator, Definition 17).

⟦◇φ⟧(g, h) iff g = h and φ can be successfully processed from g. Closure turns any formula into a test with the same truth conditions.

Equations

• φ.close g h = (g = h ∧ ∃ (k : ℕ → E), φ g k)

def Semantics.Dynamic.DPL.DPLRel.trueAt {E : Type u_1} (φ : DPLRel E) (g : ℕ → E) : Prop

Truth (Definition 3): φ is true w.r.t. g iff it has an output.

Equations

• φ.trueAt g = ∃ (h : ℕ → E), φ g h

def Semantics.Dynamic.DPL.DPLRel.satisfactionSet {E : Type u_1} (φ : DPLRel E) : Set (ℕ → E)

Satisfaction set (Definition 6): inputs from which φ succeeds.

Equations

• φ.satisfactionSet = {g : ℕ → E | ∃ (h : ℕ → E), φ g h}

def Semantics.Dynamic.DPL.DPLRel.productionSet {E : Type u_1} (φ : DPLRel E) : Set (ℕ → E)

Production set (Definition 9): possible outputs of φ.

Equations

• φ.productionSet = {h : ℕ → E | ∃ (g : ℕ → E), φ g h}

The connectives →, ∨, ∀x are interdefinable from ¬, ∧, ∃x. This is the standard classical interdefinability — but crucially, the reverse does not hold in DPL: ∧ and ∃x cannot be defined from →, ∨, ∀x because the latter are all externally static.

theorem Semantics.Dynamic.DPL.impl_interdefinable {E : Type u_1} (φ ψ : DPLRel E) : φ.impl ψ = (φ.conj ψ.neg).neg

φ → ψ ≈ ¬(φ ∧ ¬ψ) — implication from conjunction and negation.

theorem Semantics.Dynamic.DPL.disj_interdefinable {E : Type u_1} (φ ψ : DPLRel E) : φ.disj ψ = (φ.neg.conj ψ.neg).neg

φ ∨ ψ ≈ ¬(¬φ ∧ ¬ψ) — disjunction from conjunction and negation.

theorem Semantics.Dynamic.DPL.forall_interdefinable {E : Type u_1} (x : ℕ) (φ : DPLRel E) : DPLRel.forall_ x φ = (DPLRel.exists_ x φ.neg).neg

∀x.φ ≈ ¬∃x.¬φ — universal from existential and negation.

theorem Semantics.Dynamic.DPL.neg_exists_eq_forall_neg {E : Type u_1} (x : ℕ) (φ : DPLRel E) : (DPLRel.exists_ x φ).neg = DPLRel.forall_ x φ.neg

¬∃xφ ≈ ∀x¬φ — negation commutes with quantifier switch.

This follows from the fact that negation turns anything into a test.

theorem Semantics.Dynamic.DPL.donkey_equivalence {E : Type u_1} (x : ℕ) (φ ψ : DPLRel E) : (DPLRel.exists_ x φ).impl ψ = DPLRel.forall_ x (φ.impl ψ)

The donkey equivalence: ∃xφ → ψ ≈ ∀x[φ → ψ]

The central theorem of @cite{groenendijk-stokhof-1991}: an existential quantifier in the antecedent of an implication has universal force. This is what makes donkey sentences compositional — "if a farmer owns a donkey, he beats it" gets the universal reading from the dynamic semantics of implication alone, without stipulating wide-scope ∀.

theorem Semantics.Dynamic.DPL.conj_not_comm {E : Type u_1} [Nontrivial E] : ∃ (φ : DPLRel E), ∃ (ψ : DPLRel E), φ.conj ψ ≠ ψ.conj φ

Conjunction is not commutative in DPL.

∃xPx ∧ Qx and Qx ∧ ∃xPx differ because in the first, ∃x binds x in Qx (left-to-right binding), while in the second, Qx uses x's current value before ∃x reassigns it.

Requires Nontrivial E so that reassignment can change the value.

theorem Semantics.Dynamic.DPL.close_eq_neg_neg {E : Type u_1} (φ : DPLRel E) : φ.close = φ.neg.neg

◇φ ≈ ¬¬φ — closure is double negation (s-equivalence).

theorem Semantics.Dynamic.DPL.impl_isTest {E : Type u_1} (φ ψ : DPLRel E) (g h : ℕ → E) (h_impl : φ.impl ψ g h) : g = h

Implication is a test: ⟦φ → ψ⟧(g, h) implies g = h.

theorem Semantics.Dynamic.DPL.disj_isTest {E : Type u_1} (φ ψ : DPLRel E) (g h : ℕ → E) (h_disj : φ.disj ψ g h) : g = h

Disjunction is a test.

theorem Semantics.Dynamic.DPL.forall_isTest {E : Type u_1} (x : ℕ) (φ : DPLRel E) (g h : ℕ → E) (h_fa : DPLRel.forall_ x φ g h) : g = h

Universal quantification is a test.