@[reducible, inline]
Equations
- LO.Modal.Hilbert.ExtK Ax = { axioms := 𝗞 ∪ Ax, rules := ⟮Nec⟯ }
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)
:
Hilbert.ExtK Ax ⊢! φ
@[simp]
theorem
LO.Modal.Hilbert.ExtK.weakerThan
{α : Type u_1}
{Ax : Theory α}
:
Hilbert.K α ≤ₛ Hilbert.ExtK Ax
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
- LO.Modal.Hilbert.ExtS4 Ax = LO.Modal.Hilbert.ExtK (𝗧 ∪ 𝟰 ∪ Ax)
Instances For
instance
LO.Modal.Hilbert.ExtS4.instS4Formula
{α✝ : Type u_1}
{Ax : Theory α✝}
:
System.S4 (Hilbert.ExtS4 Ax)
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
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
Equations
- LO.Modal.Hilbert.instHasAxiomKFormulaGLS α = { K := fun (x x_1 : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }
Equations
- LO.Modal.Hilbert.instHasAxiomLFormulaGLS α = { L := fun (x : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }
Equations
- LO.Modal.Hilbert.instHasAxiomTFormulaGLS α = { T := fun (x : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }
@[reducible, inline]
Logic of Pure Necessitation
Equations
- LO.Modal.Hilbert.N α = { axioms := ∅, rules := ⟮Nec⟯ }