@[reducible, inline]

abbrev Semantics.Dynamic.PLA.Assignment (E : Type u_1) : Type u_1

An assignment maps variable indices to entities

Equations

• Semantics.Dynamic.PLA.Assignment E = (Semantics.Dynamic.PLA.VarIdx → E)

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.WitnessSeq (E : Type u_1) : Type u_1

A witness sequence maps pronoun indices to entities

Equations

• Semantics.Dynamic.PLA.WitnessSeq E = (Semantics.Dynamic.PLA.PronIdx → E)

def Semantics.Dynamic.PLA.«term_[_↦_]» : Lean.TrailingParserDescr

Assignment-update notation g[i ↦ e] for mathlib's Function.update.

Equations

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

structure Semantics.Dynamic.PLA.Model (E : Type u_1) : Type u_1

A model provides predicate interpretations

• interp : String → List E → Bool

  Interpretation: predicate name → argument tuple → truth value

def Semantics.Dynamic.PLA.Term.eval {E : Type u_1} (g : Assignment E) (ê : WitnessSeq E) : Term → E

Evaluate a term given assignment g and witness sequence ê.

⟦x_i⟧^{g,ê} = g(i) (variables from assignment) ⟦p_i⟧^{g,ê} = ê(i) (pronouns from witness sequence)

Variables and pronouns have different interpretation sources.

Equations

• Semantics.Dynamic.PLA.Term.eval g ê (Semantics.Dynamic.PLA.Term.var i) = g i
• Semantics.Dynamic.PLA.Term.eval g ê (Semantics.Dynamic.PLA.Term.pron i) = ê i

@[simp]

theorem Semantics.Dynamic.PLA.Term.eval_var {E : Type u_1} (g : Assignment E) (ê : WitnessSeq E) (i : VarIdx) : eval g ê (var i) = g i

@[simp]

theorem Semantics.Dynamic.PLA.Term.eval_pron {E : Type u_1} (g : Assignment E) (ê : WitnessSeq E) (i : PronIdx) : eval g ê (pron i) = ê i

def Semantics.Dynamic.PLA.Formula.sat {E : Type u_1} [Nonempty E] (M : Model E) (g : Assignment E) (ê : WitnessSeq E) : Formula → Prop

PLA Satisfaction: M, g, ê ⊨ φ

[Dek12] Definition 4, Ch. 2 (PLA Satisfaction and Truth, p.22; adapted to type-theoretic setting).

• Atomic: check predicate interpretation on evaluated terms
• Negation: classical negation
• Conjunction: both conjuncts satisfied
• Existential: witness exists in domain

Equations

• Semantics.Dynamic.PLA.Formula.sat M g ê (Semantics.Dynamic.PLA.Formula.atom name ts) = (M.interp name (List.map (Semantics.Dynamic.PLA.Term.eval g ê) ts) = true)
• Semantics.Dynamic.PLA.Formula.sat M g ê (∼φ) = ¬Semantics.Dynamic.PLA.Formula.sat M g ê φ
• Semantics.Dynamic.PLA.Formula.sat M g ê (φ ⋀ ψ) = (Semantics.Dynamic.PLA.Formula.sat M g ê φ ∧ Semantics.Dynamic.PLA.Formula.sat M g ê ψ)
• Semantics.Dynamic.PLA.Formula.sat M g ê (Semantics.Dynamic.PLA.Formula.exists_ i φ) = ∃ (e : E), Semantics.Dynamic.PLA.Formula.sat M (g[i ↦ e]) ê φ

def Semantics.Dynamic.PLA.Formula.trueIn {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) : Prop

Truth in a model: M ⊨ φ iff for all g, ∃ê such that M, g, ê ⊨ φ

Equations

• Semantics.Dynamic.PLA.Formula.trueIn M φ = ∀ (g : Semantics.Dynamic.PLA.Assignment E), ∃ (ê : Semantics.Dynamic.PLA.WitnessSeq E), Semantics.Dynamic.PLA.Formula.sat M g ê φ

theorem Semantics.Dynamic.PLA.Formula.sat_neg_neg {E : Type u_1} [Nonempty E] (M : Model E) (g : Assignment E) (ê : WitnessSeq E) (φ : Formula) : sat M g ê (∼∼φ) ↔ sat M g ê φ

Double negation elimination

theorem Semantics.Dynamic.PLA.Formula.sat_conj_left {E : Type u_1} [Nonempty E] (M : Model E) (g : Assignment E) (ê : WitnessSeq E) (φ ψ : Formula) : sat M g ê (φ ⋀ ψ) → sat M g ê φ

Conjunction elimination (left)

theorem Semantics.Dynamic.PLA.Formula.sat_conj_right {E : Type u_1} [Nonempty E] (M : Model E) (g : Assignment E) (ê : WitnessSeq E) (φ ψ : Formula) : sat M g ê (φ ⋀ ψ) → sat M g ê ψ

Conjunction elimination (right)

theorem Semantics.Dynamic.PLA.Formula.sat_conj_intro {E : Type u_1} [Nonempty E] (M : Model E) (g : Assignment E) (ê : WitnessSeq E) (φ ψ : Formula) : sat M g ê φ → sat M g ê ψ → sat M g ê (φ ⋀ ψ)

Conjunction introduction

theorem Semantics.Dynamic.PLA.Formula.sat_exists_intro {E : Type u_1} [Nonempty E] (M : Model E) (g : Assignment E) (ê : WitnessSeq E) (i : VarIdx) (φ : Formula) (e : E) : sat M (g[i ↦ e]) ê φ → sat M g ê (exists_ i φ)

Existential introduction

theorem Semantics.Dynamic.PLA.Term.eval_resolve {E : Type u_1} (g : Assignment E) (ê : WitnessSeq E) (ρ : Resolution) (t : Term) (h : ∀ (i : PronIdx), t = pron i → ê i = g (ρ i)) : eval g ê t = eval g ê (resolve ρ t)

Term evaluation under resolution: when ê(i) = g(ρ(i)), evaluation is preserved.

theorem Semantics.Dynamic.PLA.Formula.sat_resolve {E : Type u_1} [Nonempty E] (M : Model E) (g : Assignment E) (ê : WitnessSeq E) (ρ : Resolution) (φ : Formula) (hcompat : ∀ i ∈ φ.range, ê i = g (ρ i)) (hnoCapture : ∀ i ∈ φ.range, ρ i ∉ φ.domain) : sat M g ê φ ↔ sat M g ê (resolve ρ φ)

Resolution Correctness ([Dek12] Observation 7, §2.2, p.30).

If the witness sequence agrees with the assignment via resolution (ê = g ∘ ρ on pronouns), and no pronoun resolves to a bound variable, then satisfaction is preserved:

M, g, ê ⊨ φ ↔ M, g, ê ⊨ φ^ρ

def Semantics.Dynamic.PLA.exManWalkedIn : Formula

"A man walked. He sat down."

Equations

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

def Semantics.Dynamic.PLA.exResolution : Resolution

Resolution: p₀ → x₀

Equations

• Semantics.Dynamic.PLA.exResolution x✝ = 0

theorem Semantics.Dynamic.PLA.Term.eval_witness_irrelevant {E : Type u_1} (t : Term) (ht : t.pronouns = ∅) (g : Assignment E) (ê₁ ê₂ : WitnessSeq E) : eval g ê₁ t = eval g ê₂ t

For pronoun-free terms, evaluation doesn't depend on the witness sequence.

theorem Semantics.Dynamic.PLA.obs4_pla_pl_equivalence {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (hfree : φ.range = ∅) (g : Assignment E) (ê₁ ê₂ : WitnessSeq E) : Formula.sat M g ê₁ φ ↔ Formula.sat M g ê₂ φ

Observation 4 ([Dek12] §2.2, p.25): PLA and PL equivalence.

For pronoun-free formulas, satisfaction is independent of the witness sequence. This shows PLA conservatively extends PL: standard predicate logic formulas have the same truth conditions in PLA as in PL.

theorem Semantics.Dynamic.PLA.obs5_relevance {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (g₁ g₂ : Assignment E) (ê₁ ê₂ : WitnessSeq E) (hg : ∀ x ∈ φ.freeVars, g₁ x = g₂ x) (hê : ∀ i ∈ φ.range, ê₁ i = ê₂ i) : Formula.sat M g₁ ê₁ φ ↔ Formula.sat M g₂ ê₂ φ

Observation 5 ([Dek12] §2.2): Relevance.

Satisfaction depends only on the values of free variables and pronouns that actually occur in the formula. Assignments that agree on freeVars and witness sequences that agree on range yield the same satisfaction.

PLA distinguishes variables (VarIdx) from pronouns (PronIdx); Dynamic Ty2 has a single dref type S → E. The embedding uses the sum type (VarIdx ⊕ PronIdx) → E as the S parameter, providing type-safe separation without magic numbers. Because PLA updates are eliminative (filter, never extend), every PLA formula translates to a test in Dynamic Ty2.

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.MergedAssignment (E : Type u_1) : Type u_1

PLA assignment merging variable and pronoun assignments via sum type: .inl i accesses variable i, .inr i accesses pronoun i.

Equations

• Semantics.Dynamic.PLA.MergedAssignment E = (Semantics.Dynamic.PLA.VarIdx ⊕ Semantics.Dynamic.PLA.PronIdx → E)

def Semantics.Dynamic.PLA.varDref {E : Type u_1} (i : VarIdx) : Core.Dref (MergedAssignment E) E

Variable dref: projection at .inl i.

Equations

• Semantics.Dynamic.PLA.varDref i g = g (Sum.inl i)

def Semantics.Dynamic.PLA.pronDref {E : Type u_1} (i : PronIdx) : Core.Dref (MergedAssignment E) E

Pronoun dref: projection at .inr i.

Equations

• Semantics.Dynamic.PLA.pronDref i g = g (Sum.inr i)

def Semantics.Dynamic.PLA.termToDref {E : Type u_1} : Term → Core.Dref (MergedAssignment E) E

Interpret a PLA term as a Dynamic Ty2 dref.

Equations

• Semantics.Dynamic.PLA.termToDref (Semantics.Dynamic.PLA.Term.var i) = Semantics.Dynamic.PLA.varDref i
• Semantics.Dynamic.PLA.termToDref (Semantics.Dynamic.PLA.Term.pron i) = Semantics.Dynamic.PLA.pronDref i

def Semantics.Dynamic.PLA.plaPossToMerged {E : Type u_1} (p : Core.PLAPoss E) : MergedAssignment E

Convert PLAPoss to merged assignment.

Equations

• Semantics.Dynamic.PLA.plaPossToMerged p (Sum.inl i) = p.assignment i
• Semantics.Dynamic.PLA.plaPossToMerged p (Sum.inr i) = p.witnesses i

def Semantics.Dynamic.PLA.mergedToPLAPoss {E : Type u_1} (g : MergedAssignment E) : Core.PLAPoss E

Convert merged assignment to PLAPoss.

Equations

• Semantics.Dynamic.PLA.mergedToPLAPoss g = { assignment := fun (i : ℕ) => g (Sum.inl i), witnesses := fun (i : ℕ) => g (Sum.inr i) }

theorem Semantics.Dynamic.PLA.plaPoss_roundtrip {E : Type u_1} (p : Core.PLAPoss E) : mergedToPLAPoss (plaPossToMerged p) = p

theorem Semantics.Dynamic.PLA.merged_roundtrip {E : Type u_1} (g : MergedAssignment E) : plaPossToMerged (mergedToPLAPoss g) = g

def Semantics.Dynamic.PLA.extend {E : Type u_1} (g : MergedAssignment E) (i : VarIdx) (e : E) : MergedAssignment E

Functional update for merged assignments (only affects variables).

Equations

• Semantics.Dynamic.PLA.extend g i e (Sum.inl i_1) = if i_1 = i then e else g (Sum.inl i_1)
• Semantics.Dynamic.PLA.extend g i e (Sum.inr i_1) = g (Sum.inr i_1)

def Semantics.Dynamic.PLA.evalTerm {E : Type u_1} (g : MergedAssignment E) : Term → E

Evaluate a term given a merged assignment.

Equations

• Semantics.Dynamic.PLA.evalTerm g (Semantics.Dynamic.PLA.Term.var i) = g (Sum.inl i)
• Semantics.Dynamic.PLA.evalTerm g (Semantics.Dynamic.PLA.Term.pron i) = g (Sum.inr i)

def Semantics.Dynamic.PLA.formulaToCondition {E : Type u_1} (M : Model E) : Formula → Core.Condition (MergedAssignment E)

Translate a PLA formula to a Dynamic Ty2 condition.

PLA existentials check for existence of a witness but don't extend the assignment (eliminative semantics).

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Dynamic.PLA.formulaToCondition M (∼φ) = fun (g : Semantics.Dynamic.PLA.MergedAssignment E) => ¬Semantics.Dynamic.PLA.formulaToCondition M φ g

def Semantics.Dynamic.PLA.formulaToDRS {E : Type u_1} (M : Model E) (φ : Formula) : Core.Update (MergedAssignment E)

Translate a PLA formula to a Dynamic Ty2 Update. PLA's eliminative updates mean every formula translates to a test.

Equations

• Semantics.Dynamic.PLA.formulaToDRS M φ = Semantics.Dynamic.Core.test (Semantics.Dynamic.PLA.formulaToCondition M φ)

theorem Semantics.Dynamic.PLA.formulaToDRS_atom {E : Type u_1} [Nonempty E] (M : Model E) (name : String) (ts : List Term) : formulaToDRS M (Formula.atom name ts) = Core.test fun (g : MergedAssignment E) => M.interp name (List.map (evalTerm g) ts) = true

theorem Semantics.Dynamic.PLA.formulaToDRS_neg {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) : formulaToDRS M (∼φ) = Core.test fun (g : MergedAssignment E) => ¬formulaToCondition M φ g

theorem Semantics.Dynamic.PLA.formulaToDRS_conj {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) : formulaToDRS M (φ ⋀ ψ) = Core.test fun (g : MergedAssignment E) => formulaToCondition M φ g ∧ formulaToCondition M ψ g

theorem Semantics.Dynamic.PLA.formulaToDRS_exists {E : Type u_1} [Nonempty E] (M : Model E) (x : VarIdx) (φ : Formula) : formulaToDRS M (Formula.exists_ x φ) = Core.test fun (g : MergedAssignment E) => ∃ (e : E), formulaToCondition M φ (extend g x e)

def Semantics.Dynamic.PLA.splitAssignment {E : Type u_1} (g : MergedAssignment E) : Assignment E × WitnessSeq E

Split a merged assignment into variable and witness components.

Equations

• Semantics.Dynamic.PLA.splitAssignment g = (fun (i : Semantics.Dynamic.PLA.VarIdx) => g (Sum.inl i), fun (i : Semantics.Dynamic.PLA.PronIdx) => g (Sum.inr i))

theorem Semantics.Dynamic.PLA.evalTerm_eq_Term_eval {E : Type u_1} [Nonempty E] (g : MergedAssignment E) (t : Term) : evalTerm g t = Term.eval (splitAssignment g).1 (splitAssignment g).2 t

theorem Semantics.Dynamic.PLA.extend_fst_eq_update {E : Type u_1} [Nonempty E] (g : MergedAssignment E) (x : VarIdx) (e : E) : (splitAssignment (extend g x e)).1 = (splitAssignment g).1[x ↦ e]

theorem Semantics.Dynamic.PLA.extend_snd_eq {E : Type u_1} [Nonempty E] (g : MergedAssignment E) (x : VarIdx) (e : E) : (splitAssignment (extend g x e)).2 = (splitAssignment g).2

theorem Semantics.Dynamic.PLA.formulaToCondition_eq_sat {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (g : MergedAssignment E) : formulaToCondition M φ g ↔ Formula.sat M (splitAssignment g).1 (splitAssignment g).2 φ

theorem Semantics.Dynamic.PLA.formulaToDRS_correct {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (g h : MergedAssignment E) : formulaToDRS M φ g h ↔ g = h ∧ Formula.sat M (splitAssignment g).1 (splitAssignment g).2 φ

A merged assignment satisfies the embedded Update iff the split assignment satisfies the original PLA formula.