PLA satisfaction and truth

Satisfaction and truth for Predicate Logic with Anaphora [Dek12]. Variables are interpreted by an assignment g; pronouns get their values from outside the formula through a witness sequence ê. Satisfaction M, g, ê ⊨ φ is relative to both; truth existentially quantifies the witness sequence.

Main definitions

• PLA.Assignment, PLA.WitnessSeq, PLA.Model, PLA.Term.eval
• PLA.Formula.sat, PLA.Formula.trueIn: satisfaction and truth
• PLA.formulaToDRS: embedding into Dynamic Ty2 [Mus96]

Main results

• PLA.Formula.sat_resolve: resolution correctness (Observation 7 of [Dek12])
• PLA.obs4_pla_pl_equivalence: PLA conservatively extends predicate logic
• PLA.obs5_relevance: satisfaction depends only on occurring free variables and pronouns
• PLA.formulaToDRS_correct: the Dynamic Ty2 embedding preserves satisfaction

@[reducible, inline]

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

An assignment maps variable indices to entities

Equations

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

@[reducible, inline]

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

A witness sequence maps pronoun indices to entities

Equations

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

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

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

Unlike Semantics/Intensional/Variables.lean's notation:max, this stays at the default precedence: at max the trailing [ would capture the list-literal arguments of Formula.atom.

Equations

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

structure 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 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

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

@[simp]

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

@[simp]

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

theorem 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 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.

def PLA.Formula.sat {E : Type u_1} (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

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

def PLA.Formula.trueIn {E : Type u_1} (M : Model E) (φ : Formula) : Prop

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

Equations

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

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

Double negation elimination

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

Conjunction elimination (left)

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

Conjunction elimination (right)

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

Conjunction introduction

theorem PLA.Formula.sat_exists_intro {E : Type u_1} (M : Model E) (g : Assignment E) (ê : WitnessSeq E) (i : VarIdx) (φ : Formula) (e : E) : sat M (Function.update g i e) ê φ → sat M g ê (exists_ i φ)

Existential introduction

theorem PLA.Formula.sat_resolve {E : Type u_1} (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 PLA.exManWalkedIn : Formula

"A man walked. He sat down."

Equations

• PLA.exManWalkedIn = (PLA.Formula.exists_ 0 (PLA.Formula.atom "Man" [PLA.Term.var 0] ⋀ PLA.Formula.atom "WalkedIn" [PLA.Term.var 0]) ⋀ PLA.Formula.atom "SatDown" [PLA.Term.pron 0])

def PLA.exResolution : Resolution

Resolution: p₀ → x₀

Equations

• PLA.exResolution x✝ = 0

theorem PLA.obs4_pla_pl_equivalence {E : Type u_1} (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 PLA.obs5_relevance {E : Type u_1} (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.

Embedding into Dynamic Ty2

PLA distinguishes variables (VarIdx) from pronouns (PronIdx); Dynamic Ty2 ([Mus96]) 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 PLA.MergedAssignment (E : Type u_2) : Type u_2

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

Equations

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

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

Variable dref: projection at .inl i.

Equations

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

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

Pronoun dref: projection at .inr i.

Equations

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

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

Interpret a PLA term as a Dynamic Ty2 dref.

Equations

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

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

Functional update for merged assignments (only affects variables).

Equations

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

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

Evaluate a term given a merged assignment.

Equations

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

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

Split a merged assignment into variable and witness components.

Equations

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

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

theorem PLA.extend_fst_eq_update {E : Type u_1} (g : MergedAssignment E) (x : VarIdx) (e : E) : (splitAssignment (extend g x e)).1 = Function.update (splitAssignment g).1 x e

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

def PLA.formulaToCondition {E : Type u_1} (M : Model E) : Formula → DynamicSemantics.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

• PLA.formulaToCondition M (PLA.Formula.atom name ts) = fun (g : PLA.MergedAssignment E) => M.interp name (List.map (PLA.evalTerm g) ts) = true
• PLA.formulaToCondition M (∼φ) = fun (g : PLA.MergedAssignment E) => ¬PLA.formulaToCondition M φ g
• PLA.formulaToCondition M (φ ⋀ ψ) = fun (g : PLA.MergedAssignment E) => PLA.formulaToCondition M φ g ∧ PLA.formulaToCondition M ψ g
• PLA.formulaToCondition M (PLA.Formula.exists_ i φ) = fun (g : PLA.MergedAssignment E) => ∃ (e : E), PLA.formulaToCondition M φ (PLA.extend g i e)

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

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

Equations

• PLA.formulaToDRS M φ = DynamicSemantics.Update.test (PLA.formulaToCondition M φ)

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

theorem PLA.formulaToDRS_neg {E : Type u_1} (M : Model E) (φ : Formula) : formulaToDRS M (∼φ) = DynamicSemantics.Update.test fun (g : MergedAssignment E) => ¬formulaToCondition M φ g

theorem PLA.formulaToDRS_conj {E : Type u_1} (M : Model E) (φ ψ : Formula) : formulaToDRS M (φ ⋀ ψ) = DynamicSemantics.Update.test fun (g : MergedAssignment E) => formulaToCondition M φ g ∧ formulaToCondition M ψ g

theorem PLA.formulaToDRS_exists {E : Type u_1} (M : Model E) (x : VarIdx) (φ : Formula) : formulaToDRS M (Formula.exists_ x φ) = DynamicSemantics.Update.test fun (g : MergedAssignment E) => ∃ (e : E), formulaToCondition M φ (extend g x e)

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

theorem PLA.formulaToDRS_correct {E : Type u_1} (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.