K

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

• q : α

  Imported declaration from the Incompleteness formalization.

• ne_pq : p H ≠ q H
• mem_K : Axioms.K (Formula.atom (p H)) (Formula.atom (q H)) ∈ H.axioms

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasAxiomKFormulaOfDecidableEqOfHasK {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hK : H.HasK] : Entailment.HasAxiomK H

Equations

• LO.Modal.Hilbert.instHasAxiomKFormulaOfDecidableEqOfHasK = { K := fun (φ ψ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

@[reducible, inline]

abbrev LO.Modal.Hilbert.K : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

instance LO.Modal.Hilbert.instFiniteAxiomatizableNatK : Hilbert.K.FiniteAxiomatizable

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasKNatK : Hilbert.K.HasK

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.instKNatFormulaK : Entailment.K Hilbert.K

Equations

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