instance
LO.Propositional.Hilbert.instHasAxiomEFQFormulaOfDecidableEqOfHasEFQ
{α : Type u_1}
{H : Hilbert α}
[DecidableEq α]
[H.HasEFQ]
:
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]
:
Equations
- One or more equations did not get rendered due to their size.
- p : α
Instances
instance
LO.Propositional.Hilbert.instHasAxiomLEMFormulaOfDecidableEqOfHasLEM
{α : Type u_1}
{H : Hilbert α}
[DecidableEq α]
[H.HasLEM]
:
Equations
- One or more equations did not get rendered due to their size.
- p : α
Instances
instance
LO.Propositional.Hilbert.instHasAxiomDNEFormulaOfDecidableEqOfHasDNE
{α : Type u_1}
{H : Hilbert α}
[DecidableEq α]
[H.HasDNE]
:
Equations
- One or more equations did not get rendered due to their size.
- p : α
Instances
instance
LO.Propositional.Hilbert.instHasAxiomWeakLEMFormulaOfDecidableEqOfHasWeakLEM
{α : Type u_1}
{H : Hilbert α}
[DecidableEq α]
[H.HasWeakLEM]
:
Equations
- One or more equations did not get rendered due to their size.
- p : α
- q : α
- mem_dummet : (Formula.atom (p H) ➝ Formula.atom (q H)) ⋎ (Formula.atom (q H) ➝ Formula.atom (p H)) ∈ H.axioms
Instances
instance
LO.Propositional.Hilbert.instHasAxiomDummettFormulaOfDecidableEqOfHasDummett
{α : Type u_1}
{H : Hilbert α}
[DecidableEq α]
[H.HasDummett]
:
Equations
- One or more equations did not get rendered due to their size.
- p : α
- q : α
- r : α
- mem_kp : Axioms.KrieselPutnam (Formula.atom (p H)) (Formula.atom (q H)) (Formula.atom (r H)) ∈ H.axioms
Instances
instance
LO.Propositional.Hilbert.instHasAxiomKrieselPutnamFormulaOfDecidableEqOfHasKrieselPutnam
{α : Type u_1}
{H : Hilbert α}
[DecidableEq α]
[H.HasKrieselPutnam]
:
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
- LO.Propositional.Hilbert.Int = { axioms := {LO.Axioms.EFQ (LO.Propositional.Formula.atom 0)} }
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Propositional.«term𝐈𝐧𝐭» = Lean.ParserDescr.node `LO.Propositional.«term𝐈𝐧𝐭» 1024 (Lean.ParserDescr.symbol "𝐈𝐧𝐭")
Instances For
Equations
- LO.Propositional.instHasEFQNatInt = { p := 0, mem_efq := LO.Propositional.instHasEFQNatInt._proof_1 }
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Propositional.«term𝐂𝐥» = Lean.ParserDescr.node `LO.Propositional.«term𝐂𝐥» 1024 (Lean.ParserDescr.symbol "𝐂𝐥")
Instances For
Equations
- LO.Propositional.instHasEFQNatCl = { p := 0, mem_efq := LO.Propositional.instHasEFQNatCl._proof_1 }
Equations
- LO.Propositional.instHasLEMNatCl = { p := 0, mem_lem := LO.Propositional.instHasLEMNatCl._proof_1 }
Equations
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Propositional.«term𝐊𝐂» = Lean.ParserDescr.node `LO.Propositional.«term𝐊𝐂» 1024 (Lean.ParserDescr.symbol "𝐊𝐂")
Instances For
Equations
- LO.Propositional.instHasEFQNatKC = { p := 0, mem_efq := LO.Propositional.instHasEFQNatKC._proof_1 }
Equations
- LO.Propositional.instHasWeakLEMNatKC = { p := 0, mem_wlem := LO.Propositional.instHasWeakLEMNatKC._proof_1 }
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Propositional.«term𝐋𝐂» = Lean.ParserDescr.node `LO.Propositional.«term𝐋𝐂» 1024 (Lean.ParserDescr.symbol "𝐋𝐂")
Instances For
Equations
- LO.Propositional.instHasEFQNatLC = { p := 0, mem_efq := LO.Propositional.instHasEFQNatLC._proof_1 }
Equations
- LO.Propositional.instHasDummettNatLC = { p := 0, q := 1, ne_pq := LO.Propositional.instHasDummettNatLC._proof_1, mem_dummet := LO.Propositional.instHasDummettNatLC._proof_2 }
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Propositional.«term𝐊𝐏» = Lean.ParserDescr.node `LO.Propositional.«term𝐊𝐏» 1024 (Lean.ParserDescr.symbol "𝐊𝐏")
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.