@[reducible, inline]
Equations
- LO.Modal.Hilbert.K α = { axioms := 𝗞, rules := ⟮Nec⟯ }
@[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
Equations
@[reducible, inline]
Equations
Equations
@[reducible, inline]
Equations
Equations
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
Equations
@[reducible, inline]
Equations
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[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
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Equations
@[reducible, inline]
Equations
Instances For
- LO.Modal.GL.instModalDisjunctiveHilbertNatFormulaGL
- LO.Modal.Hilbert.GL.Kripke.complete
- LO.Modal.Hilbert.GL.Kripke.ffp
- LO.Modal.Hilbert.GL.Kripke.finite_sound
- LO.Modal.Hilbert.GL.Kripke.sound
- LO.Modal.Hilbert.GL.consistent
- LO.Modal.Hilbert.GL.instConsistentFormulaNat
- LO.Modal.Hilbert.GL.instUnnecessitationNatFormula
- LO.Modal.Hilbert.instBoxdotPropertyNatGLGrz
- LO.Modal.Hilbert.instGLFormulaGL
- LO.ProvabilityLogic.instArithmeticalSoundGLStandardDP
Equations
@[reducible, inline]
Equations
Instances For
- LO.Modal.Hilbert.Grz.Kripke.complete
- LO.Modal.Hilbert.Grz.Kripke.finite_sound
- LO.Modal.Hilbert.Grz.Kripke.instFiniteFramePropertyNatReflexiveTransitiveAntiSymmetricFiniteFrameClass
- LO.Modal.Hilbert.Grz.Kripke.sound
- LO.Modal.Hilbert.Grz.consistent
- LO.Modal.Hilbert.instBoxdotPropertyNatGLGrz
- LO.Modal.Hilbert.instGrzFormulaGrz
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 := ∅ }
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⟯ }