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 : Kripke.ClassicalValuation) (φ : 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 :
      Semantics (Formula ℕ) Kripke.ClassicalValuation
      Equations
      source
      @[simp]
      theorem LO.IntProp.Formula.Kripke.ClassicalSatisfies.atom_def {V : Kripke.ClassicalValuation} {a : ℕ} :
      V ⊧ atom a ↔ V a
      source
      instance LO.IntProp.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuationNat :
      Semantics.Tarski Kripke.ClassicalValuation
      source
      theorem LO.IntProp.Hilbert.Cl.classical_sound {φ : Formula ℕ} :
      Hilbert.Cl ℕ ⊢! φ → ∀ (V : Kripke.ClassicalValuation), V ⊧ φ
      source
      theorem LO.IntProp.Hilbert.Cl.unprovable_of_exists_classicalValuation {φ : Formula ℕ} :
      (∃ (V : Kripke.ClassicalValuation), ¬V ⊧ φ) → Hilbert.Cl ℕ ⊬ φ