Basic

@[reducible, inline]

abbrev LO.Modal.Logic : Type

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic = Set (LO.Modal.Formula ℕ)

@[reducible, inline]

abbrev LO.Modal.Hilbert.logic (H : Hilbert ℕ) : Logic

Imported declaration from the Incompleteness formalization.

Equations

• H.logic = {φ : LO.Modal.Formula ℕ | H ⊢! φ}

@[reducible, inline]

abbrev LO.Modal.Logic.K : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.K = LO.Modal.Hilbert.K.logic

class LO.Modal.Logic.Unnecessitation (L : Logic) : Prop

Imported declaration from the Incompleteness formalization.

• unnec_closed {φ : Formula ℕ} : □φ ∈ L → φ ∈ L

class LO.Modal.Logic.ModalDisjunctive (L : Logic) : Prop

Imported declaration from the Incompleteness formalization.

• modal_disjunctive_closed {φ ψ : Formula ℕ} : □φ ⋎ □ψ ∈ L → φ ∈ L ∨ ψ ∈ L

class LO.Modal.Logic.QuasiNormal (L : Logic) : Prop

Imported declaration from the Incompleteness formalization.

• subset_K : Logic.K ⊆ L
• mdp_closed {φ ψ : Formula ℕ} : φ ==> ψ ∈ L → φ ∈ L → ψ ∈ L
• subst_closed {φ : Formula ℕ} : φ ∈ L → ∀ (s : Substitution ℕ), φ⟦s⟧ ∈ L

class LO.Modal.Logic.Normal (L : Logic) extends L.QuasiNormal : Prop

Imported declaration from the Incompleteness formalization.

• subset_K : Logic.K ⊆ L
• mdp_closed {φ ψ : Formula ℕ} : φ ==> ψ ∈ L → φ ∈ L → ψ ∈ L
• subst_closed {φ : Formula ℕ} : φ ∈ L → ∀ (s : Substitution ℕ), φ⟦s⟧ ∈ L
• nec_closed {φ : Formula ℕ} : φ ∈ L → □φ ∈ L

class LO.Modal.Logic.Sublogic (L₁ L₂ : Logic) : Prop

Imported declaration from the Incompleteness formalization.

• subset : L₁ ⊆ L₂

class LO.Modal.Logic.ProperSublogic (L₁ L₂ : Logic) : Prop

Imported declaration from the Incompleteness formalization.

• ssubset : L₁ ⊂ L₂

instance LO.Modal.Hilbert.normal {H : Hilbert ℕ} [H.HasK] : H.logic.Normal

instance LO.Modal.Hilbert.instUnnecessitationLogicOfUnnecessitationNatFormula {H : Hilbert ℕ} [Entailment.Unnecessitation H] : H.logic.Unnecessitation

instance LO.Modal.Hilbert.instModalDisjunctiveLogicOfModalDisjunctiveNatFormula {H : Hilbert ℕ} [Entailment.ModalDisjunctive H] : H.logic.ModalDisjunctive

instance LO.Modal.Hilbert.instNormalK : Logic.K.Normal

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.logic (C : FrameClass) : Logic

Imported declaration from the Incompleteness formalization.

Equations

• C.logic = {φ : LO.Modal.Formula ℕ | C ⊧ φ}

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteFrameClass.logic (C : FiniteFrameClass) : Logic

Imported declaration from the Incompleteness formalization.

Equations

• C.logic = {φ : LO.Modal.Formula ℕ | C ⊧ φ}

theorem LO.Modal.Logic.eq_Hilbert_Logic_KripkeFrameClass_Logic {H : Hilbert ℕ} {C : Kripke.FrameClass} [sound : Sound H C] [complete : Complete H C] : H.logic = C.logic

theorem LO.Modal.Logic.eq_Hilbert_Logic_KripkeFiniteFrameClass_Logic {H : Hilbert ℕ} {C : Kripke.FiniteFrameClass} [sound : Sound H C] [complete : Complete H C] : H.logic = C.logic

theorem LO.Modal.Logic.K.eq_AllKripkeFrameClass_Logic : Logic.K = Kripke.AllFrameClass.logic

theorem LO.Modal.Logic.K.eq_AllKripkeFiniteFrameClass_Logic : Logic.K = Kripke.AllFiniteFrameClass.logic