Documentation

Foundation.Modal.Hilbert.Systems

source
@[reducible, inline]
abbrev LO.Modal.Hilbert.K (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instIsNormalK (α : Type u_1) :
(Hilbert.K α).IsNormal
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.ExtK {α : Type u_1} (Ax : Theory α) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instIsNormalExtK {α✝ : Type u_1} {Ax : Theory α✝} :
(Hilbert.ExtK Ax).IsNormal
source
theorem LO.Modal.Hilbert.ExtK.K_is_extK_of_empty {α : Type u_1} :
Hilbert.K α = Hilbert.ExtK ∅
source
theorem LO.Modal.Hilbert.ExtK.K_is_extK_of_AxiomK {α : Type u_1} :
Hilbert.K α = Hilbert.ExtK 𝗞
source
theorem LO.Modal.Hilbert.ExtK.def_ax {α : Type u_1} {Ax : Theory α} :
(Hilbert.ExtK Ax).axioms = 𝗞 ∪ Ax
source
theorem LO.Modal.Hilbert.ExtK.maxm! {α : Type u_1} {Ax : Theory α} {φ : Formula α} (h : φ ∈ Ax) :
Hilbert.ExtK Ax ⊢! φ
source
@[simp]
theorem LO.Modal.Hilbert.ExtK.weakerThan {α : Type u_1} {Ax : Theory α} :
Hilbert.K α ≤ₛ Hilbert.ExtK Ax
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KT (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instKTFormulaKT (α : Type u_1) :
System.KT (Hilbert.KT α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KB (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instKBFormulaKB (α : Type u_1) :
System.KB (Hilbert.KB α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KD (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instKDFormulaKD (α : Type u_1) :
System.KD (Hilbert.KD α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KP (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instKPFormulaKP (α : Type u_1) :
System.KP (Hilbert.KP α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KTB (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.K4 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instK4FormulaK4 (α : Type u_1) :
System.K4 (Hilbert.K4 α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.K5 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instK5FormulaK5 (α : Type u_1) :
System.K5 (Hilbert.K5 α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KD45 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.K45 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KB4 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KB5 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KDB (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KD4 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KD5 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.ExtS4 {α : Type u_1} (Ax : Theory α) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.ExtS4.instS4Formula {α✝ : Type u_1} {Ax : Theory α✝} :
System.S4 (Hilbert.ExtS4 Ax)
Equations
source
@[simp]
theorem LO.Modal.Hilbert.ExtS4.def_ax {α✝ : Type u_1} {Ax : Theory α✝} :
(Hilbert.ExtS4 Ax).axioms = 𝗞 ∪ 𝗧 ∪ 𝟰 ∪ Ax
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.S4 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.S4Dot2 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instS4Dot2FormulaS4Dot2 (α : Type u_1) :
System.S4Dot2 (Hilbert.S4Dot2 α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.S4Dot3 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instS4Dot3FormulaS4Dot3 (α : Type u_1) :
System.S4Dot3 (Hilbert.S4Dot3 α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.S4Grz (α : Type u_1) :
Hilbert α
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.KT4B (α : Type u_1) :
Hilbert α
Equations
Instances For
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.S5 (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instS5FormulaS5 (α : Type u_1) :
System.S5 (Hilbert.S5 α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.Triv (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instTrivFormulaTriv (α : Type u_1) :
System.Triv (Hilbert.Triv α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.Ver (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instVerFormulaVer (α : Type u_1) :
System.Ver (Hilbert.Ver α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.GL (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instGLFormulaGL (α : Type u_1) :
System.GL (Hilbert.GL α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.Grz (α : Type u_1) :
Hilbert α
Equations
Instances For
source
instance LO.Modal.Hilbert.instGrzFormulaGrz (α : Type u_1) :
System.Grz (Hilbert.Grz α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.GLS (α : Type u_1) :
Hilbert α

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

Equations
Instances For
source
instance LO.Modal.Hilbert.instHasAxiomKFormulaGLS (α : Type u_1) :
System.HasAxiomK (Hilbert.GLS α)
Equations
source
instance LO.Modal.Hilbert.instHasAxiomLFormulaGLS (α : Type u_1) :
System.HasAxiomL (Hilbert.GLS α)
Equations
source
instance LO.Modal.Hilbert.instHasAxiomTFormulaGLS (α : Type u_1) :
System.HasAxiomT (Hilbert.GLS α)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Hilbert.N (α : Type u_1) :
Hilbert α

Logic of Pure Necessitation

Equations
Instances For
source
instance LO.Modal.Hilbert.instHasNecOnlyN (α : Type u_1) :
(Hilbert.N α).HasNecOnly