Documentation

Foundation.Propositional.Hilbert.WellKnown

source
class LO.Propositional.Hilbert.HasEFQ {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
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.
source
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.
source
class LO.Propositional.Hilbert.HasLEM {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
source
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.
source
class LO.Propositional.Hilbert.HasDNE {α : Type u_1} (H : Hilbert α) :
Type u_1
Instances
    source
    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.
    source
    class LO.Propositional.Hilbert.HasWeakLEM {α : Type u_1} (H : Hilbert α) :
    Type u_1
    Instances
    source
    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.
    source
    class LO.Propositional.Hilbert.HasDummett {α : Type u_1} (H : Hilbert α) :
    Type u_1
    Instances
    source
    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.
    source
    class LO.Propositional.Hilbert.HasKrieselPutnam {α : Type u_1} (H : Hilbert α) :
    Type u_1
    Instances
    source
    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.
    source
    @[reducible, inline]
    abbrev LO.Propositional.Hilbert.Int :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Propositional.Logic.Int :
    Logic ℕ
    Equations
    Instances For
    source
    instance LO.Propositional.instHasEFQNatInt :
    Hilbert.Int.HasEFQ
    Equations
    source
    instance LO.Propositional.instIntHilbertNatFormulaInt :
    Entailment.Int Hilbert.Int
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Propositional.Hilbert.Cl :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Propositional.Logic.Cl :
    Logic ℕ
    Equations
    Instances For
    source
    instance LO.Propositional.instHasEFQNatCl :
    Hilbert.Cl.HasEFQ
    Equations
    source
    instance LO.Propositional.instHasLEMNatCl :
    Hilbert.Cl.HasLEM
    Equations
    source
    instance LO.Propositional.instClHilbertNatFormulaCl :
    Entailment.Cl Hilbert.Cl
    Equations
    source
    theorem LO.Propositional.Hilbert.Int_weakerThan_Cl :
    Hilbert.Int ⪯ Hilbert.Cl
    source
    @[reducible, inline]
    abbrev LO.Propositional.Hilbert.KC :
    Hilbert ℕ
    Equations
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Propositional.Logic.KC :
    Logic ℕ
    Equations
    Instances For
    source
    instance LO.Propositional.instHasEFQNatKC :
    Hilbert.KC.HasEFQ
    Equations
    source
    instance LO.Propositional.instHasWeakLEMNatKC :
    Hilbert.KC.HasWeakLEM
    Equations
    source
    instance LO.Propositional.instKCHilbertNatFormulaKC :
    Entailment.KC Hilbert.KC
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Propositional.Hilbert.LC :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Propositional.Logic.LC :
    Logic ℕ
    Equations
    Instances For
    source
    instance LO.Propositional.instHasEFQNatLC :
    Hilbert.LC.HasEFQ
    Equations
    source
    instance LO.Propositional.instHasDummettNatLC :
    Hilbert.LC.HasDummett
    Equations
    source
    instance LO.Propositional.instLCHilbertNatFormulaLC :
    Entailment.LC Hilbert.LC
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev LO.Propositional.Hilbert.KP :
    Hilbert ℕ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
    source
    @[reducible, inline]
    abbrev LO.Propositional.Logic.KP :
    Logic ℕ
    Equations
    Instances For
    source
    instance LO.Propositional.instHasEFQNatKP :
    Hilbert.KP.HasEFQ
    Equations
    source
    instance LO.Propositional.instHasKrieselPutnamNatKP :
    Hilbert.KP.HasKrieselPutnam
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance LO.Propositional.instKPHilbertNatFormulaKP :
    Entailment.KP Hilbert.KP
    Equations
    • One or more equations did not get rendered due to their size.