Linglib.Theories.Semantics.Dynamic.Systems.PLA.Semantics

source

@[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)

Instances For

source

@[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)

Instances For

source

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

Assignment E

Update an assignment at a single variable: g[i ↦ e]

Equations

(g[i ↦ e]) j = if j = i then e else g j

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[simp]

theorem Semantics.Dynamic.PLA.Assignment.update_same {E : Type u_1} (g : Assignment E) (i : VarIdx) (e : E) :

(g[i ↦ e]) i = e

source

@[simp]

theorem Semantics.Dynamic.PLA.Assignment.update_other {E : Type u_1} (g : Assignment E) (i j : VarIdx) (e : E) (h : j ≠ i) :

(g[i ↦ e]) j = g j

source

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

Instances For

source

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

Instances For

source

@[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

source

@[simp]

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

eval g ê (pron i) = ê i

source

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, ê ⊨ φ

Dekker Definition 3 (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]) ê φ

Instances For

source

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 ê φ

Instances For

source

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

source

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)

source

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)

source

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

source

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

source

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.

source

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 Theorem (Dekker §2.3).

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, ê ⊨ φ^ρ

source

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.

Instances For

source

def Semantics.Dynamic.PLA.exResolution :

Resolution

Resolution: p₀ → x₀

Equations

Semantics.Dynamic.PLA.exResolution x✝ = 0

Instances For