def LO.System.mdp_in {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} : 𝓢 ⊢ p ⋏ (p ➝ q) ➝ q

Equations

• LO.System.mdp_in = LO.System.FiniteContext.deduct' (let_fun hp := LO.System.FiniteContext.byAxm ⋯; let_fun hpq := LO.System.FiniteContext.byAxm ⋯; hpq⨀hp)

theorem LO.System.mdp_in! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} : 𝓢 ⊢! p ⋏ (p ➝ q) ➝ q

def LO.System.bot_of_mem_either {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} [LO.System.NegationEquiv 𝓢] (h₁ : p ∈ Γ) (h₂ : ∼p ∈ Γ) : Γ ⊢[𝓢] ⊥

Equations

• LO.System.bot_of_mem_either h₁ h₂ = let_fun hp := LO.System.FiniteContext.byAxm h₁; let_fun hnp := LO.System.neg_equiv'.mp (LO.System.FiniteContext.byAxm h₂); hnp⨀hp

@[simp]

theorem LO.System.bot_of_mem_either! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} [LO.System.NegationEquiv 𝓢] (h₁ : p ∈ Γ) (h₂ : ∼p ∈ Γ) : Γ ⊢[𝓢]! ⊥

def LO.System.efq_of_mem_either {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {Γ : List F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] (h₁ : p ∈ Γ) (h₂ : ∼p ∈ Γ) : Γ ⊢[𝓢] q

Equations

• LO.System.efq_of_mem_either h₁ h₂ = LO.System.efq' (LO.System.bot_of_mem_either h₁ h₂)

@[simp]

theorem LO.System.efq_of_mem_either! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {Γ : List F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] (h₁ : p ∈ Γ) (h₂ : ∼p ∈ Γ) : Γ ⊢[𝓢]! q

def LO.System.efq_imply_not₁ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢ ∼p ➝ p ➝ q

Equations

• LO.System.efq_imply_not₁ = LO.System.FiniteContext.deduct' (LO.System.FiniteContext.deduct (LO.System.efq_of_mem_either ⋯ ⋯))

@[simp]

theorem LO.System.efq_imply_not₁! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢! ∼p ➝ p ➝ q

def LO.System.efq_imply_not₂ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢ p ➝ ∼p ➝ q

Equations

• LO.System.efq_imply_not₂ = LO.System.FiniteContext.deduct' (LO.System.FiniteContext.deduct (LO.System.efq_of_mem_either ⋯ ⋯))

@[simp]

theorem LO.System.efq_imply_not₂! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢! p ➝ ∼p ➝ q

theorem LO.System.efq_of_neg! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] (h : 𝓢 ⊢! ∼p) : 𝓢 ⊢! p ➝ q

theorem LO.System.efq_of_neg₂! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] (h : 𝓢 ⊢! p) : 𝓢 ⊢! ∼p ➝ q

def LO.System.neg_mdp {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (hnp : 𝓢 ⊢ ∼p) (hn : 𝓢 ⊢ p) : 𝓢 ⊢ ⊥

Equations

• LO.System.neg_mdp hnp hn = LO.System.neg_equiv'.mp hnp⨀hn

theorem LO.System.neg_mdp! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (hnp : 𝓢 ⊢! ∼p) (hn : 𝓢 ⊢! p) : 𝓢 ⊢! ⊥

def LO.System.dneOr {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.HasAxiomDNE 𝓢] (d : 𝓢 ⊢ ∼∼p ⋎ ∼∼q) : 𝓢 ⊢ p ⋎ q

Equations

• LO.System.dneOr d = LO.System.or₃''' (LO.System.impTrans'' LO.System.dne LO.System.or₁) (LO.System.impTrans'' LO.System.dne LO.System.or₂) d

def LO.System.implyLeftOr' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢ p ➝ r) : 𝓢 ⊢ p ➝ r ⋎ q

Equations

• LO.System.implyLeftOr' h = LO.System.FiniteContext.deduct' (LO.System.or₁' (LO.System.FiniteContext.deductInv (LO.System.FiniteContext.of h)))

theorem LO.System.imply_left_or'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! p ➝ r) : 𝓢 ⊢! p ➝ r ⋎ q

def LO.System.implyRightOr' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢ q ➝ r) : 𝓢 ⊢ q ➝ p ⋎ r

Equations

• LO.System.implyRightOr' h = LO.System.FiniteContext.deduct' (LO.System.or₂' (LO.System.FiniteContext.deductInv (LO.System.FiniteContext.of h)))

theorem LO.System.imply_right_or'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! q ➝ r) : 𝓢 ⊢! q ➝ p ⋎ r

def LO.System.implyRightAnd {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hq : 𝓢 ⊢ p ➝ q) (hr : 𝓢 ⊢ p ➝ r) : 𝓢 ⊢ p ➝ q ⋏ r

Equations

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

theorem LO.System.imply_right_and! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hq : 𝓢 ⊢! p ➝ q) (hr : 𝓢 ⊢! p ➝ r) : 𝓢 ⊢! p ➝ q ⋏ r

theorem LO.System.imply_left_and_comm'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (d : 𝓢 ⊢! p ⋏ q ➝ r) : 𝓢 ⊢! q ⋏ p ➝ r

theorem LO.System.dhyp_and_left! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! p ➝ r) : 𝓢 ⊢! q ⋏ p ➝ r

theorem LO.System.dhyp_and_right! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! p ➝ r) : 𝓢 ⊢! p ⋏ q ➝ r

theorem LO.System.cut! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {c : F} {q₁ : F} {p₂ : F} {q₂ : F} (d₁ : 𝓢 ⊢! p₁ ⋏ c ➝ q₁) (d₂ : 𝓢 ⊢! p₂ ➝ c ⋎ q₂) : 𝓢 ⊢! p₁ ⋏ p₂ ➝ q₁ ⋎ q₂

@[simp]

theorem LO.System.imply_left_verum {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} : 𝓢 ⊢! p ➝ ⊤

def LO.System.orComm {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} : 𝓢 ⊢ p ⋎ q ➝ q ⋎ p

Equations

• LO.System.orComm = LO.System.FiniteContext.deduct' (LO.System.or₃''' LO.System.or₂ LO.System.or₁ LO.System.FiniteContext.id)

theorem LO.System.or_comm! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} : 𝓢 ⊢! p ⋎ q ➝ q ⋎ p

def LO.System.orComm' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} (h : 𝓢 ⊢ p ⋎ q) : 𝓢 ⊢ q ⋎ p

Equations

• LO.System.orComm' h = LO.System.orComm⨀h

theorem LO.System.or_comm'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} (h : 𝓢 ⊢! p ⋎ q) : 𝓢 ⊢! q ⋎ p

theorem LO.System.or_assoc'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} : 𝓢 ⊢! p ⋎ q ⋎ r ↔ 𝓢 ⊢! (p ⋎ q) ⋎ r

theorem LO.System.and_assoc! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} : 𝓢 ⊢! (p ⋏ q) ⋏ r ⭤ p ⋏ q ⋏ r

def LO.System.andReplaceLeft' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hc : 𝓢 ⊢ p ⋏ q) (h : 𝓢 ⊢ p ➝ r) : 𝓢 ⊢ r ⋏ q

Equations

• LO.System.andReplaceLeft' hc h = LO.System.and₃' (h⨀LO.System.and₁' hc) (LO.System.and₂' hc)

theorem LO.System.and_replace_left'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hc : 𝓢 ⊢! p ⋏ q) (h : 𝓢 ⊢! p ➝ r) : 𝓢 ⊢! r ⋏ q

def LO.System.andReplaceLeft {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢ p ➝ r) : 𝓢 ⊢ p ⋏ q ➝ r ⋏ q

Equations

• LO.System.andReplaceLeft h = LO.System.FiniteContext.deduct' (LO.System.andReplaceLeft' LO.System.FiniteContext.id (LO.System.FiniteContext.of h))

theorem LO.System.and_replace_left! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! p ➝ r) : 𝓢 ⊢! p ⋏ q ➝ r ⋏ q

def LO.System.andReplaceRight' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hc : 𝓢 ⊢ p ⋏ q) (h : 𝓢 ⊢ q ➝ r) : 𝓢 ⊢ p ⋏ r

Equations

• LO.System.andReplaceRight' hc h = LO.System.and₃' (LO.System.and₁' hc) (h⨀LO.System.and₂' hc)

theorem LO.System.andReplaceRight'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hc : 𝓢 ⊢! p ⋏ q) (h : 𝓢 ⊢! q ➝ r) : 𝓢 ⊢! p ⋏ r

def LO.System.andReplaceRight {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢ q ➝ r) : 𝓢 ⊢ p ⋏ q ➝ p ⋏ r

Equations

• LO.System.andReplaceRight h = LO.System.FiniteContext.deduct' (LO.System.andReplaceRight' LO.System.FiniteContext.id (LO.System.FiniteContext.of h))

theorem LO.System.and_replace_right! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! q ➝ r) : 𝓢 ⊢! p ⋏ q ➝ p ⋏ r

def LO.System.andReplace' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} {s : F} (hc : 𝓢 ⊢ p ⋏ q) (h₁ : 𝓢 ⊢ p ➝ r) (h₂ : 𝓢 ⊢ q ➝ s) : 𝓢 ⊢ r ⋏ s

Equations

• LO.System.andReplace' hc h₁ h₂ = LO.System.andReplaceRight' (LO.System.andReplaceLeft' hc h₁) h₂

theorem LO.System.and_replace'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} {s : F} (hc : 𝓢 ⊢! p ⋏ q) (h₁ : 𝓢 ⊢! p ➝ r) (h₂ : 𝓢 ⊢! q ➝ s) : 𝓢 ⊢! r ⋏ s

def LO.System.andReplace {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} {s : F} (h₁ : 𝓢 ⊢ p ➝ r) (h₂ : 𝓢 ⊢ q ➝ s) : 𝓢 ⊢ p ⋏ q ➝ r ⋏ s

Equations

• LO.System.andReplace h₁ h₂ = LO.System.FiniteContext.deduct' (LO.System.andReplace' LO.System.FiniteContext.id (LO.System.FiniteContext.of h₁) (LO.System.FiniteContext.of h₂))

theorem LO.System.and_replace! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} {s : F} (h₁ : 𝓢 ⊢! p ➝ r) (h₂ : 𝓢 ⊢! q ➝ s) : 𝓢 ⊢! p ⋏ q ➝ r ⋏ s

def LO.System.orReplaceLeft' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hc : 𝓢 ⊢ p ⋎ q) (hp : 𝓢 ⊢ p ➝ r) : 𝓢 ⊢ r ⋎ q

Equations

• LO.System.orReplaceLeft' hc hp = LO.System.or₃''' (LO.System.impTrans'' hp LO.System.or₁) LO.System.or₂ hc

theorem LO.System.or_replace_left'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hc : 𝓢 ⊢! p ⋎ q) (hp : 𝓢 ⊢! p ➝ r) : 𝓢 ⊢! r ⋎ q

def LO.System.orReplaceLeft {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hp : 𝓢 ⊢ p ➝ r) : 𝓢 ⊢ p ⋎ q ➝ r ⋎ q

Equations

• LO.System.orReplaceLeft hp = LO.System.FiniteContext.deduct' (LO.System.orReplaceLeft' LO.System.FiniteContext.id (LO.System.FiniteContext.of hp))

theorem LO.System.or_replace_left! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hp : 𝓢 ⊢! p ➝ r) : 𝓢 ⊢! p ⋎ q ➝ r ⋎ q

def LO.System.orReplaceRight' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hc : 𝓢 ⊢ p ⋎ q) (hq : 𝓢 ⊢ q ➝ r) : 𝓢 ⊢ p ⋎ r

Equations

• LO.System.orReplaceRight' hc hq = LO.System.or₃''' LO.System.or₁ (LO.System.impTrans'' hq LO.System.or₂) hc

theorem LO.System.or_replace_right'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hc : 𝓢 ⊢! p ⋎ q) (hq : 𝓢 ⊢! q ➝ r) : 𝓢 ⊢! p ⋎ r

def LO.System.orReplaceRight {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hq : 𝓢 ⊢ q ➝ r) : 𝓢 ⊢ p ⋎ q ➝ p ⋎ r

Equations

• LO.System.orReplaceRight hq = LO.System.FiniteContext.deduct' (LO.System.orReplaceRight' LO.System.FiniteContext.id (LO.System.FiniteContext.of hq))

theorem LO.System.or_replace_right! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (hq : 𝓢 ⊢! q ➝ r) : 𝓢 ⊢! p ⋎ q ➝ p ⋎ r

def LO.System.orReplace' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {q₁ : F} {p₂ : F} {q₂ : F} (h : 𝓢 ⊢ p₁ ⋎ q₁) (hp : 𝓢 ⊢ p₁ ➝ p₂) (hq : 𝓢 ⊢ q₁ ➝ q₂) : 𝓢 ⊢ p₂ ⋎ q₂

Equations

• LO.System.orReplace' h hp hq = LO.System.orReplaceRight' (LO.System.orReplaceLeft' h hp) hq

theorem LO.System.or_replace'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {q₁ : F} {p₂ : F} {q₂ : F} (h : 𝓢 ⊢! p₁ ⋎ q₁) (hp : 𝓢 ⊢! p₁ ➝ p₂) (hq : 𝓢 ⊢! q₁ ➝ q₂) : 𝓢 ⊢! p₂ ⋎ q₂

def LO.System.orReplace {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢ p₁ ➝ p₂) (hq : 𝓢 ⊢ q₁ ➝ q₂) : 𝓢 ⊢ p₁ ⋎ q₁ ➝ p₂ ⋎ q₂

Equations

• LO.System.orReplace hp hq = LO.System.FiniteContext.deduct' (LO.System.orReplace' LO.System.FiniteContext.id (LO.System.FiniteContext.of hp) (LO.System.FiniteContext.of hq))

theorem LO.System.or_replace! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢! p₁ ➝ p₂) (hq : 𝓢 ⊢! q₁ ➝ q₂) : 𝓢 ⊢! p₁ ⋎ q₁ ➝ p₂ ⋎ q₂

def LO.System.orReplaceIff {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢ p₁ ⭤ p₂) (hq : 𝓢 ⊢ q₁ ⭤ q₂) : 𝓢 ⊢ p₁ ⋎ q₁ ⭤ p₂ ⋎ q₂

Equations

• LO.System.orReplaceIff hp hq = LO.System.iffIntro (LO.System.orReplace (LO.System.and₁' hp) (LO.System.and₁' hq)) (LO.System.orReplace (LO.System.and₂' hp) (LO.System.and₂' hq))

theorem LO.System.or_replace_iff! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢! p₁ ⭤ p₂) (hq : 𝓢 ⊢! q₁ ⭤ q₂) : 𝓢 ⊢! p₁ ⋎ q₁ ⭤ p₂ ⋎ q₂

theorem LO.System.or_assoc! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} : 𝓢 ⊢! p ⋎ q ⋎ r ⭤ (p ⋎ q) ⋎ r

theorem LO.System.or_replace_right_iff! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (d : 𝓢 ⊢! q ⭤ r) : 𝓢 ⊢! p ⋎ q ⭤ p ⋎ r

theorem LO.System.or_replace_left_iff! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (d : 𝓢 ⊢! p ⭤ r) : 𝓢 ⊢! p ⋎ q ⭤ r ⋎ q

def LO.System.andReplaceIff {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢ p₁ ⭤ p₂) (hq : 𝓢 ⊢ q₁ ⭤ q₂) : 𝓢 ⊢ p₁ ⋏ q₁ ⭤ p₂ ⋏ q₂

Equations

• LO.System.andReplaceIff hp hq = LO.System.iffIntro (LO.System.andReplace (LO.System.and₁' hp) (LO.System.and₁' hq)) (LO.System.andReplace (LO.System.and₂' hp) (LO.System.and₂' hq))

theorem LO.System.and_replace_iff! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢! p₁ ⭤ p₂) (hq : 𝓢 ⊢! q₁ ⭤ q₂) : 𝓢 ⊢! p₁ ⋏ q₁ ⭤ p₂ ⋏ q₂

def LO.System.impReplaceIff {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢ p₁ ⭤ p₂) (hq : 𝓢 ⊢ q₁ ⭤ q₂) : 𝓢 ⊢ (p₁ ➝ q₁) ⭤ (p₂ ➝ q₂)

Equations

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

theorem LO.System.imp_replace_iff! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢! p₁ ⭤ p₂) (hq : 𝓢 ⊢! q₁ ⭤ q₂) : 𝓢 ⊢! (p₁ ➝ q₁) ⭤ (p₂ ➝ q₂)

theorem LO.System.imp_replace_iff!' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p₁ : F} {p₂ : F} {q₁ : F} {q₂ : F} (hp : 𝓢 ⊢! p₁ ⭤ p₂) (hq : 𝓢 ⊢! q₁ ⭤ q₂) : 𝓢 ⊢! p₁ ➝ q₁ ↔ 𝓢 ⊢! p₂ ➝ q₂

def LO.System.dni {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ p ➝ ∼∼p

Equations

• LO.System.dni = LO.System.FiniteContext.deduct' (LO.System.neg_equiv'.mpr (LO.System.FiniteContext.deduct (LO.System.bot_of_mem_either ⋯ ⋯)))

@[simp]

theorem LO.System.dni! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! p ➝ ∼∼p

def LO.System.dni' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢ p) : 𝓢 ⊢ ∼∼p

Equations

• LO.System.dni' b = LO.System.dni⨀b

theorem LO.System.dni'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢! p) : 𝓢 ⊢! ∼∼p

def LO.System.dniOr' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (d : 𝓢 ⊢ p ⋎ q) : 𝓢 ⊢ ∼∼p ⋎ ∼∼q

Equations

• LO.System.dniOr' d = LO.System.or₃''' (LO.System.impTrans'' LO.System.dni LO.System.or₁) (LO.System.impTrans'' LO.System.dni LO.System.or₂) d

theorem LO.System.dni_or'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (d : 𝓢 ⊢! p ⋎ q) : 𝓢 ⊢! ∼∼p ⋎ ∼∼q

def LO.System.dniAnd' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (d : 𝓢 ⊢ p ⋏ q) : 𝓢 ⊢ ∼∼p ⋏ ∼∼q

Equations

• LO.System.dniAnd' d = LO.System.and₃' (LO.System.dni' (LO.System.and₁' d)) (LO.System.dni' (LO.System.and₂' d))

theorem LO.System.dni_and'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (d : 𝓢 ⊢! p ⋏ q) : 𝓢 ⊢! ∼∼p ⋏ ∼∼q

def LO.System.dn {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢ p ⭤ ∼∼p

Equations

• LO.System.dn = LO.System.iffIntro LO.System.dni LO.System.dne

@[simp]

theorem LO.System.dn! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢! p ⭤ ∼∼p

def LO.System.contra₀ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ (p ➝ q) ➝ ∼q ➝ ∼p

Equations

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

@[simp]

def LO.System.contra₀! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! (p ➝ q) ➝ ∼q ➝ ∼p

Equations

• ⋯ = ⋯

def LO.System.contra₀' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢ p ➝ q) : 𝓢 ⊢ ∼q ➝ ∼p

Equations

• LO.System.contra₀' b = LO.System.contra₀⨀b

theorem LO.System.contra₀'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢! p ➝ q) : 𝓢 ⊢! ∼q ➝ ∼p

def LO.System.contra₀x2' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢ p ➝ q) : 𝓢 ⊢ ∼∼p ➝ ∼∼q

Equations

• LO.System.contra₀x2' b = LO.System.contra₀' (LO.System.contra₀' b)

theorem LO.System.contra₀x2'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢! p ➝ q) : 𝓢 ⊢! ∼∼p ➝ ∼∼q

def LO.System.contra₀x2 {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ (p ➝ q) ➝ ∼∼p ➝ ∼∼q

Equations

• LO.System.contra₀x2 = LO.System.FiniteContext.deduct' (LO.System.contra₀x2' LO.System.FiniteContext.id)

@[simp]

theorem LO.System.contra₀x2! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! (p ➝ q) ➝ ∼∼p ➝ ∼∼q

def LO.System.contra₁' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢ p ➝ ∼q) : 𝓢 ⊢ q ➝ ∼p

Equations

• LO.System.contra₁' b = LO.System.impTrans'' LO.System.dni (LO.System.contra₀' b)

theorem LO.System.contra₁'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢! p ➝ ∼q) : 𝓢 ⊢! q ➝ ∼p

def LO.System.contra₁ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ (p ➝ ∼q) ➝ q ➝ ∼p

Equations

• LO.System.contra₁ = LO.System.FiniteContext.deduct' (LO.System.contra₁' LO.System.FiniteContext.id)

theorem LO.System.contra₁! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! (p ➝ ∼q) ➝ q ➝ ∼p

def LO.System.contra₂' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (b : 𝓢 ⊢ ∼p ➝ q) : 𝓢 ⊢ ∼q ➝ p

Equations

• LO.System.contra₂' b = LO.System.impTrans'' (LO.System.contra₀' b) LO.System.dne

theorem LO.System.contra₂'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (b : 𝓢 ⊢! ∼p ➝ q) : 𝓢 ⊢! ∼q ➝ p

def LO.System.contra₂ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢ (∼p ➝ q) ➝ ∼q ➝ p

Equations

• LO.System.contra₂ = LO.System.FiniteContext.deduct' (LO.System.contra₂' LO.System.FiniteContext.id)

@[simp]

theorem LO.System.contra₂! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢! (∼p ➝ q) ➝ ∼q ➝ p

def LO.System.contra₃' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (b : 𝓢 ⊢ ∼p ➝ ∼q) : 𝓢 ⊢ q ➝ p

Equations

• LO.System.contra₃' b = LO.System.impTrans'' LO.System.dni (LO.System.contra₂' b)

theorem LO.System.contra₃'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (b : 𝓢 ⊢! ∼p ➝ ∼q) : 𝓢 ⊢! q ➝ p

def LO.System.contra₃ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢ (∼p ➝ ∼q) ➝ q ➝ p

Equations

• LO.System.contra₃ = LO.System.FiniteContext.deduct' (LO.System.contra₃' LO.System.FiniteContext.id)

@[simp]

theorem LO.System.contra₃! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢! (∼p ➝ ∼q) ➝ q ➝ p

def LO.System.negReplaceIff' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢ p ⭤ q) : 𝓢 ⊢ ∼p ⭤ ∼q

Equations

• LO.System.negReplaceIff' b = LO.System.iffIntro (LO.System.contra₀' (LO.System.and₂' b)) (LO.System.contra₀' (LO.System.and₁' b))

theorem LO.System.neg_replace_iff'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢! p ⭤ q) : 𝓢 ⊢! ∼p ⭤ ∼q

def LO.System.iffNegLeftToRight' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (h : 𝓢 ⊢ p ⭤ ∼q) : 𝓢 ⊢ ∼p ⭤ q

Equations

• LO.System.iffNegLeftToRight' h = LO.System.iffIntro (LO.System.contra₂' (LO.System.and₂' h)) (LO.System.contra₁' (LO.System.and₁' h))

theorem LO.System.iff_neg_left_to_right'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (h : 𝓢 ⊢! p ⭤ ∼q) : 𝓢 ⊢! ∼p ⭤ q

def LO.System.iffNegRightToLeft' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (h : 𝓢 ⊢ ∼p ⭤ q) : 𝓢 ⊢ p ⭤ ∼q

Equations

• LO.System.iffNegRightToLeft' h = LO.System.iffComm' (LO.System.iffNegLeftToRight' (LO.System.iffComm' h))

theorem LO.System.iff_neg_right_to_left'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (h : 𝓢 ⊢! ∼p ⭤ q) : 𝓢 ⊢! p ⭤ ∼q

def LO.System.negneg_equiv {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ ∼∼p ⭤ ((p ➝ ⊥) ➝ ⊥)

Equations

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

@[simp]

theorem LO.System.negneg_equiv! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! ∼∼p ⭤ ((p ➝ ⊥) ➝ ⊥)

def LO.System.negneg_equiv_dne {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢ p ⭤ ((p ➝ ⊥) ➝ ⊥)

Equations

• LO.System.negneg_equiv_dne = LO.System.iffTrans'' LO.System.dn LO.System.negneg_equiv

theorem LO.System.negneg_equiv_dne! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢! p ⭤ ((p ➝ ⊥) ➝ ⊥)

def LO.System.elim_contra_neg {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomElimContra 𝓢] : 𝓢 ⊢ ((q ➝ ⊥) ➝ p ➝ ⊥) ➝ p ➝ q

Equations

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

theorem LO.System.elim_contra_neg! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomElimContra 𝓢] : 𝓢 ⊢! ((q ➝ ⊥) ➝ p ➝ ⊥) ➝ p ➝ q

def LO.System.tne {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ ∼∼∼p ➝ ∼p

Equations

• LO.System.tne = LO.System.contra₀' LO.System.dni

@[simp]

theorem LO.System.tne! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! ∼∼∼p ➝ ∼p

def LO.System.tne' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢ ∼∼∼p) : 𝓢 ⊢ ∼p

Equations

• LO.System.tne' b = LO.System.tne⨀b

theorem LO.System.tne'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢! ∼∼∼p) : 𝓢 ⊢! ∼p

def LO.System.implyLeftReplace {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢ q ➝ p) : 𝓢 ⊢ (p ➝ r) ➝ q ➝ r

Equations

• LO.System.implyLeftReplace h = LO.System.FiniteContext.deduct' (LO.System.impTrans'' (LO.System.FiniteContext.of h) LO.System.FiniteContext.id)

theorem LO.System.replace_imply_left! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! q ➝ p) : 𝓢 ⊢! (p ➝ r) ➝ q ➝ r

theorem LO.System.replace_imply_left_by_iff'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! p ⭤ q) : 𝓢 ⊢! p ➝ r ↔ 𝓢 ⊢! q ➝ r

theorem LO.System.replace_imply_right_by_iff'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! p ⭤ q) : 𝓢 ⊢! r ➝ p ↔ 𝓢 ⊢! r ➝ q

def LO.System.impSwap' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢ p ➝ q ➝ r) : 𝓢 ⊢ q ➝ p ➝ r

Equations

• LO.System.impSwap' h = LO.System.FiniteContext.deduct' (LO.System.FiniteContext.deduct (LO.System.FiniteContext.of h⨀LO.System.FiniteContext.byAxm ⋯⨀LO.System.FiniteContext.byAxm ⋯))

theorem LO.System.imp_swap'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! p ➝ q ➝ r) : 𝓢 ⊢! q ➝ p ➝ r

def LO.System.impSwap {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} : 𝓢 ⊢ (p ➝ q ➝ r) ➝ q ➝ p ➝ r

Equations

• LO.System.impSwap = LO.System.FiniteContext.deduct' (LO.System.impSwap' LO.System.FiniteContext.id)

@[simp]

theorem LO.System.imp_swap! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} : 𝓢 ⊢! (p ➝ q ➝ r) ➝ q ➝ p ➝ r

def LO.System.ppq {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} (h : 𝓢 ⊢ p ➝ p ➝ q) : 𝓢 ⊢ p ➝ q

Equations

• LO.System.ppq h = LO.System.FiniteContext.deduct' (let_fun this := LO.System.FiniteContext.of h; this⨀LO.System.FiniteContext.byAxm ⋯⨀LO.System.FiniteContext.byAxm ⋯)

theorem LO.System.ppq! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} (h : 𝓢 ⊢! p ➝ p ➝ q) : 𝓢 ⊢! p ➝ q

def LO.System.p_pq_q {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} : 𝓢 ⊢ p ➝ (p ➝ q) ➝ q

Equations

• LO.System.p_pq_q = LO.System.impSwap' (LO.System.impId (p ➝ q))

theorem LO.System.p_pq_q! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} : 𝓢 ⊢! p ➝ (p ➝ q) ➝ q

def LO.System.dhyp_imp' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢ p ➝ q) : 𝓢 ⊢ (r ➝ p) ➝ r ➝ q

Equations

• LO.System.dhyp_imp' h = LO.System.imply₂⨀LO.System.dhyp r h

theorem LO.System.dhyp_imp'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! p ➝ q) : 𝓢 ⊢! (r ➝ p) ➝ r ➝ q

def LO.System.rev_dhyp_imp' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢ q ➝ p) : 𝓢 ⊢ (p ➝ r) ➝ q ➝ r

Equations

• LO.System.rev_dhyp_imp' h = LO.System.impSwap' (LO.System.impTrans'' h LO.System.p_pq_q)

theorem LO.System.rev_dhyp_imp'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {r : F} (h : 𝓢 ⊢! q ➝ p) : 𝓢 ⊢! (p ➝ r) ➝ q ➝ r

noncomputable def LO.System.dnDistributeImply {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ ∼∼(p ➝ q) ➝ ∼∼p ➝ ∼∼q

Equations

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

@[simp]

theorem LO.System.dn_distribute_imply! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! ∼∼(p ➝ q) ➝ ∼∼p ➝ ∼∼q

noncomputable def LO.System.dnDistributeImply' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢ ∼∼(p ➝ q)) : 𝓢 ⊢ ∼∼p ➝ ∼∼q

Equations

• LO.System.dnDistributeImply' b = LO.System.dnDistributeImply⨀b

theorem LO.System.dn_distribute_imply'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢! ∼∼(p ➝ q)) : 𝓢 ⊢! ∼∼p ➝ ∼∼q

def LO.System.introFalsumOfAnd' {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (h : 𝓢 ⊢ p ⋏ ∼p) : 𝓢 ⊢ ⊥

Equations

• LO.System.introFalsumOfAnd' h = LO.System.neg_equiv'.mp (LO.System.and₂' h)⨀LO.System.and₁' h

theorem LO.System.intro_falsum_of_and'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (h : 𝓢 ⊢! p ⋏ ∼p) : 𝓢 ⊢! ⊥

theorem LO.System.lac'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] (h : 𝓢 ⊢! p ⋏ ∼p) : 𝓢 ⊢! ⊥

Law of contradiction

def LO.System.introFalsumOfAnd {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ p ⋏ ∼p ➝ ⊥

Equations

• LO.System.introFalsumOfAnd = LO.System.FiniteContext.deduct' (LO.System.introFalsumOfAnd' LO.System.FiniteContext.id)

@[simp]

theorem LO.System.intro_bot_of_and! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! p ⋏ ∼p ➝ ⊥

theorem LO.System.lac! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! p ⋏ ∼p ➝ ⊥

Law of contradiction

def LO.System.implyOfNotOr {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢ ∼p ⋎ q ➝ p ➝ q

Equations

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

@[simp]

theorem LO.System.imply_of_not_or! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢! ∼p ⋎ q ➝ p ➝ q

def LO.System.implyOfNotOr' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] (b : 𝓢 ⊢ ∼p ⋎ q) : 𝓢 ⊢ p ➝ q

Equations

• LO.System.implyOfNotOr' b = LO.System.implyOfNotOr⨀b

theorem LO.System.imply_of_not_or'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] (b : 𝓢 ⊢! ∼p ⋎ q) : 𝓢 ⊢! p ➝ q

def LO.System.demorgan₁ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ ∼p ⋎ ∼q ➝ ∼(p ⋏ q)

Equations

• LO.System.demorgan₁ = LO.System.or₃'' (LO.System.contra₀' LO.System.and₁) (LO.System.contra₀' LO.System.and₂)

@[simp]

theorem LO.System.demorgan₁! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! ∼p ⋎ ∼q ➝ ∼(p ⋏ q)

def LO.System.demorgan₁' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (d : 𝓢 ⊢ ∼p ⋎ ∼q) : 𝓢 ⊢ ∼(p ⋏ q)

Equations

• LO.System.demorgan₁' d = LO.System.demorgan₁⨀d

theorem LO.System.demorgan₁'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (d : 𝓢 ⊢! ∼p ⋎ ∼q) : 𝓢 ⊢! ∼(p ⋏ q)

def LO.System.demorgan₂ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ ∼p ⋏ ∼q ➝ ∼(p ⋎ q)

Equations

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

@[simp]

theorem LO.System.demorgan₂! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! ∼p ⋏ ∼q ➝ ∼(p ⋎ q)

def LO.System.demorgan₂' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (d : 𝓢 ⊢ ∼p ⋏ ∼q) : 𝓢 ⊢ ∼(p ⋎ q)

Equations

• LO.System.demorgan₂' d = LO.System.demorgan₂⨀d

theorem LO.System.demorgan₂'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (d : 𝓢 ⊢! ∼p ⋏ ∼q) : 𝓢 ⊢! ∼(p ⋎ q)

def LO.System.demorgan₃ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ ∼(p ⋎ q) ➝ ∼p ⋏ ∼q

Equations

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

@[simp]

theorem LO.System.demorgan₃! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! ∼(p ⋎ q) ➝ ∼p ⋏ ∼q

def LO.System.demorgan₃' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢ ∼(p ⋎ q)) : 𝓢 ⊢ ∼p ⋏ ∼q

Equations

• LO.System.demorgan₃' b = LO.System.demorgan₃⨀b

theorem LO.System.demorgan₃'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] (b : 𝓢 ⊢! ∼(p ⋎ q)) : 𝓢 ⊢! ∼p ⋏ ∼q

noncomputable def LO.System.demorgan₄ {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢ ∼(p ⋏ q) ➝ ∼p ⋎ ∼q

Equations

• LO.System.demorgan₄ = LO.System.contra₂' (LO.System.FiniteContext.deduct' (LO.System.andReplace' (LO.System.demorgan₃' LO.System.FiniteContext.id) LO.System.dne LO.System.dne))

@[simp]

theorem LO.System.demorgan₄! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢! ∼(p ⋏ q) ➝ ∼p ⋎ ∼q

noncomputable def LO.System.demorgan₄' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (b : 𝓢 ⊢ ∼(p ⋏ q)) : 𝓢 ⊢ ∼p ⋎ ∼q

Equations

• LO.System.demorgan₄' b = LO.System.demorgan₄⨀b

theorem LO.System.demorgan₄'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (b : 𝓢 ⊢! ∼(p ⋏ q)) : 𝓢 ⊢! ∼p ⋎ ∼q

noncomputable def LO.System.NotOrOfImply' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (d : 𝓢 ⊢ p ➝ q) : 𝓢 ⊢ ∼p ⋎ q

Equations

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

theorem LO.System.not_or_of_imply'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] (d : 𝓢 ⊢! p ➝ q) : 𝓢 ⊢! ∼p ⋎ q

noncomputable def LO.System.NotOrOfImply {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢ (p ➝ q) ➝ ∼p ⋎ q

Equations

• LO.System.NotOrOfImply = LO.System.FiniteContext.deduct' (LO.System.NotOrOfImply' (LO.System.FiniteContext.byAxm ⋯))

theorem LO.System.not_or_of_imply! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢! (p ➝ q) ➝ ∼p ⋎ q

noncomputable def LO.System.dnCollectImply {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢ (∼∼p ➝ ∼∼q) ➝ ∼∼(p ➝ q)

Equations

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

@[simp]

theorem LO.System.dn_collect_imply! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢! (∼∼p ➝ ∼∼q) ➝ ∼∼(p ➝ q)

noncomputable def LO.System.dnCollectImply' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] (b : 𝓢 ⊢ ∼∼p ➝ ∼∼q) : 𝓢 ⊢ ∼∼(p ➝ q)

Equations

• LO.System.dnCollectImply' b = LO.System.dnCollectImply⨀b

theorem LO.System.dn_collect_imply'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] (b : 𝓢 ⊢! ∼∼p ➝ ∼∼q) : 𝓢 ⊢! ∼∼(p ➝ q)

def LO.System.andImplyAndOfImply {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {p' : F} {q' : F} (bp : 𝓢 ⊢ p ➝ p') (bq : 𝓢 ⊢ q ➝ q') : 𝓢 ⊢ p ⋏ q ➝ p' ⋏ q'

Equations

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

def LO.System.andIffAndOfIff {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {p' : F} {q' : F} (bp : 𝓢 ⊢ p ⭤ p') (bq : 𝓢 ⊢ q ⭤ q') : 𝓢 ⊢ p ⋏ q ⭤ p' ⋏ q'

Equations

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

instance LO.System.instHasAxiomEFQOfHasAxiomDNE {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : LO.System.HasAxiomEFQ 𝓢

Equations

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

noncomputable instance LO.System.instHasAxiomLEMOfHasAxiomDNE {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : LO.System.HasAxiomLEM 𝓢

Equations

• LO.System.instHasAxiomLEMOfHasAxiomDNE = { lem := fun (x : F) => LO.System.dneOr (LO.System.NotOrOfImply' LO.System.dni) }

instance LO.System.instHasAxiomDNEOfHasAxiomEFQOfHasAxiomLEM {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] [LO.System.HasAxiomLEM 𝓢] : LO.System.HasAxiomDNE 𝓢

Equations

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

instance LO.System.instHasAxiomWeakLEMOfHasAxiomLEM {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.HasAxiomLEM 𝓢] : LO.System.HasAxiomWeakLEM 𝓢

Equations

• LO.System.instHasAxiomWeakLEMOfHasAxiomLEM = { wlem := fun (p : F) => LO.System.lem }

instance LO.System.instHasAxiomDummettOfHasAxiomEFQOfHasAxiomLEM {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] [LO.System.HasAxiomLEM 𝓢] : LO.System.HasAxiomDummett 𝓢

Equations

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

noncomputable instance LO.System.instHasAxiomPeirceOfHasAxiomDNE {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : LO.System.HasAxiomPeirce 𝓢

Equations

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

instance LO.System.instHasAxiomElimContraOfHasAxiomDNE {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : LO.System.HasAxiomElimContra 𝓢

Equations

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

noncomputable def LO.System.implyIffNotOr {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢ (p ➝ q) ⭤ ∼p ⋎ q

Equations

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

noncomputable def LO.System.imply_iff_not_or! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomDNE 𝓢] : 𝓢 ⊢! (p ➝ q) ⭤ ∼p ⋎ q

Equations

• ⋯ = ⋯

def LO.System.conjIffConj {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] (Γ : List F) : 𝓢 ⊢ ⋀Γ ⭤ Γ.conj

Equations

• LO.System.conjIffConj [] = LO.System.iffId ⊤
• LO.System.conjIffConj [head] = LO.System.iffIntro (LO.System.FiniteContext.deduct' (LO.System.andIntro LO.System.FiniteContext.id LO.System.verum)) LO.System.and₁
• LO.System.conjIffConj (p :: q :: Γ) = LO.System.andIffAndOfIff (LO.System.iffId p) (LO.System.conjIffConj (q :: Γ))

@[simp]

theorem LO.System.conjIffConj! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} : 𝓢 ⊢! ⋀Γ ⭤ Γ.conj

theorem LO.System.implyLeft_conj_eq_conj! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} : 𝓢 ⊢! Γ.conj ➝ p ↔ 𝓢 ⊢! ⋀Γ ➝ p

theorem LO.System.generalConj'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} (h : p ∈ Γ) : 𝓢 ⊢! ⋀Γ ➝ p

theorem LO.System.generalConj'₂! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} (h : p ∈ Γ) (d : 𝓢 ⊢! ⋀Γ) : 𝓢 ⊢! p

theorem LO.System.iff_provable_list_conj {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} : 𝓢 ⊢! ⋀Γ ↔ ∀ p ∈ Γ, 𝓢 ⊢! p

theorem LO.System.conjconj_subset! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} {Δ : List F} (h : ∀ p ∈ Γ, p ∈ Δ) : 𝓢 ⊢! ⋀Δ ➝ ⋀Γ

theorem LO.System.conjconj_provable! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} {Δ : List F} (h : ∀ p ∈ Γ, Δ ⊢[𝓢]! p) : 𝓢 ⊢! ⋀Δ ➝ ⋀Γ

theorem LO.System.conjconj_provable₂! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} {Δ : List F} (h : ∀ p ∈ Γ, Δ ⊢[𝓢]! p) : Δ ⊢[𝓢]! ⋀Γ

theorem LO.System.id_conj! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} (he : ∀ g ∈ Γ, g = p) : 𝓢 ⊢! p ➝ ⋀Γ

theorem LO.System.replace_imply_left_conj! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {Γ : List F} (he : ∀ g ∈ Γ, g = p) (hd : 𝓢 ⊢! ⋀Γ ➝ q) : 𝓢 ⊢! p ➝ q

theorem LO.System.iff_imply_left_cons_conj'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {Γ : List F} : 𝓢 ⊢! ⋀(p :: Γ) ➝ q ↔ 𝓢 ⊢! p ⋏ ⋀Γ ➝ q

@[simp]

theorem LO.System.imply_left_concat_conj! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} {Δ : List F} : 𝓢 ⊢! ⋀(Γ ++ Δ) ➝ ⋀Γ ⋏ ⋀Δ

@[simp]

theorem LO.System.forthback_conj_remove! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} : 𝓢 ⊢! ⋀List.remove p Γ ⋏ p ➝ ⋀Γ

theorem LO.System.imply_left_remove_conj! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {Γ : List F} (b : 𝓢 ⊢! ⋀Γ ➝ q) : 𝓢 ⊢! ⋀List.remove p Γ ⋏ p ➝ q

theorem LO.System.iff_concat_conj'! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} {Δ : List F} : 𝓢 ⊢! ⋀(Γ ++ Δ) ↔ 𝓢 ⊢! ⋀Γ ⋏ ⋀Δ

@[simp]

theorem LO.System.iff_concat_conj! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} {Δ : List F} : 𝓢 ⊢! ⋀(Γ ++ Δ) ⭤ ⋀Γ ⋏ ⋀Δ

theorem LO.System.imply_left_conj_concat! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} {Δ : List F} : 𝓢 ⊢! ⋀(Γ ++ Δ) ➝ p ↔ 𝓢 ⊢! ⋀Γ ⋏ ⋀Δ ➝ p

theorem LO.System.iff_concact_disj! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} {Δ : List F} [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢! ⋁(Γ ++ Δ) ⭤ ⋁Γ ⋎ ⋁Δ

theorem LO.System.iff_concact_disj'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : List F} {Δ : List F} [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢! ⋁(Γ ++ Δ) ↔ 𝓢 ⊢! ⋁Γ ⋎ ⋁Δ

theorem LO.System.implyRight_cons_disj! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {Γ : List F} [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢! p ➝ ⋁(q :: Γ) ↔ 𝓢 ⊢! p ➝ q ⋎ ⋁Γ

@[simp]

theorem LO.System.forthback_disj_remove {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} [LO.System.HasAxiomEFQ 𝓢] : 𝓢 ⊢! ⋁Γ ➝ p ⋎ ⋁List.remove p Γ

theorem LO.System.disj_allsame! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} [LO.System.HasAxiomEFQ 𝓢] (hd : ∀ q ∈ Γ, q = p) : 𝓢 ⊢! ⋁Γ ➝ p

theorem LO.System.disj_allsame'! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : List F} [LO.System.HasAxiomEFQ 𝓢] (hd : ∀ q ∈ Γ, q = p) (h : 𝓢 ⊢! ⋁Γ) : 𝓢 ⊢! p

theorem LO.System.inconsistent_of_provable_of_unprovable {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomEFQ 𝓢] {p : F} (hp : 𝓢 ⊢! p) (hn : 𝓢 ⊢! ∼p) : LO.System.Inconsistent 𝓢