Documentation

Linglib.Theories.Semantics.Dynamic.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
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
    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
      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
            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, ê ⊨ φ

              @cite{dekker-2012} 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
              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
                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 (@cite{dekker-2012} 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, ê ⊨ φ^ρ

                  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
                    Instances For
                      source
                      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.

                      source
                      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 (@cite{dekker-2012} §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.

                      source
                      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 (@cite{dekker-2012} §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.