Documentation

Foundation.IntProp.Kripke.Classical

source
@[reducible, inline]
abbrev LO.IntProp.Kripke.ClassicalValuation :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.IntProp.Formula.Kripke.ClassicalSatisfies (V : LO.IntProp.Kripke.ClassicalValuation) (φ : LO.IntProp.Formula ℕ) :
    Prop
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance LO.IntProp.Formula.Kripke.ClassicalSatisfies.instSemanticsNatClassicalValuation :
      LO.Semantics (LO.IntProp.Formula ℕ) LO.IntProp.Kripke.ClassicalValuation
      Equations
      source
      @[simp]
      theorem LO.IntProp.Formula.Kripke.ClassicalSatisfies.atom_def {V : LO.IntProp.Kripke.ClassicalValuation} {a : ℕ} :
      V ⊧ LO.IntProp.Formula.atom a ↔ V a
      source
      instance LO.IntProp.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuationNat :
      LO.Semantics.Tarski LO.IntProp.Kripke.ClassicalValuation
      Equations
      source
      theorem LO.IntProp.Hilbert.Cl.classical_sound {φ : LO.IntProp.Formula ℕ} :
      LO.IntProp.Hilbert.Cl ℕ ⊢! φ → ∀ (V : LO.IntProp.Kripke.ClassicalValuation), V ⊧ φ
      source
      theorem LO.IntProp.Hilbert.Cl.unprovable_of_exists_classicalValuation {φ : LO.IntProp.Formula ℕ} :
      (∃ (V : LO.IntProp.Kripke.ClassicalValuation), ¬V ⊧ φ) → LO.IntProp.Hilbert.Cl ℕ ⊬ φ