Int

class LO.IntProp.Hilbert.HasEFQ {α : Type u_1} (H : Hilbert α) : Type u_1

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

• mem_efq : ⊥ ==> Formula.atom (p H) ∈ H.axioms

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasAxiomEFQFormulaOfDecidableEqOfHasEFQ {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hEfq : H.HasEFQ] : Entailment.HasAxiomEFQ H

Equations

• LO.IntProp.Hilbert.instHasAxiomEFQFormulaOfDecidableEqOfHasEFQ = { efq := fun (φ : LO.IntProp.Formula α) => LO.IntProp.Hilbert.Deduction.maxm ⋯ }

@[implicit_reducible]

instance LO.IntProp.Hilbert.instIntuitionisticFormulaOfDecidableEqOfHasEFQ {α : Type u_1} {H : Hilbert α} [DecidableEq α] [H.HasEFQ] : Entailment.Intuitionistic H

Equations

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

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Int : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Hilbert.Int = { axioms := {LO.Axioms.EFQ (LO.IntProp.Formula.atom 0)} }

instance LO.IntProp.Hilbert.instFiniteAxiomatizableNatInt : Hilbert.Int.FiniteAxiomatizable

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasEFQNatInt : Hilbert.Int.HasEFQ

Equations

• LO.IntProp.Hilbert.instHasEFQNatInt = { p := 0, mem_efq := LO.IntProp.Hilbert.instHasEFQNatInt._proof_1 }