Documentation

Foundation.Propositional.Kripke.Hilbert.Int

instance LO.Propositional.Hilbert.Int.Kripke.sound :

Sound Hilbert.Int Kripke.FrameClass.all

instance LO.Propositional.Hilbert.Int.Kripke.consistent :

Entailment.Consistent Hilbert.Int

instance LO.Propositional.Hilbert.Int.Kripke.sound_finite :

Sound Hilbert.Int Kripke.FrameClass.finite_all

instance LO.Propositional.Hilbert.Int.Kripke.canonical :

Kripke.Canonical Hilbert.Int Kripke.FrameClass.all

instance LO.Propositional.Hilbert.Int.Kripke.complete :

Complete Hilbert.Int Kripke.FrameClass.all

instance LO.Propositional.Hilbert.Int.Kripke.complete_finite :

Complete Hilbert.Int Kripke.FrameClass.finite_all

@[reducible, inline]

abbrev LO.Propositional.Hilbert.Int.Kripke.counterexampleDPFrame (F₁ F₂ : Kripke.Frame) (w₁ : F₁.World) (w₂ : F₂.World) :

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev LO.Propositional.Hilbert.Int.Kripke.counterexampleDPModel (M₁ M₂ : Kripke.Model) (w₁ : M₁.World) (w₂ : M₂.World) :

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem LO.Propositional.Hilbert.Int.Kripke.satisfies_left_on_counterexampleDPModel {M₁ M₂ : Kripke.Model} {w : M₁.World} {φ : Formula ℕ} {w₁ : M₁.World} {w₂ : M₂.World} :

w ⊧ φ ↔ Formula.Kripke.Satisfies (counterexampleDPModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) φ

theorem LO.Propositional.Hilbert.Int.Kripke.satisfies_right_on_counterexampleDPModel {M₁ M₂ : Kripke.Model} {w : M₂.World} {φ : Formula ℕ} {w₁ : M₁.World} {w₂ : M₂.World} :

w ⊧ φ ↔ Formula.Kripke.Satisfies (counterexampleDPModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) φ

theorem LO.Propositional.Hilbert.Int.Kripke.disjunctive {φ ψ : Formula ℕ} :

Hilbert.Int ⊢! φ ⋎ ψ → Hilbert.Int ⊢! φ ∨ Hilbert.Int ⊢! ψ

instance LO.Propositional.Hilbert.Int.Kripke.instDisjunctiveFormulaNat :

Entailment.Disjunctive Hilbert.Int