structure LO.Propositional.Superintuitionistic.DeductionParameter (α : Type u_1) : Type u_1

• axiomSet : LO.Propositional.Superintuitionistic.AxiomSet α

def LO.Propositional.Superintuitionistic.«termAx(_)» : Lean.ParserDescr

Equations

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

class LO.Propositional.Superintuitionistic.DeductionParameter.IncludeEFQ {α : Type u} (𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α) : Type

• include_EFQ : 𝗘𝗙𝗤 ⊆ Ax(𝓓)

theorem LO.Propositional.Superintuitionistic.DeductionParameter.IncludeEFQ.include_EFQ {α : Type u} {𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} [self : 𝓓.IncludeEFQ] : 𝗘𝗙𝗤 ⊆ Ax(𝓓)

class LO.Propositional.Superintuitionistic.DeductionParameter.IncludeLEM {α : Type u} (𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α) : Type

• include_LEM : 𝗟𝗘𝗠 ⊆ Ax(𝓓)

theorem LO.Propositional.Superintuitionistic.DeductionParameter.IncludeLEM.include_LEM {α : Type u} {𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} [self : 𝓓.IncludeLEM] : 𝗟𝗘𝗠 ⊆ Ax(𝓓)

class LO.Propositional.Superintuitionistic.DeductionParameter.IncludeDNE {α : Type u} (𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α) : Type

• include_DNE : 𝗗𝗡𝗘 ⊆ Ax(𝓓)

theorem LO.Propositional.Superintuitionistic.DeductionParameter.IncludeDNE.include_DNE {α : Type u} {𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} [self : 𝓓.IncludeDNE] : 𝗗𝗡𝗘 ⊆ Ax(𝓓)

inductive LO.Propositional.Superintuitionistic.Deduction {α : Type u} (𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α) : LO.Propositional.Superintuitionistic.Formula α → Type u

• 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)

instance LO.Propositional.Superintuitionistic.instSystemFormulaDeductionParameter {α : Type u} : LO.System (LO.Propositional.Superintuitionistic.Formula α) (LO.Propositional.Superintuitionistic.DeductionParameter α)

Equations

• LO.Propositional.Superintuitionistic.instSystemFormulaDeductionParameter = { Prf := LO.Propositional.Superintuitionistic.Deduction }

instance LO.Propositional.Superintuitionistic.instMinimalDeductionParameterFormula {α : Type u} {𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} : LO.System.Minimal 𝓓

Equations

• LO.Propositional.Superintuitionistic.instMinimalDeductionParameterFormula = LO.System.Minimal.mk

instance LO.Propositional.Superintuitionistic.instHasAxiomEFQDeductionParameterFormulaOfIncludeEFQ {α : Type u} {𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} [𝓓.IncludeEFQ] : LO.System.HasAxiomEFQ 𝓓

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] : LO.System.HasAxiomLEM 𝓓

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] : LO.System.HasAxiomDNE 𝓓

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] : LO.System.Intuitionistic 𝓓

Equations

• LO.Propositional.Superintuitionistic.instIntuitionisticDeductionParameterFormulaOfIncludeEFQ = LO.System.Intuitionistic.mk

instance LO.Propositional.Superintuitionistic.instClassicalDeductionParameterFormulaOfIncludeDNE {α : Type u} {𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} [𝓓.IncludeDNE] : LO.System.Classical 𝓓

Equations

• LO.Propositional.Superintuitionistic.instClassicalDeductionParameterFormulaOfIncludeDNE = LO.System.Classical.mk

instance LO.Propositional.Superintuitionistic.instClassicalDeductionParameterFormulaOfIncludeEFQOfIncludeLEM {α : Type u} [DecidableEq α] {𝓓 : LO.Propositional.Superintuitionistic.DeductionParameter α} [𝓓.IncludeEFQ] [𝓓.IncludeLEM] : LO.System.Classical 𝓓

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]

abbrev LO.Propositional.Superintuitionistic.DeductionParameter.Minimal {α : Type u} : LO.Propositional.Superintuitionistic.DeductionParameter α

Equations

• LO.Propositional.Superintuitionistic.DeductionParameter.Minimal = { axiomSet := ∅ }

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.DeductionParameter.Intuitionistic {α : Type u} : LO.Propositional.Superintuitionistic.DeductionParameter α

Equations

• 𝐈𝐧𝐭 = { axiomSet := 𝗘𝗙𝗤 }

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

Equations

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

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} : LO.System.Intuitionistic 𝐈𝐧𝐭

Equations

• LO.Propositional.Superintuitionistic.DeductionParameter.instIntuitionisticFormulaIntuitionistic = LO.System.Intuitionistic.mk

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.DeductionParameter.Classical {α : Type u} : LO.Propositional.Superintuitionistic.DeductionParameter α

Equations

• 𝐂𝐥 = { axiomSet := 𝗘𝗙𝗤 ∪ 𝗟𝗘𝗠 }

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

Equations

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

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]

abbrev LO.Propositional.Superintuitionistic.DeductionParameter.KC {α : Type u} : LO.Propositional.Superintuitionistic.DeductionParameter α

Equations

• 𝐊𝐂 = { axiomSet := 𝗘𝗙𝗤 ∪ 𝗪𝗟𝗘𝗠 }

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

Equations

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

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} : LO.System.HasAxiomWeakLEM 𝐊𝐂

Equations

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

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.DeductionParameter.LC {α : Type u} : LO.Propositional.Superintuitionistic.DeductionParameter α

Equations

• 𝐋𝐂 = { axiomSet := 𝗘𝗙𝗤 ∪ 𝗗𝘂𝗺 }

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

Equations

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

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} : LO.System.HasAxiomDummett 𝐋𝐂

Equations

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

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.DeductionParameter.WeakMinimal {α : Type u} : LO.Propositional.Superintuitionistic.DeductionParameter α

Equations

• LO.Propositional.Superintuitionistic.DeductionParameter.WeakMinimal = { axiomSet := 𝗟𝗘𝗠 }

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.DeductionParameter.WeakClassical {α : Type u} : LO.Propositional.Superintuitionistic.DeductionParameter α

Equations

• LO.Propositional.Superintuitionistic.DeductionParameter.WeakClassical = { axiomSet := 𝗣𝗲 }

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.

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.Int_weaker_than_Cl {α : Type u} : 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥

theorem LO.Propositional.Superintuitionistic.Int_weaker_than_KC {α : Type u} : 𝐈𝐧𝐭 ≤ₛ 𝐊𝐂

theorem LO.Propositional.Superintuitionistic.Int_weaker_than_LC {α : Type u} : 𝐈𝐧𝐭 ≤ₛ 𝐋𝐂

theorem LO.Propositional.Superintuitionistic.KC_weaker_than_Cl {α : Type u} : 𝐊𝐂 ≤ₛ 𝐂𝐥

theorem LO.Propositional.Superintuitionistic.LC_weaker_than_Cl {α : Type u} [DecidableEq α] : 𝐋𝐂 ≤ₛ 𝐂𝐥

theorem LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable {α : Type u} [DecidableEq α] {p : LO.Propositional.Superintuitionistic.Formula α} : 𝐈𝐧𝐭 ⊢! ~~p ↔ 𝐂𝐥 ⊢! p

theorem LO.Propositional.Superintuitionistic.glivenko {α : Type u} [DecidableEq α] {p : LO.Propositional.Superintuitionistic.Formula α} : 𝐈𝐧𝐭 ⊢! ~~p ↔ 𝐂𝐥 ⊢! p

Alias of LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable.

theorem LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq {α : Type u} [DecidableEq α] {p : LO.Propositional.Superintuitionistic.Formula α} : 𝐈𝐧𝐭 ⊢! ~p ↔ 𝐂𝐥 ⊢! ~p