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

• p : α
• mem_efq : ⊥ ➝ Formula.atom (p H) ∈ H.axioms

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

Equations

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

instance LO.Propositional.Hilbert.instIntFormulaOfDecidableEqOfHasEFQ {α : Type u_1} {H : Hilbert α} [DecidableEq α] [H.HasEFQ] : Entailment.Int H

Equations

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

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 α] [H.HasLEM] : Entailment.HasAxiomLEM H

Equations

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

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 α] [H.HasDNE] : Entailment.HasAxiomDNE H

Equations

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

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 α] [H.HasWeakLEM] : Entailment.HasAxiomWeakLEM H

Equations

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

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 α] [H.HasDummett] : Entailment.HasAxiomDummett H

Equations

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

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

• p : α
• q : α
• r : α
• ne_pq : p H ≠ q H
• ne_qr : q H ≠ r H
• ne_rp : r H ≠ p H
• mem_kp : Axioms.KrieselPutnam (Formula.atom (p H)) (Formula.atom (q H)) (Formula.atom (r H)) ∈ H.axioms

instance LO.Propositional.Hilbert.instHasAxiomKrieselPutnamFormulaOfDecidableEqOfHasKrieselPutnam {α : Type u_1} {H : Hilbert α} [DecidableEq α] [H.HasKrieselPutnam] : Entailment.HasAxiomKrieselPutnam H

Equations

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

@[reducible, inline]

abbrev LO.Propositional.Hilbert.Int : Hilbert ℕ

Equations

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

@[reducible, inline]

abbrev LO.Propositional.Int : Logic ℕ

Equations

• 𝐈𝐧𝐭 = LO.Propositional.Hilbert.Int.logic

def LO.Propositional.«term𝐈𝐧𝐭» : Lean.ParserDescr

Equations

• LO.Propositional.«term𝐈𝐧𝐭» = Lean.ParserDescr.node `LO.Propositional.«term𝐈𝐧𝐭» 1024 (Lean.ParserDescr.symbol "𝐈𝐧𝐭")

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

Equations

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

instance LO.Propositional.instIntHilbertNatFormulaInt : Entailment.Int Hilbert.Int

Equations

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

@[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)} }

@[reducible, inline]

abbrev LO.Propositional.Cl : Logic ℕ

Equations

• 𝐂𝐥 = LO.Propositional.Hilbert.Cl.logic

def LO.Propositional.«term𝐂𝐥» : Lean.ParserDescr

Equations

• LO.Propositional.«term𝐂𝐥» = Lean.ParserDescr.node `LO.Propositional.«term𝐂𝐥» 1024 (Lean.ParserDescr.symbol "𝐂𝐥")

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

Equations

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

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

Equations

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

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

Equations

• LO.Propositional.instClHilbertNatFormulaCl = { toMinimal := LO.Propositional.Hilbert.instMinimalFormula, toHasAxiomDNE := LO.Entailment.instHasAxiomDNEOfDecidableEqOfHasAxiomEFQOfHasAxiomLEM }

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

@[reducible, inline]

abbrev LO.Propositional.Modal.KC : Hilbert ℕ

Equations

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

@[reducible, inline]

abbrev LO.Propositional.KC : Logic ℕ

Equations

• 𝐊𝐂 = LO.Propositional.Modal.KC.logic

def LO.Propositional.«term𝐊𝐂» : Lean.ParserDescr

Equations

• LO.Propositional.«term𝐊𝐂» = Lean.ParserDescr.node `LO.Propositional.«term𝐊𝐂» 1024 (Lean.ParserDescr.symbol "𝐊𝐂")

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

Equations

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

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

Equations

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

instance LO.Propositional.instKCHilbertNatFormulaKC : Entailment.KC Modal.KC

Equations

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

@[reducible, inline]

abbrev LO.Propositional.Hilbert.LC : Hilbert ℕ

Equations

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

@[reducible, inline]

abbrev LO.Propositional.LC : Logic ℕ

Equations

• 𝐋𝐂 = LO.Propositional.Hilbert.LC.logic

def LO.Propositional.«term𝐋𝐂» : Lean.ParserDescr

Equations

• LO.Propositional.«term𝐋𝐂» = Lean.ParserDescr.node `LO.Propositional.«term𝐋𝐂» 1024 (Lean.ParserDescr.symbol "𝐋𝐂")

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev LO.Propositional.Modal.KrieselPutnam : Hilbert ℕ

Equations

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

@[reducible, inline]

abbrev LO.Propositional.KrieselPutnam : Logic ℕ

Equations

• 𝐊𝐏 = LO.Propositional.Modal.KrieselPutnam.logic

def LO.Propositional.«term𝐊𝐏» : Lean.ParserDescr

Equations

• LO.Propositional.«term𝐊𝐏» = Lean.ParserDescr.node `LO.Propositional.«term𝐊𝐏» 1024 (Lean.ParserDescr.symbol "𝐊𝐏")

instance LO.Propositional.instHasEFQNatKrieselPutnam : Modal.KrieselPutnam.HasEFQ

Equations

• LO.Propositional.instHasEFQNatKrieselPutnam = { p := 0, mem_efq := LO.Propositional.instHasEFQNatKrieselPutnam._proof_1 }

instance LO.Propositional.instHasKrieselPutnamNatKrieselPutnam : Modal.KrieselPutnam.HasKrieselPutnam

Equations

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

instance LO.Propositional.instKrieselPutnamHilbertNatFormulaKrieselPutnam : Entailment.KrieselPutnam Modal.KrieselPutnam

Equations

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