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

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

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

Equations

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

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

• p : α
• mem_dne : ∼∼Formula.atom (p H) ➝ Formula.atom (p H) ∈ H.axioms

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

Equations

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

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

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

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

Equations

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

class LO.Propositional.Hilbert.HasDummett {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• q : α
• 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

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

Equations

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

@[reducible, inline]

abbrev LO.Propositional.Hilbert.Cl : Hilbert ℕ

Equations

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

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

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

Equations

• LO.Propositional.Hilbert.instHasEFQNatCl = { p := 0, mem_efq := LO.Propositional.Hilbert.instHasEFQNatCl.proof_1 }

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

Equations

• LO.Propositional.Hilbert.instHasLEMNatCl = { p := 0, mem_lem := LO.Propositional.Hilbert.instHasLEMNatCl.proof_1 }

instance LO.Propositional.Hilbert.instClNatFormulaCl : Entailment.Cl Hilbert.Cl

Equations

• LO.Propositional.Hilbert.instClNatFormulaCl = LO.Entailment.Cl.mk

theorem LO.Propositional.Hilbert.Int_weakerThan_Cl : Hilbert.Int ⪯ Hilbert.Cl

@[reducible, inline]

abbrev LO.Propositional.Hilbert.KC : Hilbert ℕ

Equations

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

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

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

Equations

• LO.Propositional.Hilbert.instHasEFQNatKC = { p := 0, mem_efq := LO.Propositional.Hilbert.instHasEFQNatKC.proof_1 }

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

Equations

• LO.Propositional.Hilbert.instHasWeakLEMNatKC = { p := 0, mem_wlem := LO.Propositional.Hilbert.instHasWeakLEMNatKC.proof_1 }

instance LO.Propositional.Hilbert.instKCNatFormulaKC : Entailment.KC Hilbert.KC

Equations

• LO.Propositional.Hilbert.instKCNatFormulaKC = LO.Entailment.KC.mk

@[reducible, inline]

abbrev LO.Propositional.Hilbert.LC : Hilbert ℕ

Equations

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

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

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

Equations

• LO.Propositional.Hilbert.instHasEFQNatLC = { p := 0, mem_efq := LO.Propositional.Hilbert.instHasEFQNatLC.proof_1 }

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

Equations

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

instance LO.Propositional.Hilbert.instLCNatFormulaLC : Entailment.LC Hilbert.LC

Equations

• LO.Propositional.Hilbert.instLCNatFormulaLC = LO.Entailment.LC.mk