class LO.Modal.Hilbert.HasP {α : Type u_1} (H : Hilbert α) : Prop

• mem_P : Axioms.P ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomPFormulaOfDecidableEqOfHasP {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hP : H.HasP] : Entailment.HasAxiomP H

Equations

• LO.Modal.Hilbert.instHasAxiomPFormulaOfDecidableEqOfHasP = { P := LO.Modal.Hilbert.Deduction.maxm ⋯ }

@[reducible, inline]

abbrev LO.Modal.Hilbert.KP : Hilbert ℕ

Equations

• LO.Modal.Hilbert.KP = { axioms := {LO.Modal.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Modal.Axioms.P} }

instance LO.Modal.Hilbert.instHasKNatKP : Hilbert.KP.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKP = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKP._proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKP._proof_2 }

instance LO.Modal.Hilbert.instHasPNatKP : Hilbert.KP.HasP

instance LO.Modal.Hilbert.instKPNatFormulaKP : Entailment.KP Hilbert.KP

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Modal.Hilbert.iff_provable_KP_provable_KD {φ : Formula ℕ} : Hilbert.KP ⊢! φ ↔ Hilbert.KD ⊢! φ