Supplemental

def LO.Entailment.mdpIn {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ⋏ (φ ==> ψ) ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.mdpIn = LO.Entailment.FiniteContext.deduct' (have hp := LO.Entailment.FiniteContext.byAxm ⋯; have hpq := LO.Entailment.FiniteContext.byAxm ⋯; hpq⨀hp)

theorem LO.Entailment.mdpIn! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! φ ⋏ (φ ==> ψ) ==> ψ

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.botOfMemEither h₁ h₂ = LO.Entailment.negEquiv'.mp (LO.Entailment.FiniteContext.byAxm h₂)⨀LO.Entailment.FiniteContext.byAxm h₁

theorem LO.Entailment.botOfMemEither! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) : Γ ⊢[𝓢]! ⊥

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.efqOfMemEither h₁ h₂ = LO.Entailment.efq' (LO.Entailment.botOfMemEither h₁ h₂)

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

def LO.Entailment.efqImplyNot₁ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢ ∼φ ==> φ ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.efqImplyNot₁ = LO.Entailment.FiniteContext.deduct' (LO.Entailment.FiniteContext.deduct (LO.Entailment.efqOfMemEither ⋯ ⋯))

@[simp]

theorem LO.Entailment.efqImplyNot₁! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢! ∼φ ==> φ ==> ψ

def LO.Entailment.efqImplyNot₂ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢ φ ==> ∼φ ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.efqImplyNot₂ = LO.Entailment.FiniteContext.deduct' (LO.Entailment.FiniteContext.deduct (LO.Entailment.efqOfMemEither ⋯ ⋯))

@[simp]

theorem LO.Entailment.efqImplyNot₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢! φ ==> ∼φ ==> ψ

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.negMdp hnp hn = LO.Entailment.negEquiv'.mp hnp⨀hn

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.imply_right_and! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢! φ ==> ψ) (hr : 𝓢 ⊢! φ ==> χ) : 𝓢 ⊢! φ ==> ψ ⋏ χ

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

theorem LO.Entailment.dhyp_and_left! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ==> χ) : 𝓢 ⊢! ψ ⋏ φ ==> χ

theorem LO.Entailment.dhyp_and_right! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ==> χ) : 𝓢 ⊢! φ ⋏ ψ ==> χ

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

def LO.Entailment.orComm {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ⋎ ψ ==> ψ ⋎ φ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.or_comm! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! φ ⋎ ψ ==> ψ ⋎ φ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

theorem LO.Entailment.or_assoc'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢! φ ⋎ ψ ⋎ χ ↔ 𝓢 ⊢! (φ ⋎ ψ) ⋎ χ

theorem LO.Entailment.and_assoc! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢! (φ ⋏ ψ) ⋏ χ <=> φ ⋏ ψ ⋏ χ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.and_replace_left! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ==> χ) : 𝓢 ⊢! φ ⋏ ψ ==> χ ⋏ ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.and_replace_right! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ ==> χ) : 𝓢 ⊢! φ ⋏ ψ ==> φ ⋏ χ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.or_replace_left! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hp : 𝓢 ⊢! φ ==> χ) : 𝓢 ⊢! φ ⋎ ψ ==> χ ⋎ ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.or_replace_right! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢! ψ ==> χ) : 𝓢 ⊢! φ ⋎ ψ ==> φ ⋎ χ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.orReplaceIff {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ <=> φ₂) (hq : 𝓢 ⊢ ψ₁ <=> ψ₂) : 𝓢 ⊢ φ₁ ⋎ ψ₁ <=> φ₂ ⋎ ψ₂

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.or_replace_iff! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ <=> φ₂) (hq : 𝓢 ⊢! ψ₁ <=> ψ₂) : 𝓢 ⊢! φ₁ ⋎ ψ₁ <=> φ₂ ⋎ ψ₂

theorem LO.Entailment.or_assoc! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢! φ ⋎ ψ ⋎ χ <=> (φ ⋎ ψ) ⋎ χ

theorem LO.Entailment.or_replace_right_iff! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢! ψ <=> χ) : 𝓢 ⊢! φ ⋎ ψ <=> φ ⋎ χ

theorem LO.Entailment.or_replace_left_iff! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢! φ <=> χ) : 𝓢 ⊢! φ ⋎ ψ <=> χ ⋎ ψ

def LO.Entailment.andReplaceIff {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ <=> φ₂) (hq : 𝓢 ⊢ ψ₁ <=> ψ₂) : 𝓢 ⊢ φ₁ ⋏ ψ₁ <=> φ₂ ⋏ ψ₂

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.and_replace_iff! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ <=> φ₂) (hq : 𝓢 ⊢! ψ₁ <=> ψ₂) : 𝓢 ⊢! φ₁ ⋏ ψ₁ <=> φ₂ ⋏ ψ₂

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.imp_replace_iff! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ <=> φ₂) (hq : 𝓢 ⊢! ψ₁ <=> ψ₂) : 𝓢 ⊢! (φ₁ ==> ψ₁) <=> (φ₂ ==> ψ₂)

theorem LO.Entailment.imp_replace_iff!' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ <=> φ₂) (hq : 𝓢 ⊢! ψ₁ <=> ψ₂) : 𝓢 ⊢! φ₁ ==> ψ₁ ↔ 𝓢 ⊢! φ₂ ==> ψ₂

def LO.Entailment.dni {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ==> ∼∼φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.dni = LO.Entailment.FiniteContext.deduct' (LO.Entailment.negEquiv'.mpr (LO.Entailment.FiniteContext.deduct (LO.Entailment.botOfMemEither ⋯ ⋯)))

@[simp]

theorem LO.Entailment.dni! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢! φ ==> ∼∼φ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.falsumDNE {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] : 𝓢 ⊢ ∼∼⊥ ==> ⊥

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Entailment.falsumDN {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] : 𝓢 ⊢ ∼∼⊥ <=> ⊥

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.falsumDN = LO.Entailment.andIntro LO.Entailment.falsumDNE LO.Entailment.dni

def LO.Entailment.dn {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢ φ <=> ∼∼φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.dn! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢! φ <=> ∼∼φ

def LO.Entailment.contra₀ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ (φ ==> ψ) ==> ∼ψ ==> ∼φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.contra₀! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! (φ ==> ψ) ==> ∼ψ ==> ∼φ

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.contra₀'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢! φ ==> ψ) : 𝓢 ⊢! ∼ψ ==> ∼φ

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.contra₀x2'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢! φ ==> ψ) : 𝓢 ⊢! ∼∼φ ==> ∼∼ψ

def LO.Entailment.contra₀x2 {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ (φ ==> ψ) ==> ∼∼φ ==> ∼∼ψ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.contra₀x2! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! (φ ==> ψ) ==> ∼∼φ ==> ∼∼ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.contra₁ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ (φ ==> ∼ψ) ==> ψ ==> ∼φ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.contra₁! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! (φ ==> ∼ψ) ==> ψ ==> ∼φ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.contra₂ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢ (∼φ ==> ψ) ==> ∼ψ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.contra₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢! (∼φ ==> ψ) ==> ∼ψ ==> φ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.contra₃ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢ (∼φ ==> ∼ψ) ==> ψ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.contra₃! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢! (∼φ ==> ∼ψ) ==> ψ ==> φ

def LO.Entailment.negReplaceIff' {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢ φ <=> ψ) : 𝓢 ⊢ ∼φ <=> ∼ψ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.neg_replace_iff'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢! φ <=> ψ) : 𝓢 ⊢! ∼φ <=> ∼ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.iff_neg_left_to_right'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] (h : 𝓢 ⊢! φ <=> ∼ψ) : 𝓢 ⊢! ∼φ <=> ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.iff_neg_right_to_left'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] (h : 𝓢 ⊢! ∼φ <=> ψ) : 𝓢 ⊢! φ <=> ∼ψ

def LO.Entailment.negnegEquiv {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ ∼∼φ <=> ((φ ==> ⊥) ==> ⊥)

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.negnegEquiv! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢! ∼∼φ <=> ((φ ==> ⊥) ==> ⊥)

def LO.Entailment.negnegEquivDne {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢ φ <=> ((φ ==> ⊥) ==> ⊥)

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.negnegEquivDne = LO.Entailment.iffTrans'' LO.Entailment.dn LO.Entailment.negnegEquiv

theorem LO.Entailment.negnegEquivDne! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢! φ <=> ((φ ==> ⊥) ==> ⊥)

def LO.Entailment.elimContraNeg {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomElimContra 𝓢] : 𝓢 ⊢ ((ψ ==> ⊥) ==> φ ==> ⊥) ==> φ ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.elimContraNeg! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomElimContra 𝓢] : 𝓢 ⊢! ((ψ ==> ⊥) ==> φ ==> ⊥) ==> φ ==> ψ

def LO.Entailment.tne {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ ∼∼∼φ ==> ∼φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.tne! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢! ∼∼∼φ ==> ∼φ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.tneIff {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ ∼∼∼φ <=> ∼φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.tneIff = LO.Entailment.andIntro LO.Entailment.tne LO.Entailment.dni

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

theorem LO.Entailment.replace_imply_left_by_iff'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ <=> ψ) : 𝓢 ⊢! φ ==> χ ↔ 𝓢 ⊢! ψ ==> χ

theorem LO.Entailment.replace_imply_right_by_iff'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ <=> ψ) : 𝓢 ⊢! χ ==> φ ↔ 𝓢 ⊢! χ ==> ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.impSwap {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ (φ ==> ψ ==> χ) ==> ψ ==> φ ==> χ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.imp_swap! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢! (φ ==> ψ ==> χ) ==> ψ ==> φ ==> χ

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.ppq h = LO.Entailment.FiniteContext.deduct' (LO.Entailment.FiniteContext.of h⨀LO.Entailment.FiniteContext.byAxm ⋯⨀LO.Entailment.FiniteContext.byAxm ⋯)

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

def LO.Entailment.pPqQ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ==> (φ ==> ψ) ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.pPqQ = LO.Entailment.impSwap' (LO.Entailment.impId (φ ==> ψ))

theorem LO.Entailment.pPqQ! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! φ ==> (φ ==> ψ) ==> ψ

def LO.Entailment.dhypImp' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ==> ψ) : 𝓢 ⊢ (χ ==> φ) ==> χ ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.dhypImp' h = LO.Entailment.imply₂⨀LO.Entailment.imply₁' h

theorem LO.Entailment.dhypImp'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ==> ψ) : 𝓢 ⊢! (χ ==> φ) ==> χ ==> ψ

def LO.Entailment.revDhypImp' {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ ==> φ) : 𝓢 ⊢ (φ ==> χ) ==> ψ ==> χ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.revDhypImp' h = LO.Entailment.impSwap' (LO.Entailment.impTrans'' h LO.Entailment.pPqQ)

theorem LO.Entailment.revDhypImp'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ ==> φ) : 𝓢 ⊢! (φ ==> χ) ==> ψ ==> χ

noncomputable def LO.Entailment.dnDistributeImply {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ ∼∼(φ ==> ψ) ==> ∼∼φ ==> ∼∼ψ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.dn_distribute_imply! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! ∼∼(φ ==> ψ) ==> ∼∼φ ==> ∼∼ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.introFalsumOfAnd' h = LO.Entailment.negEquiv'.mp (LO.Entailment.and₂' h)⨀LO.Entailment.and₁' h

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

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

Law of contradiction

def LO.Entailment.introFalsumOfAnd {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ⋏ ∼φ ==> ⊥

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.intro_bot_of_and! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢! φ ⋏ ∼φ ==> ⊥

theorem LO.Entailment.lac! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢! φ ⋏ ∼φ ==> ⊥

Law of contradiction

def LO.Entailment.implyOfNotOr {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢ ∼φ ⋎ ψ ==> φ ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.imply_of_not_or! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢! ∼φ ⋎ ψ ==> φ ==> ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.demorgan₁ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ ∼φ ⋎ ∼ψ ==> ∼(φ ⋏ ψ)

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.demorgan₁! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! ∼φ ⋎ ∼ψ ==> ∼(φ ⋏ ψ)

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.demorgan₂ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ ∼φ ⋏ ∼ψ ==> ∼(φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.demorgan₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! ∼φ ⋏ ∼ψ ==> ∼(φ ⋎ ψ)

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

def LO.Entailment.demorgan₃ {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ ∼(φ ⋎ ψ) ==> ∼φ ⋏ ∼ψ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.demorgan₃! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! ∼(φ ⋎ ψ) ==> ∼φ ⋏ ∼ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.demorgan₄! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢! ∼(φ ⋏ ψ) ==> ∼φ ⋎ ∼ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

noncomputable def LO.Entailment.NotOrOfImply' {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] (d : 𝓢 ⊢ φ ==> ψ) : 𝓢 ⊢ ∼φ ⋎ ψ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.not_or_of_imply'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] (d : 𝓢 ⊢! φ ==> ψ) : 𝓢 ⊢! ∼φ ⋎ ψ

noncomputable def LO.Entailment.NotOrOfImply {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢ (φ ==> ψ) ==> ∼φ ⋎ ψ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.not_or_of_imply! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢! (φ ==> ψ) ==> ∼φ ⋎ ψ

noncomputable def LO.Entailment.dnCollectImply {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢ (∼∼φ ==> ∼∼ψ) ==> ∼∼(φ ==> ψ)

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.dn_collect_imply! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢! (∼∼φ ==> ∼∼ψ) ==> ∼∼(φ ==> ψ)

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Entailment.andIffAndOfIff {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ φ' ψ' : F} (bp : 𝓢 ⊢ φ <=> φ') (bq : 𝓢 ⊢ ψ <=> ψ') : 𝓢 ⊢ φ ⋏ ψ <=> φ' ⋏ ψ'

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LO.Entailment.instHasAxiomWeakLEMOfHasAxiomDummett {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomDummett 𝓢] : HasAxiomWeakLEM 𝓢

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

noncomputable def LO.Entailment.implyIffNotOr {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢ (φ ==> ψ) <=> ∼φ ⋎ ψ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.imply_iff_not_or! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢! (φ ==> ψ) <=> ∼φ ⋎ ψ

Imported declaration from the Incompleteness formalization.

def LO.Entailment.conjIffConj {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) : 𝓢 ⊢ ⋀Γ <=> Γ.conj

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.Entailment.conjIffConj [] = LO.Entailment.iffId ⊤
• LO.Entailment.conjIffConj (φ :: ψ :: Γ) = LO.Entailment.andIffAndOfIff (LO.Entailment.iffId φ) (LO.Entailment.conjIffConj (ψ :: Γ))

@[simp]

theorem LO.Entailment.conjIffConj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : List F} : 𝓢 ⊢! ⋀Γ <=> Γ.conj

theorem LO.Entailment.implyLeft_conj_eq_conj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} : 𝓢 ⊢! Γ.conj ==> φ ↔ 𝓢 ⊢! ⋀Γ ==> φ

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

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

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

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

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

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

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

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

theorem LO.Entailment.iff_imply_left_cons_conj'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} : 𝓢 ⊢! ⋀(φ :: Γ) ==> ψ ↔ 𝓢 ⊢! φ ⋏ ⋀Γ ==> ψ

@[simp]

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

@[simp]

theorem LO.Entailment.forthback_conj_remove! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} : 𝓢 ⊢! ⋀List.remove φ Γ ⋏ φ ==> ⋀Γ

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

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

@[simp]

theorem LO.Entailment.iff_concat_conj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} : 𝓢 ⊢! ⋀(Γ ++ Δ) <=> ⋀Γ ⋏ ⋀Δ

theorem LO.Entailment.imply_left_conj_concat! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ Δ : List F} : 𝓢 ⊢! ⋀(Γ ++ Δ) ==> φ ↔ 𝓢 ⊢! ⋀Γ ⋏ ⋀Δ ==> φ

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

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

theorem LO.Entailment.implyRight_cons_disj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢! φ ==> ⋁(ψ :: Γ) ↔ 𝓢 ⊢! φ ==> ψ ⋎ ⋁Γ

@[simp]

theorem LO.Entailment.forthback_disj_remove {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢! ⋁Γ ==> φ ⋎ ⋁List.remove φ Γ

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

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

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