Foundation.Modal.Hilbert.Systems

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.K (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.K α = { axioms := 𝗞, rules := ⟮Nec⟯ }

Instances For

source

instance LO.Modal.Hilbert.instIsNormalK (α : Type u_1) :

(LO.Modal.Hilbert.K α).IsNormal

Equations

⋯ = ⋯

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.ExtK {α : Type u_1} (Ax : LO.Modal.Theory α) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.ExtK Ax = { axioms := 𝗞 ∪ Ax, rules := ⟮Nec⟯ }

Instances For

source

instance LO.Modal.Hilbert.instIsNormalExtK {α✝ : Type u_1} {Ax : LO.Modal.Theory α✝} :

(LO.Modal.Hilbert.ExtK Ax).IsNormal

Equations

⋯ = ⋯

source

theorem LO.Modal.Hilbert.ExtK.K_is_extK_of_empty {α : Type u_1} :

LO.Modal.Hilbert.K α = LO.Modal.Hilbert.ExtK ∅

source

theorem LO.Modal.Hilbert.ExtK.K_is_extK_of_AxiomK {α : Type u_1} :

LO.Modal.Hilbert.K α = LO.Modal.Hilbert.ExtK 𝗞

source

theorem LO.Modal.Hilbert.ExtK.def_ax {α : Type u_1} {Ax : LO.Modal.Theory α} :

(LO.Modal.Hilbert.ExtK Ax).axioms = 𝗞 ∪ Ax

source

theorem LO.Modal.Hilbert.ExtK.maxm! {α : Type u_1} {Ax : LO.Modal.Theory α} {φ : LO.Modal.Formula α} (h : φ ∈ Ax) :

LO.Modal.Hilbert.ExtK Ax ⊢! φ

source

@[simp]

theorem LO.Modal.Hilbert.ExtK.weakerThan {α : Type u_1} {Ax : LO.Modal.Theory α} :

LO.Modal.Hilbert.K α ≤ₛ LO.Modal.Hilbert.ExtK Ax

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KT (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KT α = LO.Modal.Hilbert.ExtK 𝗧

Instances For

source

instance LO.Modal.Hilbert.instKTFormulaKT (α : Type u_1) :

LO.System.KT (LO.Modal.Hilbert.KT α)

Equations

LO.Modal.Hilbert.instKTFormulaKT α = LO.System.KT.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KB α = LO.Modal.Hilbert.ExtK 𝗕

Instances For

source

instance LO.Modal.Hilbert.instKBFormulaKB (α : Type u_1) :

LO.System.KB (LO.Modal.Hilbert.KB α)

Equations

LO.Modal.Hilbert.instKBFormulaKB α = LO.System.KB.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KD α = LO.Modal.Hilbert.ExtK 𝗗

Instances For

source

instance LO.Modal.Hilbert.instKDFormulaKD (α : Type u_1) :

LO.System.KD (LO.Modal.Hilbert.KD α)

Equations

LO.Modal.Hilbert.instKDFormulaKD α = LO.System.KD.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KP (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KP α = LO.Modal.Hilbert.ExtK 𝗣

Instances For

source

instance LO.Modal.Hilbert.instKPFormulaKP (α : Type u_1) :

LO.System.KP (LO.Modal.Hilbert.KP α)

Equations

LO.Modal.Hilbert.instKPFormulaKP α = LO.System.KP.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KTB (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KTB α = LO.Modal.Hilbert.ExtK (𝗧 ∪ 𝗕)

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.K4 α = LO.Modal.Hilbert.ExtK 𝟰

Instances For

source

instance LO.Modal.Hilbert.instK4FormulaK4 (α : Type u_1) :

LO.System.K4 (LO.Modal.Hilbert.K4 α)

Equations

LO.Modal.Hilbert.instK4FormulaK4 α = LO.System.K4.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.K5 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.K5 α = LO.Modal.Hilbert.ExtK 𝟱

Instances For

source

instance LO.Modal.Hilbert.instK5FormulaK5 (α : Type u_1) :

LO.System.K5 (LO.Modal.Hilbert.K5 α)

Equations

LO.Modal.Hilbert.instK5FormulaK5 α = LO.System.K5.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD45 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KD45 α = LO.Modal.Hilbert.ExtK (𝗗 ∪ 𝟰 ∪ 𝟱)

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.K45 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.K45 α = LO.Modal.Hilbert.ExtK (𝟰 ∪ 𝟱)

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB4 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KB4 α = LO.Modal.Hilbert.ExtK (𝗕 ∪ 𝟰)

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB5 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KB5 α = LO.Modal.Hilbert.ExtK (𝗕 ∪ 𝟱)

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KDB (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KDB α = LO.Modal.Hilbert.ExtK (𝗗 ∪ 𝗕)

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD4 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KD4 α = LO.Modal.Hilbert.ExtK (𝗗 ∪ 𝟰)

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD5 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KD5 α = LO.Modal.Hilbert.ExtK (𝗗 ∪ 𝟱)

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.ExtS4 {α : Type u_1} (Ax : LO.Modal.Theory α) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.ExtS4 Ax = LO.Modal.Hilbert.ExtK (𝗧 ∪ 𝟰 ∪ Ax)

Instances For

source

instance LO.Modal.Hilbert.ExtS4.instS4Formula {α✝ : Type u_1} {Ax : LO.Modal.Theory α✝} :

LO.System.S4 (LO.Modal.Hilbert.ExtS4 Ax)

Equations

LO.Modal.Hilbert.ExtS4.instS4Formula = LO.System.S4.mk

source

@[simp]

theorem LO.Modal.Hilbert.ExtS4.def_ax {α✝ : Type u_1} {Ax : LO.Modal.Theory α✝} :

(LO.Modal.Hilbert.ExtS4 Ax).axioms = 𝗞 ∪ 𝗧 ∪ 𝟰 ∪ Ax

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.S4 α = LO.Modal.Hilbert.ExtS4 ∅

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4Dot2 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.S4Dot2 α = LO.Modal.Hilbert.ExtS4 .𝟮

Instances For

source

instance LO.Modal.Hilbert.instS4Dot2FormulaS4Dot2 (α : Type u_1) :

LO.System.S4Dot2 (LO.Modal.Hilbert.S4Dot2 α)

Equations

LO.Modal.Hilbert.instS4Dot2FormulaS4Dot2 α = LO.System.S4Dot2.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4Dot3 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.S4Dot3 α = LO.Modal.Hilbert.ExtS4 .𝟯

Instances For

source

instance LO.Modal.Hilbert.instS4Dot3FormulaS4Dot3 (α : Type u_1) :

LO.System.S4Dot3 (LO.Modal.Hilbert.S4Dot3 α)

Equations

LO.Modal.Hilbert.instS4Dot3FormulaS4Dot3 α = LO.System.S4Dot3.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4Grz (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.S4Grz α = LO.Modal.Hilbert.ExtS4 𝗚𝗿𝘇

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.KT4B (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.KT4B α = LO.Modal.Hilbert.ExtS4 𝗕

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.S5 (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.S5 α = LO.Modal.Hilbert.ExtK (𝗧 ∪ 𝟱)

Instances For

source

instance LO.Modal.Hilbert.instS5FormulaS5 (α : Type u_1) :

LO.System.S5 (LO.Modal.Hilbert.S5 α)

Equations

LO.Modal.Hilbert.instS5FormulaS5 α = LO.System.S5.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.Triv (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.Triv α = LO.Modal.Hilbert.ExtK (𝗧 ∪ 𝗧𝗰)

Instances For

source

instance LO.Modal.Hilbert.instTrivFormulaTriv (α : Type u_1) :

LO.System.Triv (LO.Modal.Hilbert.Triv α)

Equations

LO.Modal.Hilbert.instTrivFormulaTriv α = LO.System.Triv.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.Ver (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.Ver α = LO.Modal.Hilbert.ExtK 𝗩𝗲𝗿

Instances For

source

instance LO.Modal.Hilbert.instVerFormulaVer (α : Type u_1) :

LO.System.Ver (LO.Modal.Hilbert.Ver α)

Equations

LO.Modal.Hilbert.instVerFormulaVer α = LO.System.Ver.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.GL (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.GL α = LO.Modal.Hilbert.ExtK 𝗟

Instances For

source

instance LO.Modal.Hilbert.instGLFormulaGL (α : Type u_1) :

LO.System.GL (LO.Modal.Hilbert.GL α)

Equations

LO.Modal.Hilbert.instGLFormulaGL α = LO.System.GL.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.Grz (α : Type u_1) :

LO.Modal.Hilbert α

Equations

LO.Modal.Hilbert.Grz α = LO.Modal.Hilbert.ExtK 𝗚𝗿𝘇

Instances For

source

instance LO.Modal.Hilbert.instGrzFormulaGrz (α : Type u_1) :

LO.System.Grz (LO.Modal.Hilbert.Grz α)

Equations

LO.Modal.Hilbert.instGrzFormulaGrz α = LO.System.Grz.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.GLS (α : Type u_1) :

LO.Modal.Hilbert α

Solovey's Provability Logic of True Arithmetic. Remark necessitation is not permitted.

Equations

LO.Modal.Hilbert.GLS α = { axioms := (LO.Modal.Hilbert.GL α).theorems ∪ 𝗧, rules := ∅ }

Instances For

source

instance LO.Modal.Hilbert.instHasAxiomKFormulaGLS (α : Type u_1) :

LO.System.HasAxiomK (LO.Modal.Hilbert.GLS α)

Equations

LO.Modal.Hilbert.instHasAxiomKFormulaGLS α = { K := fun (x x_1 : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

source

instance LO.Modal.Hilbert.instHasAxiomLFormulaGLS (α : Type u_1) :

LO.System.HasAxiomL (LO.Modal.Hilbert.GLS α)

Equations

LO.Modal.Hilbert.instHasAxiomLFormulaGLS α = { L := fun (x : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

source

instance LO.Modal.Hilbert.instHasAxiomTFormulaGLS (α : Type u_1) :

LO.System.HasAxiomT (LO.Modal.Hilbert.GLS α)

Equations

LO.Modal.Hilbert.instHasAxiomTFormulaGLS α = { T := fun (x : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.N (α : Type u_1) :

LO.Modal.Hilbert α

Logic of Pure Necessitation

Equations

LO.Modal.Hilbert.N α = { axioms := ∅, rules := ⟮Nec⟯ }

Instances For

source

instance LO.Modal.Hilbert.instHasNecOnlyN (α : Type u_1) :

(LO.Modal.Hilbert.N α).HasNecOnly

Equations

⋯ = ⋯