@[reducible, inline]

abbrev LO.IntProp.Kripke.ClassicalValuation : Type

Equations

• LO.IntProp.Kripke.ClassicalValuation = (ℕ → Prop)

Instances For

• LO.IntProp.Formula.Kripke.ClassicalSatisfies.instSemanticsNatClassicalValuation
• LO.IntProp.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuationNat

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

instance LO.IntProp.Formula.Kripke.ClassicalSatisfies.instSemanticsNatClassicalValuation : Semantics (Formula ℕ) Kripke.ClassicalValuation

Equations

• LO.IntProp.Formula.Kripke.ClassicalSatisfies.instSemanticsNatClassicalValuation = { Realize := LO.IntProp.Formula.Kripke.ClassicalSatisfies }

@[simp]

theorem LO.IntProp.Formula.Kripke.ClassicalSatisfies.atom_def {V : Kripke.ClassicalValuation} {a : ℕ} : V ⊧ atom a ↔ V a

instance LO.IntProp.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuationNat : Semantics.Tarski Kripke.ClassicalValuation

theorem LO.IntProp.Hilbert.Cl.classical_sound {φ : Formula ℕ} : Hilbert.Cl ℕ ⊢! φ → ∀ (V : Kripke.ClassicalValuation), V ⊧ φ

theorem LO.IntProp.Hilbert.Cl.unprovable_of_exists_classicalValuation {φ : Formula ℕ} : (∃ (V : Kripke.ClassicalValuation), ¬V ⊧ φ) → Hilbert.Cl ℕ ⊬ φ