Documentation

Linglib.Semantics.Dynamic.DPL.Semantics

The interpretations of dynamic predicate logic #

A formula of DPL/Syntax.lean has two interpretations in a structure M. The dynamic one, Formula.eval, is Groenendijk and Stokhof's, a relation between assignments, built from the update algebra of Update.lean, with conjunction as composition, the existential as a random reset followed by its scope, and everything else a test. The static one is that of predicate logic, mathlib's satisfaction of the formula read as a first-order formula, φ.toFormula.Realize. A formula is true at an assignment under the dynamic interpretation when it has an output there, (φ.eval M).dom; the two notions of truth agree on the scope-bound formulas (DPL/Context.lean) and differ where a quantifier binds outside its scope.

Main definitions #

Main results #

Implementation notes #

eval is stated through the substrate's dexists and dforall, so that the laws of the update algebra apply to it as they stand; mem_dexists and mem_dforall unfold them at assignments. The converse of isTest_eval fails, a test such as x ≐ y ⋏ ∃[x] (x ≐ y) having an active quantifier variable.

References #

source
def DPL.Formula.eval {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] :
Formula L V → DynamicSemantics.Update (V → M)

The dynamic interpretation relates the input assignments to their output assignments.

Equations
Instances For
    source
    @[simp]
    theorem DPL.Formula.eval_top {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] :
    eval M top = SetRel.id
    source
    @[simp]
    theorem DPL.Formula.eval_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] (φ : Formula L V) :
    eval M φ.neg = DynamicSemantics.Update.test (eval M φ).neg
    source
    @[simp]
    theorem DPL.Formula.eval_conj {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] (φ ψ : Formula L V) :
    eval M (φ.conj ψ) = SetRel.comp (eval M φ) (eval M ψ)
    source
    @[simp]
    theorem DPL.Formula.eval_disj {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] (φ ψ : Formula L V) :
    eval M (φ.disj ψ) = DynamicSemantics.Update.test ((eval M φ).disj (eval M ψ))
    source
    @[simp]
    theorem DPL.Formula.eval_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] (φ ψ : Formula L V) :
    eval M (φ.imp ψ) = DynamicSemantics.Update.test ((eval M φ).impl (eval M ψ))
    source
    @[simp]
    theorem DPL.Formula.eval_ex {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] (φ : Formula L V) (x : V) :
    eval M (ex x φ) = DynamicSemantics.Update.dexists x (eval M φ)
    source
    @[simp]
    theorem DPL.Formula.eval_all {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] (φ : Formula L V) (x : V) :
    eval M (all x φ) = DynamicSemantics.Update.test (DynamicSemantics.Update.dforall x (eval M φ))
    source
    @[simp]
    theorem DPL.Formula.eval_rel {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] {n : ℕ} (R : L.Relations n) (ts : Fin n → L.Term V) :
    eval M (rel R ts) = DynamicSemantics.Update.test {g : V → M | FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => FirstOrder.Language.Term.realize g (ts i)}
    source
    @[simp]
    theorem DPL.Formula.eval_equal {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] (t₁ t₂ : L.Term V) :
    eval M (equal t₁ t₂) = DynamicSemantics.Update.test {g : V → M | FirstOrder.Language.Term.realize g t₁ = FirstOrder.Language.Term.realize g t₂}
    source
    theorem DPL.Formula.mem_eval_exs {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] (φ : Formula L V) {xs : List V} {g h : V → M} :
    (g, h) ∈ eval M (exs xs φ) ↔ ∃ (k : V → M), (∀ y ∉ xs, k y = g y) ∧ (k, h) ∈ eval M φ

    An existential closure runs its scope from an assignment that differs from the input at most on the closed variables.

    source
    theorem DPL.Formula.eval_conjs_map {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] {α : Type u_1} (t : α → Formula L V) (C : α → Set (V → M)) (as : List α) (h : ∀ a ∈ as, eval M (t a) = DynamicSemantics.Update.test (C a)) :
    eval M (conjs (List.map t as)) = DynamicSemantics.Update.test {f : V → M | ∀ a ∈ as, f ∈ C a}

    A conjunction of tests is the test of their conditions together.

    source
    theorem DPL.Formula.isTest_eval {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (M : Type x) [L.Structure M] {φ : Formula L V} (h : φ.aqv = ∅) :
    (eval M φ).IsTest

    A formula with no active quantifier variable is a test, since atoms, negations, disjunctions, implications and universals are and conjunction preserves it.