WellKnown

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

• mem_lem : Formula.atom (p H) ⋎ ∼Formula.atom (p H) ∈ H.axioms

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasAxiomLEMFormulaOfDecidableEqOfHasLEM {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hLEM : H.HasLEM] : Entailment.HasAxiomLEM H

Equations

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

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

• mem_dne : ∼∼Formula.atom (p H) ==> Formula.atom (p H) ∈ H.axioms

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasAxiomDNEFormulaOfDecidableEqOfHasDNE {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hDNE : H.HasDNE] : Entailment.HasAxiomDNE H

Equations

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

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

• mem_wlem : ∼Formula.atom (p H) ⋎ ∼∼Formula.atom (p H) ∈ H.axioms

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasAxiomWeakLEMFormulaOfDecidableEqOfHasWeakLEM {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hWLEM : H.HasWeakLEM] : Entailment.HasAxiomWeakLEM H

Equations

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

class LO.IntProp.Hilbert.HasDummett {α : 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_dummet : (Formula.atom (p H) ==> Formula.atom (q H)) ⋎ (Formula.atom (q H) ==> Formula.atom (p H)) ∈ H.axioms

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasAxiomDummettFormulaOfDecidableEqOfHasDummett {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hDummett : H.HasDummett] : Entailment.HasAxiomDummett H

Equations

• LO.IntProp.Hilbert.instHasAxiomDummettFormulaOfDecidableEqOfHasDummett = { dummett := fun (φ ψ : LO.IntProp.Formula α) => LO.IntProp.Hilbert.Deduction.maxm ⋯ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Cl : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

instance LO.IntProp.Hilbert.instFiniteAxiomatizableNatCl : Hilbert.Cl.FiniteAxiomatizable

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasEFQNatCl : Hilbert.Cl.HasEFQ

Equations

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

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasLEMNatCl : Hilbert.Cl.HasLEM

Equations

• LO.IntProp.Hilbert.instHasLEMNatCl = { p := 0, mem_lem := LO.IntProp.Hilbert.instHasLEMNatCl._proof_1 }

@[implicit_reducible]

instance LO.IntProp.Hilbert.instClassicalNatFormulaCl : Entailment.Classical Hilbert.Cl

Equations

• LO.IntProp.Hilbert.instClassicalNatFormulaCl = { toMinimal := LO.IntProp.Hilbert.instMinimalFormula, toHasAxiomDNE := LO.Entailment.instHasAxiomDNEOfHasAxiomEFQOfHasAxiomLEM }

theorem LO.IntProp.Hilbert.Int_weakerThan_Cl : Hilbert.Int wkn Hilbert.Cl

@[reducible, inline]

abbrev LO.IntProp.Hilbert.KC : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

instance LO.IntProp.Hilbert.instFiniteAxiomatizableNatKC : Hilbert.KC.FiniteAxiomatizable

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasEFQNatKC : Hilbert.KC.HasEFQ

Equations

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

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasWeakLEMNatKC : Hilbert.KC.HasWeakLEM

Equations

• LO.IntProp.Hilbert.instHasWeakLEMNatKC = { p := 0, mem_wlem := LO.IntProp.Hilbert.instHasWeakLEMNatKC._proof_1 }

@[implicit_reducible]

instance LO.IntProp.Hilbert.instIntuitionisticNatFormulaKC : Entailment.Intuitionistic Hilbert.KC

Equations

• LO.IntProp.Hilbert.instIntuitionisticNatFormulaKC = { toMinimal := LO.IntProp.Hilbert.instMinimalFormula, toHasAxiomEFQ := LO.IntProp.Hilbert.instHasAxiomEFQFormulaOfDecidableEqOfHasEFQ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.LC : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Hilbert.LC = { axioms := {LO.Axioms.EFQ (LO.IntProp.Formula.atom 0), LO.Axioms.Dummett (LO.IntProp.Formula.atom 0) (LO.IntProp.Formula.atom 1)} }

instance LO.IntProp.Hilbert.instFiniteAxiomatizableNatLC : Hilbert.LC.FiniteAxiomatizable

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasEFQNatLC : Hilbert.LC.HasEFQ

Equations

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

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasDummettNatLC : Hilbert.LC.HasDummett

Equations

• LO.IntProp.Hilbert.instHasDummettNatLC = { p := 0, q := 1, ne_pq := LO.IntProp.Hilbert.instHasDummettNatLC._proof_1, mem_dummet := LO.IntProp.Hilbert.instHasDummettNatLC._proof_2 }

@[implicit_reducible]

instance LO.IntProp.Hilbert.instIntuitionisticNatFormulaLC : Entailment.Intuitionistic Hilbert.LC

Equations

• LO.IntProp.Hilbert.instIntuitionisticNatFormulaLC = { toMinimal := LO.IntProp.Hilbert.instMinimalFormula, toHasAxiomEFQ := LO.IntProp.Hilbert.instHasAxiomEFQFormulaOfDecidableEqOfHasEFQ }