Documentation

Foundation.Modal.Hilbert.Systems

instance LO.Modal.Hilbert.instIsNormalK (α : Type u_1) :
(Hilbert.K α).IsNormal
@[reducible, inline]
abbrev LO.Modal.Hilbert.ExtK {α : Type u_1} (Ax : Theory α) :
Equations
Instances For
instance LO.Modal.Hilbert.instIsNormalExtK {α✝ : Type u_1} {Ax : Theory α✝} :
(Hilbert.ExtK Ax).IsNormal
theorem LO.Modal.Hilbert.ExtK.def_ax {α : Type u_1} {Ax : Theory α} :
(Hilbert.ExtK Ax).axioms = 𝗞 Ax
theorem LO.Modal.Hilbert.ExtK.maxm! {α : Type u_1} {Ax : Theory α} {φ : Formula α} (h : φ Ax) :
@[simp]
theorem LO.Modal.Hilbert.ExtS4.def_ax {α✝ : Type u_1} {Ax : Theory α✝} :
@[reducible, inline]
abbrev LO.Modal.Hilbert.GLS (α : Type u_1) :

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

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