- axiomSet : LO.Propositional.Superintuitionistic.AxiomSet α
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
class
LO.Propositional.Superintuitionistic.DeductionParameter.IncludeEFQ
{α : Type u}
(Λ : LO.Propositional.Superintuitionistic.DeductionParameter α)
:
Instances
theorem
LO.Propositional.Superintuitionistic.DeductionParameter.IncludeEFQ.include_EFQ
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[self : Λ.IncludeEFQ]
:
class
LO.Propositional.Superintuitionistic.DeductionParameter.IncludeLEM
{α : Type u}
(Λ : LO.Propositional.Superintuitionistic.DeductionParameter α)
:
Instances
theorem
LO.Propositional.Superintuitionistic.DeductionParameter.IncludeLEM.include_LEM
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[self : Λ.IncludeLEM]
:
class
LO.Propositional.Superintuitionistic.DeductionParameter.IncludeDNE
{α : Type u}
(Λ : LO.Propositional.Superintuitionistic.DeductionParameter α)
:
Instances
theorem
LO.Propositional.Superintuitionistic.DeductionParameter.IncludeDNE.include_DNE
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[self : Λ.IncludeDNE]
:
inductive
LO.Propositional.Superintuitionistic.Deduction
{α : Type u}
(Λ : LO.Propositional.Superintuitionistic.DeductionParameter α)
:
- eaxm: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → {p : LO.Propositional.Superintuitionistic.Formula α} → p ∈ Ax(Λ) → LO.Propositional.Superintuitionistic.Deduction Λ p
- mdp: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → {p q : LO.Propositional.Superintuitionistic.Formula α} → LO.Propositional.Superintuitionistic.Deduction Λ (p ⟶ q) → LO.Propositional.Superintuitionistic.Deduction Λ p → LO.Propositional.Superintuitionistic.Deduction Λ q
- verum: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → LO.Propositional.Superintuitionistic.Deduction Λ ⊤
- imply₁: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p q : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ (p ⟶ q ⟶ p)
- imply₂: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p q r : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ ((p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r)
- and₁: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p q : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ (p ⋏ q ⟶ p)
- and₂: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p q : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ (p ⋏ q ⟶ q)
- and₃: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p q : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ (p ⟶ q ⟶ p ⋏ q)
- or₁: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p q : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ (p ⟶ p ⋎ q)
- or₂: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p q : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ (q ⟶ p ⋎ q)
- or₃: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p q r : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)
- neg_equiv: {α : Type u} → {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} → (p : LO.Propositional.Superintuitionistic.Formula α) → LO.Propositional.Superintuitionistic.Deduction Λ (LO.Axioms.NegEquiv p)
Instances For
Equations
- LO.Propositional.Superintuitionistic.instSystemFormulaDeductionParameter = { Prf := LO.Propositional.Superintuitionistic.Deduction }
instance
LO.Propositional.Superintuitionistic.instMinimalDeductionParameterFormula
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
:
Equations
- LO.Propositional.Superintuitionistic.instMinimalDeductionParameterFormula = LO.System.Minimal.mk
instance
LO.Propositional.Superintuitionistic.instHasAxiomEFQDeductionParameterFormulaOfIncludeEFQ
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[Λ.IncludeEFQ]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.Propositional.Superintuitionistic.instHasAxiomLEMDeductionParameterFormulaOfIncludeLEM
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[Λ.IncludeLEM]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.Propositional.Superintuitionistic.instHasAxiomDNEDeductionParameterFormulaOfIncludeDNE
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[Λ.IncludeDNE]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.Propositional.Superintuitionistic.instIntuitionisticDeductionParameterFormulaOfIncludeEFQ
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[Λ.IncludeEFQ]
:
Equations
- LO.Propositional.Superintuitionistic.instIntuitionisticDeductionParameterFormulaOfIncludeEFQ = LO.System.Intuitionistic.mk
instance
LO.Propositional.Superintuitionistic.instClassicalDeductionParameterFormulaOfIncludeDNE
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[Λ.IncludeDNE]
:
Equations
- LO.Propositional.Superintuitionistic.instClassicalDeductionParameterFormulaOfIncludeDNE = LO.System.Classical.mk
instance
LO.Propositional.Superintuitionistic.instClassicalDeductionParameterFormulaOfIncludeEFQOfIncludeLEM
{α : Type u}
[DecidableEq α]
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
[Λ.IncludeEFQ]
[Λ.IncludeLEM]
:
Equations
- LO.Propositional.Superintuitionistic.instClassicalDeductionParameterFormulaOfIncludeEFQOfIncludeLEM = LO.System.Classical.mk
theorem
LO.Propositional.Superintuitionistic.DeductionParameter.eaxm!
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
{p : LO.Propositional.Superintuitionistic.Formula α}
(h : p ∈ Ax(Λ))
:
Λ ⊢! p
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.«term𝐈𝐧𝐭» = Lean.ParserDescr.node `LO.Propositional.Superintuitionistic.DeductionParameter.term𝐈𝐧𝐭 1024 (Lean.ParserDescr.symbol "𝐈𝐧𝐭")
Instances For
instance
LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeEFQIntuitionistic
{α : Type u}
:
𝐈𝐧𝐭.IncludeEFQ
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeEFQIntuitionistic = { include_EFQ := ⋯ }
instance
LO.Propositional.Superintuitionistic.DeductionParameter.instIntuitionisticFormulaIntuitionistic
{α : Type u}
:
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.instIntuitionisticFormulaIntuitionistic = LO.System.Intuitionistic.mk
@[reducible, inline]
Instances For
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.«term𝐂𝐥» = Lean.ParserDescr.node `LO.Propositional.Superintuitionistic.DeductionParameter.term𝐂𝐥 1024 (Lean.ParserDescr.symbol "𝐂𝐥")
Instances For
instance
LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeLEMClassical
{α : Type u}
:
𝐂𝐥.IncludeLEM
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeLEMClassical = { include_LEM := ⋯ }
instance
LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeEFQClassical
{α : Type u}
:
𝐂𝐥.IncludeEFQ
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeEFQClassical = { include_EFQ := ⋯ }
@[reducible, inline]
Instances For
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.«term𝐊𝐂» = Lean.ParserDescr.node `LO.Propositional.Superintuitionistic.DeductionParameter.term𝐊𝐂 1024 (Lean.ParserDescr.symbol "𝐊𝐂")
Instances For
instance
LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeEFQKC
{α : Type u}
:
𝐊𝐂.IncludeEFQ
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeEFQKC = { include_EFQ := ⋯ }
instance
LO.Propositional.Superintuitionistic.DeductionParameter.instHasAxiomWeakLEMFormulaKC
{α : Type u}
:
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
Instances For
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.«term𝐋𝐂» = Lean.ParserDescr.node `LO.Propositional.Superintuitionistic.DeductionParameter.term𝐋𝐂 1024 (Lean.ParserDescr.symbol "𝐋𝐂")
Instances For
instance
LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeEFQLC
{α : Type u}
:
𝐋𝐂.IncludeEFQ
Equations
- LO.Propositional.Superintuitionistic.DeductionParameter.instIncludeEFQLC = { include_EFQ := ⋯ }
instance
LO.Propositional.Superintuitionistic.DeductionParameter.instHasAxiomDummettFormulaLC
{α : Type u}
:
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
noncomputable def
LO.Propositional.Superintuitionistic.Deduction.rec!
{α : Type u}
{Λ : LO.Propositional.Superintuitionistic.DeductionParameter α}
{motive : (a : LO.Propositional.Superintuitionistic.Formula α) → Λ ⊢! a → Sort u_1}
(eaxm : {p : LO.Propositional.Superintuitionistic.Formula α} → (a : p ∈ Ax(Λ)) → motive p ⋯)
(mdp : {p q : LO.Propositional.Superintuitionistic.Formula α} →
{hpq : Λ ⊢! p ⟶ q} → {hp : Λ ⊢! p} → motive (p ⟶ q) hpq → motive p hp → motive q ⋯)
(verum : motive ⊤ ⋯)
(imply₁ : {p q : LO.Propositional.Superintuitionistic.Formula α} → motive (p ⟶ q ⟶ p) ⋯)
(imply₂ : {p q r : LO.Propositional.Superintuitionistic.Formula α} → motive ((p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r) ⋯)
(and₁ : {p q : LO.Propositional.Superintuitionistic.Formula α} → motive (p ⋏ q ⟶ p) ⋯)
(and₂ : {p q : LO.Propositional.Superintuitionistic.Formula α} → motive (p ⋏ q ⟶ q) ⋯)
(and₃ : {p q : LO.Propositional.Superintuitionistic.Formula α} → motive (p ⟶ q ⟶ p ⋏ q) ⋯)
(or₁ : {p q : LO.Propositional.Superintuitionistic.Formula α} → motive (p ⟶ p ⋎ q) ⋯)
(or₂ : {p q : LO.Propositional.Superintuitionistic.Formula α} → motive (q ⟶ p ⋎ q) ⋯)
(or₃ : {p q r : LO.Propositional.Superintuitionistic.Formula α} → motive ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r) ⋯)
(neg_equiv : {p : LO.Propositional.Superintuitionistic.Formula α} → motive (LO.Axioms.NegEquiv p) ⋯)
{a : LO.Propositional.Superintuitionistic.Formula α}
(t : Λ ⊢! a)
:
motive a t
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Propositional.Superintuitionistic.weaker_than_of_subset_axiomset'
{α : Type u}
{Λ₁ : LO.Propositional.Superintuitionistic.DeductionParameter α}
{Λ₂ : LO.Propositional.Superintuitionistic.DeductionParameter α}
(hMaxm : ∀ {p : LO.Propositional.Superintuitionistic.Formula α}, p ∈ Ax(Λ₁) → Λ₂ ⊢! p)
:
Λ₁ ≤ₛ Λ₂
theorem
LO.Propositional.Superintuitionistic.weaker_than_of_subset_axiomset
{α : Type u}
{Λ₁ : LO.Propositional.Superintuitionistic.DeductionParameter α}
{Λ₂ : LO.Propositional.Superintuitionistic.DeductionParameter α}
(hSubset : autoParam (Ax(Λ₁) ⊆ Ax(Λ₂)) _auto✝)
:
Λ₁ ≤ₛ Λ₂
theorem
LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
{α : Type u}
[DecidableEq α]
{p : LO.Propositional.Superintuitionistic.Formula α}
: