Foundation.Logic.HilbertStyle.Supplemental

source

def LO.System.mdp_in {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ φ ⋏ (φ ➝ ψ) ➝ ψ

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)

source

theorem LO.System.mdp_in! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! φ ⋏ (φ ➝ ψ) ➝ ψ

source

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

Γ ⊢[𝓢] ⊥

Equations

LO.System.bot_of_mem_either h₁ h₂ = LO.System.neg_equiv'.mp (LO.System.FiniteContext.byAxm h₂)⨀LO.System.FiniteContext.byAxm h₁

source

@[simp]

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

Γ ⊢[𝓢]! ⊥

source

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

Γ ⊢[𝓢] ψ

Equations

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

source

@[simp]

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

Γ ⊢[𝓢]! ψ

source

def LO.System.efq_imply_not₁ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢ ∼φ ➝ φ ➝ ψ

Equations

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

source

@[simp]

theorem LO.System.efq_imply_not₁! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢! ∼φ ➝ φ ➝ ψ

source

def LO.System.efq_imply_not₂ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢ φ ➝ ∼φ ➝ ψ

Equations

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

source

@[simp]

theorem LO.System.efq_imply_not₂! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢! φ ➝ ∼φ ➝ ψ

source

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

𝓢 ⊢! φ ➝ ψ

source

theorem LO.System.efq_of_neg₂! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] (h : 𝓢 ⊢! φ) :

𝓢 ⊢! ∼φ ➝ ψ

source

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

𝓢 ⊢ ⊥

Equations

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

source

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

𝓢 ⊢! ⊥

source

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

𝓢 ⊢ φ ⋎ ψ

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

source

theorem LO.System.dne_or! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] (d : 𝓢 ⊢! ∼∼φ ⋎ ∼∼ψ) :

𝓢 ⊢! φ ⋎ ψ

source

def LO.System.implyLeftOr' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ➝ χ) :

𝓢 ⊢ φ ➝ χ ⋎ ψ

Equations

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

source

theorem LO.System.imply_left_or'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ➝ χ) :

𝓢 ⊢! φ ➝ χ ⋎ ψ

source

def LO.System.implyRightOr' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ ➝ χ) :

𝓢 ⊢ ψ ➝ φ ⋎ χ

Equations

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

source

theorem LO.System.imply_right_or'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ ➝ χ) :

𝓢 ⊢! ψ ➝ φ ⋎ χ

source

def LO.System.implyRightAnd {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢ φ ➝ ψ) (hr : 𝓢 ⊢ φ ➝ χ) :

𝓢 ⊢ φ ➝ ψ ⋏ χ

Equations

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

source

theorem LO.System.imply_right_and! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢! φ ➝ ψ) (hr : 𝓢 ⊢! φ ➝ χ) :

𝓢 ⊢! φ ➝ ψ ⋏ χ

source

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

𝓢 ⊢! ψ ⋏ φ ➝ χ

source

theorem LO.System.dhyp_and_left! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ➝ χ) :

𝓢 ⊢! ψ ⋏ φ ➝ χ

source

theorem LO.System.dhyp_and_right! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ➝ χ) :

𝓢 ⊢! φ ⋏ ψ ➝ χ

source

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

𝓢 ⊢! φ₁ ⋏ φ₂ ➝ ψ₁ ⋎ ψ₂

source

def LO.System.orComm {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ φ ⋎ ψ ➝ ψ ⋎ φ

Equations

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

source

theorem LO.System.or_comm! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! φ ⋎ ψ ➝ ψ ⋎ φ

source

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

𝓢 ⊢ ψ ⋎ φ

Equations

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

source

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

𝓢 ⊢! ψ ⋎ φ

source

theorem LO.System.or_assoc'! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} :

𝓢 ⊢! φ ⋎ ψ ⋎ χ ↔ 𝓢 ⊢! (φ ⋎ ψ) ⋎ χ

source

theorem LO.System.and_assoc! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} :

𝓢 ⊢! (φ ⋏ ψ) ⋏ χ ⭤ φ ⋏ ψ ⋏ χ

source

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

𝓢 ⊢ χ ⋏ ψ

Equations

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

source

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

𝓢 ⊢! χ ⋏ ψ

source

def LO.System.andReplaceLeft {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ➝ χ) :

𝓢 ⊢ φ ⋏ ψ ➝ χ ⋏ ψ

Equations

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

source

theorem LO.System.and_replace_left! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ➝ χ) :

𝓢 ⊢! φ ⋏ ψ ➝ χ ⋏ ψ

source

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

𝓢 ⊢ φ ⋏ χ

Equations

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

source

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

𝓢 ⊢! φ ⋏ χ

source

def LO.System.andReplaceRight {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ ➝ χ) :

𝓢 ⊢ φ ⋏ ψ ➝ φ ⋏ χ

Equations

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

source

theorem LO.System.and_replace_right! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ ➝ χ) :

𝓢 ⊢! φ ⋏ ψ ➝ φ ⋏ χ

source

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

𝓢 ⊢ χ ⋏ s

Equations

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

source

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

𝓢 ⊢! χ ⋏ s

source

def LO.System.andReplace {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ s : F} (h₁ : 𝓢 ⊢ φ ➝ χ) (h₂ : 𝓢 ⊢ ψ ➝ s) :

𝓢 ⊢ φ ⋏ ψ ➝ χ ⋏ 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₂))

source

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

𝓢 ⊢! φ ⋏ ψ ➝ χ ⋏ s

source

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

𝓢 ⊢ χ ⋎ ψ

Equations

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

source

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

𝓢 ⊢! χ ⋎ ψ

source

def LO.System.orReplaceLeft {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (hp : 𝓢 ⊢ φ ➝ χ) :

𝓢 ⊢ φ ⋎ ψ ➝ χ ⋎ ψ

Equations

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

source

theorem LO.System.or_replace_left! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (hp : 𝓢 ⊢! φ ➝ χ) :

𝓢 ⊢! φ ⋎ ψ ➝ χ ⋎ ψ

source

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

𝓢 ⊢ φ ⋎ χ

Equations

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

source

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

𝓢 ⊢! φ ⋎ χ

source

def LO.System.orReplaceRight {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢ ψ ➝ χ) :

𝓢 ⊢ φ ⋎ ψ ➝ φ ⋎ χ

Equations

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

source

theorem LO.System.or_replace_right! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢! ψ ➝ χ) :

𝓢 ⊢! φ ⋎ ψ ➝ φ ⋎ χ

source

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

𝓢 ⊢ φ₂ ⋎ ψ₂

Equations

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

source

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

𝓢 ⊢! φ₂ ⋎ ψ₂

source

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

𝓢 ⊢ φ₁ ⋎ ψ₁ ➝ φ₂ ⋎ ψ₂

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

source

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

𝓢 ⊢! φ₁ ⋎ ψ₁ ➝ φ₂ ⋎ ψ₂

source

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

𝓢 ⊢ φ₁ ⋎ ψ₁ ⭤ φ₂ ⋎ ψ₂

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

source

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

𝓢 ⊢! φ₁ ⋎ ψ₁ ⭤ φ₂ ⋎ ψ₂

source

theorem LO.System.or_assoc! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} :

𝓢 ⊢! φ ⋎ ψ ⋎ χ ⭤ (φ ⋎ ψ) ⋎ χ

source

theorem LO.System.or_replace_right_iff! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢! ψ ⭤ χ) :

𝓢 ⊢! φ ⋎ ψ ⭤ φ ⋎ χ

source

theorem LO.System.or_replace_left_iff! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢! φ ⭤ χ) :

𝓢 ⊢! φ ⋎ ψ ⭤ χ ⋎ ψ

source

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

𝓢 ⊢ φ₁ ⋏ ψ₁ ⭤ φ₂ ⋏ ψ₂

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

source

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

𝓢 ⊢! φ₁ ⋏ ψ₁ ⭤ φ₂ ⋏ ψ₂

source

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

𝓢 ⊢ (φ₁ ➝ ψ₁) ⭤ (φ₂ ➝ ψ₂)

Equations

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

source

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

𝓢 ⊢! (φ₁ ➝ ψ₁) ⭤ (φ₂ ➝ ψ₂)

source

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

𝓢 ⊢! φ₁ ➝ ψ₁ ↔ 𝓢 ⊢! φ₂ ➝ ψ₂

source

def LO.System.dni {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} :

𝓢 ⊢ φ ➝ ∼∼φ

Equations

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

source

@[simp]

theorem LO.System.dni! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} :

𝓢 ⊢! φ ➝ ∼∼φ

source

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

𝓢 ⊢ ∼∼φ

Equations

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

source

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

𝓢 ⊢! ∼∼φ

source

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

𝓢 ⊢ ∼∼φ ⋎ ∼∼ψ

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

source

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

𝓢 ⊢! ∼∼φ ⋎ ∼∼ψ

source

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

𝓢 ⊢ ∼∼φ ⋏ ∼∼ψ

Equations

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

source

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

𝓢 ⊢! ∼∼φ ⋏ ∼∼ψ

source

def LO.System.falsumDNE {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] :

𝓢 ⊢ ∼∼⊥ ➝ ⊥

Equations

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

source

def LO.System.falsumDN {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] :

𝓢 ⊢ ∼∼⊥ ⭤ ⊥

Equations

LO.System.falsumDN = LO.System.andIntro LO.System.falsumDNE LO.System.dni

source

def LO.System.dn {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢ φ ⭤ ∼∼φ

Equations

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

source

@[simp]

theorem LO.System.dn! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢! φ ⭤ ∼∼φ

source

def LO.System.contra₀ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ (φ ➝ ψ) ➝ ∼ψ ➝ ∼φ

Equations

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

source

@[simp]

def LO.System.contra₀! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! (φ ➝ ψ) ➝ ∼ψ ➝ ∼φ

Equations

⋯ = ⋯

source

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

𝓢 ⊢ ∼ψ ➝ ∼φ

Equations

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

source

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

𝓢 ⊢! ∼ψ ➝ ∼φ

source

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

𝓢 ⊢ ∼∼φ ➝ ∼∼ψ

Equations

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

source

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

𝓢 ⊢! ∼∼φ ➝ ∼∼ψ

source

def LO.System.contra₀x2 {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ (φ ➝ ψ) ➝ ∼∼φ ➝ ∼∼ψ

Equations

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

source

@[simp]

theorem LO.System.contra₀x2! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! (φ ➝ ψ) ➝ ∼∼φ ➝ ∼∼ψ

source

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

𝓢 ⊢ ψ ➝ ∼φ

Equations

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

source

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

𝓢 ⊢! ψ ➝ ∼φ

source

def LO.System.contra₁ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ (φ ➝ ∼ψ) ➝ ψ ➝ ∼φ

Equations

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

source

theorem LO.System.contra₁! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! (φ ➝ ∼ψ) ➝ ψ ➝ ∼φ

source

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

𝓢 ⊢ ∼ψ ➝ φ

Equations

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

source

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

𝓢 ⊢! ∼ψ ➝ φ

source

def LO.System.contra₂ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢ (∼φ ➝ ψ) ➝ ∼ψ ➝ φ

Equations

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

source

@[simp]

theorem LO.System.contra₂! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢! (∼φ ➝ ψ) ➝ ∼ψ ➝ φ

source

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

𝓢 ⊢ ψ ➝ φ

Equations

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

source

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

𝓢 ⊢! ψ ➝ φ

source

def LO.System.contra₃ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢ (∼φ ➝ ∼ψ) ➝ ψ ➝ φ

Equations

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

source

@[simp]

theorem LO.System.contra₃! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢! (∼φ ➝ ∼ψ) ➝ ψ ➝ φ

source

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

𝓢 ⊢ ∼φ ⭤ ∼ψ

Equations

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

source

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

𝓢 ⊢! ∼φ ⭤ ∼ψ

source

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

𝓢 ⊢ ∼φ ⭤ ψ

Equations

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

source

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

𝓢 ⊢! ∼φ ⭤ ψ

source

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

𝓢 ⊢ φ ⭤ ∼ψ

Equations

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

source

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

𝓢 ⊢! φ ⭤ ∼ψ

source

def LO.System.negneg_equiv {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} [NegationEquiv 𝓢] :

𝓢 ⊢ ∼∼φ ⭤ ((φ ➝ ⊥) ➝ ⊥)

Equations

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

source

@[simp]

theorem LO.System.negneg_equiv! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} [NegationEquiv 𝓢] :

𝓢 ⊢! ∼∼φ ⭤ ((φ ➝ ⊥) ➝ ⊥)

source

def LO.System.negneg_equiv_dne {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} [NegationEquiv 𝓢] [HasAxiomDNE 𝓢] :

𝓢 ⊢ φ ⭤ ((φ ➝ ⊥) ➝ ⊥)

Equations

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

source

theorem LO.System.negneg_equiv_dne! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} [NegationEquiv 𝓢] [HasAxiomDNE 𝓢] :

𝓢 ⊢! φ ⭤ ((φ ➝ ⊥) ➝ ⊥)

source

def LO.System.elim_contra_neg {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomElimContra 𝓢] :

𝓢 ⊢ ((ψ ➝ ⊥) ➝ φ ➝ ⊥) ➝ φ ➝ ψ

Equations

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

source

theorem LO.System.elim_contra_neg! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomElimContra 𝓢] :

𝓢 ⊢! ((ψ ➝ ⊥) ➝ φ ➝ ⊥) ➝ φ ➝ ψ

source

def LO.System.tne {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} :

𝓢 ⊢ ∼∼∼φ ➝ ∼φ

Equations

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

source

@[simp]

theorem LO.System.tne! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} :

𝓢 ⊢! ∼∼∼φ ➝ ∼φ

source

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

𝓢 ⊢ ∼φ

Equations

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

source

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

𝓢 ⊢! ∼φ

source

def LO.System.tneIff {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} :

𝓢 ⊢ ∼∼∼φ ⭤ ∼φ

Equations

LO.System.tneIff = LO.System.andIntro LO.System.tne LO.System.dni

source

def LO.System.implyLeftReplace {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ ➝ φ) :

𝓢 ⊢ (φ ➝ χ) ➝ ψ ➝ χ

Equations

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

source

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

𝓢 ⊢! (φ ➝ χ) ➝ ψ ➝ χ

source

theorem LO.System.replace_imply_left_by_iff'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ⭤ ψ) :

𝓢 ⊢! φ ➝ χ ↔ 𝓢 ⊢! ψ ➝ χ

source

theorem LO.System.replace_imply_right_by_iff'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ⭤ ψ) :

𝓢 ⊢! χ ➝ φ ↔ 𝓢 ⊢! χ ➝ ψ

source

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

𝓢 ⊢ ψ ➝ φ ➝ χ

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

source

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

𝓢 ⊢! ψ ➝ φ ➝ χ

source

def LO.System.impSwap {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} :

𝓢 ⊢ (φ ➝ ψ ➝ χ) ➝ ψ ➝ φ ➝ χ

Equations

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

source

@[simp]

theorem LO.System.imp_swap! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ χ : F} :

𝓢 ⊢! (φ ➝ ψ ➝ χ) ➝ ψ ➝ φ ➝ χ

source

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

𝓢 ⊢ φ ➝ ψ

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

source

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

𝓢 ⊢! φ ➝ ψ

source

def LO.System.p_pq_q {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ φ ➝ (φ ➝ ψ) ➝ ψ

Equations

LO.System.p_pq_q = LO.System.impSwap' (LO.System.impId (φ ➝ ψ))

source

theorem LO.System.p_pq_q! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! φ ➝ (φ ➝ ψ) ➝ ψ

source

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

𝓢 ⊢ (χ ➝ φ) ➝ χ ➝ ψ

Equations

LO.System.dhyp_imp' h = LO.System.imply₂ ⨀LO.System.imply₁' h

source

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

𝓢 ⊢! (χ ➝ φ) ➝ χ ➝ ψ

source

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

𝓢 ⊢ (φ ➝ χ) ➝ ψ ➝ χ

Equations

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

source

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

𝓢 ⊢! (φ ➝ χ) ➝ ψ ➝ χ

source

noncomputable def LO.System.dnDistributeImply {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ ∼∼(φ ➝ ψ) ➝ ∼∼φ ➝ ∼∼ψ

Equations

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

source

@[simp]

theorem LO.System.dn_distribute_imply! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! ∼∼(φ ➝ ψ) ➝ ∼∼φ ➝ ∼∼ψ

source

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

𝓢 ⊢ ∼∼φ ➝ ∼∼ψ

Equations

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

source

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

𝓢 ⊢! ∼∼φ ➝ ∼∼ψ

source

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

𝓢 ⊢ ⊥

Equations

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

source

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

𝓢 ⊢! ⊥

source

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

𝓢 ⊢! ⊥

Law of contradiction

source

def LO.System.introFalsumOfAnd {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} :

𝓢 ⊢ φ ⋏ ∼φ ➝ ⊥

Equations

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

source

@[simp]

theorem LO.System.intro_bot_of_and! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} :

𝓢 ⊢! φ ⋏ ∼φ ➝ ⊥

source

theorem LO.System.lac! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} :

𝓢 ⊢! φ ⋏ ∼φ ➝ ⊥

Law of contradiction

source

def LO.System.implyOfNotOr {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢ ∼φ ⋎ ψ ➝ φ ➝ ψ

Equations

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

source

@[simp]

theorem LO.System.imply_of_not_or! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢! ∼φ ⋎ ψ ➝ φ ➝ ψ

source

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

𝓢 ⊢ φ ➝ ψ

Equations

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

source

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

𝓢 ⊢! φ ➝ ψ

source

def LO.System.demorgan₁ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ ∼φ ⋎ ∼ψ ➝ ∼(φ ⋏ ψ)

Equations

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

source

@[simp]

theorem LO.System.demorgan₁! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! ∼φ ⋎ ∼ψ ➝ ∼(φ ⋏ ψ)

source

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

𝓢 ⊢ ∼(φ ⋏ ψ)

Equations

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

source

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

𝓢 ⊢! ∼(φ ⋏ ψ)

source

def LO.System.demorgan₂ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ ∼φ ⋏ ∼ψ ➝ ∼(φ ⋎ ψ)

Equations

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

source

@[simp]

theorem LO.System.demorgan₂! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! ∼φ ⋏ ∼ψ ➝ ∼(φ ⋎ ψ)

source

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

𝓢 ⊢ ∼(φ ⋎ ψ)

Equations

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

source

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

𝓢 ⊢! ∼(φ ⋎ ψ)

source

def LO.System.demorgan₃ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢ ∼(φ ⋎ ψ) ➝ ∼φ ⋏ ∼ψ

Equations

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

source

@[simp]

theorem LO.System.demorgan₃! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} :

𝓢 ⊢! ∼(φ ⋎ ψ) ➝ ∼φ ⋏ ∼ψ

source

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

𝓢 ⊢ ∼φ ⋏ ∼ψ

Equations

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

source

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

𝓢 ⊢! ∼φ ⋏ ∼ψ

source

noncomputable def LO.System.demorgan₄ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢ ∼(φ ⋏ ψ) ➝ ∼φ ⋎ ∼ψ

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

source

@[simp]

theorem LO.System.demorgan₄! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢! ∼(φ ⋏ ψ) ➝ ∼φ ⋎ ∼ψ

source

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

𝓢 ⊢ ∼φ ⋎ ∼ψ

Equations

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

source

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

𝓢 ⊢! ∼φ ⋎ ∼ψ

source

noncomputable def LO.System.NotOrOfImply' {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] (d : 𝓢 ⊢ φ ➝ ψ) :

𝓢 ⊢ ∼φ ⋎ ψ

Equations

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

source

theorem LO.System.not_or_of_imply'! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] (d : 𝓢 ⊢! φ ➝ ψ) :

𝓢 ⊢! ∼φ ⋎ ψ

source

noncomputable def LO.System.NotOrOfImply {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢ (φ ➝ ψ) ➝ ∼φ ⋎ ψ

Equations

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

source

theorem LO.System.not_or_of_imply! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢! (φ ➝ ψ) ➝ ∼φ ⋎ ψ

source

noncomputable def LO.System.dnCollectImply {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢ (∼∼φ ➝ ∼∼ψ) ➝ ∼∼(φ ➝ ψ)

Equations

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

source

@[simp]

theorem LO.System.dn_collect_imply! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢! (∼∼φ ➝ ∼∼ψ) ➝ ∼∼(φ ➝ ψ)

source

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

𝓢 ⊢ ∼∼(φ ➝ ψ)

Equations

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

source

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

𝓢 ⊢! ∼∼(φ ➝ ψ)

source

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

𝓢 ⊢ φ ⋏ ψ ➝ φ' ⋏ ψ'

Equations

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

source

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

𝓢 ⊢ φ ⋏ ψ ⭤ φ' ⋏ ψ'

Equations

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

source

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

HasAxiomEFQ 𝓢

Equations

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

source

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

HasAxiomLEM 𝓢

Equations

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

source

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

HasAxiomDNE 𝓢

Equations

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

source

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

HasAxiomWeakLEM 𝓢

Equations

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

source

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

HasAxiomDummett 𝓢

Equations

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

source

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

HasAxiomWeakLEM 𝓢

Equations

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

source

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

HasAxiomPeirce 𝓢

Equations

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

source

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

HasAxiomElimContra 𝓢

Equations

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

source

noncomputable def LO.System.implyIffNotOr {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢ (φ ➝ ψ) ⭤ ∼φ ⋎ ψ

Equations

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

source

noncomputable def LO.System.imply_iff_not_or! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢! (φ ➝ ψ) ⭤ ∼φ ⋎ ψ

Equations

⋯ = ⋯

source

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

𝓢 ⊢ ⋀Γ ⭤ Γ.conj

Equations

source

@[simp]

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

𝓢 ⊢! ⋀Γ ⭤ Γ.conj

source

theorem LO.System.implyLeft_conj_eq_conj! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} {Γ : List F} :

𝓢 ⊢! Γ.conj ➝ φ ↔ 𝓢 ⊢! ⋀Γ ➝ φ

source

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

𝓢 ⊢! ⋀Γ ➝ φ

source

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

𝓢 ⊢! φ

source

theorem LO.System.iff_provable_list_conj {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {Γ : List F} :

𝓢 ⊢! ⋀Γ ↔ ∀ φ ∈ Γ, 𝓢 ⊢! φ

source

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

𝓢 ⊢! ⋀Δ ➝ ⋀Γ

source

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

𝓢 ⊢! ⋀Δ ➝ ⋀Γ

source

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

Δ ⊢[𝓢]! ⋀Γ

source

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

𝓢 ⊢! φ ➝ ⋀Γ

source

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

𝓢 ⊢! φ ➝ ψ

source

theorem LO.System.iff_imply_left_cons_conj'! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} {Γ : List F} :

𝓢 ⊢! ⋀(φ :: Γ) ➝ ψ ↔ 𝓢 ⊢! φ ⋏ ⋀Γ ➝ ψ

source

@[simp]

theorem LO.System.imply_left_concat_conj! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {Γ Δ : List F} :

𝓢 ⊢! ⋀(Γ ++ Δ) ➝ ⋀Γ ⋏ ⋀Δ

source

@[simp]

theorem LO.System.forthback_conj_remove! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} {Γ : List F} :

𝓢 ⊢! ⋀List.remove φ Γ ⋏ φ ➝ ⋀Γ

source

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

𝓢 ⊢! ⋀List.remove φ Γ ⋏ φ ➝ ψ

source

theorem LO.System.iff_concat_conj'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {Γ Δ : List F} :

𝓢 ⊢! ⋀(Γ ++ Δ) ↔ 𝓢 ⊢! ⋀Γ ⋏ ⋀Δ

source

@[simp]

theorem LO.System.iff_concat_conj! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {Γ Δ : List F} :

𝓢 ⊢! ⋀(Γ ++ Δ) ⭤ ⋀Γ ⋏ ⋀Δ

source

theorem LO.System.imply_left_conj_concat! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} {Γ Δ : List F} :

𝓢 ⊢! ⋀(Γ ++ Δ) ➝ φ ↔ 𝓢 ⊢! ⋀Γ ⋏ ⋀Δ ➝ φ

source

theorem LO.System.iff_concact_disj! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {Γ Δ : List F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢! ⋁(Γ ++ Δ) ⭤ ⋁Γ ⋎ ⋁Δ

source

theorem LO.System.iff_concact_disj'! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {Γ Δ : List F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢! ⋁(Γ ++ Δ) ↔ 𝓢 ⊢! ⋁Γ ⋎ ⋁Δ

source

theorem LO.System.implyRight_cons_disj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ ψ : F} {Γ : List F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢! φ ➝ ⋁(ψ :: Γ) ↔ 𝓢 ⊢! φ ➝ ψ ⋎ ⋁Γ

source

@[simp]

theorem LO.System.forthback_disj_remove {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [System F S] {𝓢 : S} [System.Minimal 𝓢] {φ : F} {Γ : List F} [HasAxiomEFQ 𝓢] :

𝓢 ⊢! ⋁Γ ➝ φ ⋎ ⋁List.remove φ Γ

source

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

𝓢 ⊢! ⋁Γ ➝ φ

source

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

𝓢 ⊢! φ

source

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

Inconsistent 𝓢