Basic

def LO.Entailment.cast {S : Type u_1} {F : Type u_2} [Entailment F S] {𝓢 : S} {φ ψ : F} (e : φ = ψ) (b : 𝓢 ⊢ φ) : 𝓢 ⊢ ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.cast e b = e ▸ b

theorem LO.Entailment.cast! {S : Type u_1} {F : Type u_2} [Entailment F S] {𝓢 : S} {φ ψ : F} (e : φ = ψ) (b : 𝓢 ⊢! φ) : 𝓢 ⊢! ψ

Imported declaration from the Incompleteness formalization.

class LO.Entailment.ModusPonens {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.mdp {S : Type u_1} {F : Type u_2} {inst✝ : LogicalConnective F} {inst✝¹ : Entailment F S} {𝓢 : S} [self : ModusPonens 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ

Alias of LO.Entailment.ModusPonens.mdp.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.mdp = @LO.Entailment.ModusPonens.mdp

def LO.Entailment.«term_⨀_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀") (Lean.ParserDescr.cat `term 91))

theorem LO.Entailment.mdp! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] : 𝓢 ⊢! φ ==> ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ

def LO.Entailment.«term_⨀__1» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀") (Lean.ParserDescr.cat `term 91))

class LO.Entailment.HasAxiomVerum {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type u_3

Imported declaration from the Incompleteness formalization.

• verum : 𝓢 ⊢ Axioms.Verum

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.verum {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomVerum 𝓢] : 𝓢 ⊢ ⊤

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.verum = LO.Entailment.HasAxiomVerum.verum

@[simp]

theorem LO.Entailment.verum! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [HasAxiomVerum 𝓢] : 𝓢 ⊢! ⊤

class LO.Entailment.HasAxiomImply₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.imply₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomImply₁ 𝓢] : 𝓢 ⊢ φ ==> ψ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.imply₁ = LO.Entailment.HasAxiomImply₁.imply₁ φ ψ

@[simp]

theorem LO.Entailment.imply₁! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomImply₁ 𝓢] : 𝓢 ⊢! φ ==> ψ ==> φ

def LO.Entailment.imply₁' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] (h : 𝓢 ⊢ φ) : 𝓢 ⊢ ψ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.imply₁'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] (d : 𝓢 ⊢! φ) : 𝓢 ⊢! ψ ==> φ

@[deprecated LO.Entailment.imply₁' (since := "2026-05-27")]

def LO.Entailment.dhyp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] (ψ : F) (b : 𝓢 ⊢ φ) : 𝓢 ⊢ ψ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.dhyp ψ b = LO.Entailment.imply₁' b

class LO.Entailment.HasAxiomImply₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.imply₂ = LO.Entailment.HasAxiomImply₂.imply₂ φ ψ χ

@[simp]

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

def LO.Entailment.imply₂' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomImply₂ 𝓢] (d₁ : 𝓢 ⊢ φ ==> ψ ==> χ) (d₂ : 𝓢 ⊢ φ ==> ψ) (d₃ : 𝓢 ⊢ φ) : 𝓢 ⊢ χ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.imply₂' d₁ d₂ d₃ = LO.Entailment.imply₂⨀d₁⨀d₂⨀d₃

theorem LO.Entailment.imply₂'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomImply₂ 𝓢] (d₁ : 𝓢 ⊢! φ ==> ψ ==> χ) (d₂ : 𝓢 ⊢! φ ==> ψ) (d₃ : 𝓢 ⊢! φ) : 𝓢 ⊢! χ

class LO.Entailment.HasAxiomAndElim {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ

  Imported declaration from the Incompleteness formalization.

• and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.and₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.and₁ = LO.Entailment.HasAxiomAndElim.and₁ φ ψ

@[simp]

theorem LO.Entailment.and₁! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢! φ ⋏ ψ ==> φ

def LO.Entailment.and₁' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ φ

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Entailment.andLeft {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ φ

Alias of LO.Entailment.and₁'.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.andLeft = @LO.Entailment.and₁'

theorem LO.Entailment.and₁'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! φ

theorem LO.Entailment.and_left! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! φ

Alias of LO.Entailment.and₁'!.

def LO.Entailment.and₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.and₂ = LO.Entailment.HasAxiomAndElim.and₂ φ ψ

@[simp]

theorem LO.Entailment.and₂! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢! φ ⋏ ψ ==> ψ

def LO.Entailment.and₂' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ψ

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Entailment.andRight {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ψ

Alias of LO.Entailment.and₂'.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.andRight = @LO.Entailment.and₂'

theorem LO.Entailment.and₂'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ψ

theorem LO.Entailment.and_right! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ψ

Alias of LO.Entailment.and₂'!.

class LO.Entailment.HasAxiomAndInst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.and₃ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomAndInst 𝓢] : 𝓢 ⊢ φ ==> ψ ==> φ ⋏ ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.and₃ = LO.Entailment.HasAxiomAndInst.and₃ φ ψ

@[simp]

theorem LO.Entailment.and₃! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomAndInst 𝓢] : 𝓢 ⊢! φ ==> ψ ==> φ ⋏ ψ

def LO.Entailment.and₃' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (d₁ : 𝓢 ⊢ φ) (d₂ : 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⋏ ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.and₃' d₁ d₂ = LO.Entailment.and₃⨀d₁⨀d₂

def LO.Entailment.andIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (d₁ : 𝓢 ⊢ φ) (d₂ : 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⋏ ψ

Alias of LO.Entailment.and₃'.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.andIntro = @LO.Entailment.and₃'

theorem LO.Entailment.and₃'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (d₁ : 𝓢 ⊢! φ) (d₂ : 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ⋏ ψ

theorem LO.Entailment.and_intro! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (d₁ : 𝓢 ⊢! φ) (d₂ : 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ⋏ ψ

Alias of LO.Entailment.and₃'!.

class LO.Entailment.HasAxiomOrInst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ

  Imported declaration from the Incompleteness formalization.

• or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.or₁ = LO.Entailment.HasAxiomOrInst.or₁ φ ψ

@[simp]

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

def LO.Entailment.or₁' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢ φ) : 𝓢 ⊢ φ ⋎ ψ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.or₁'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢! φ) : 𝓢 ⊢! φ ⋎ ψ

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.or₂ = LO.Entailment.HasAxiomOrInst.or₂ φ ψ

@[simp]

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

def LO.Entailment.or₂' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⋎ ψ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.or₂'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ⋎ ψ

class LO.Entailment.HasAxiomOrElim {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.or₃ = LO.Entailment.HasAxiomOrElim.or₃ φ ψ χ

@[simp]

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

def LO.Entailment.or₃'' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ ==> χ) (d₂ : 𝓢 ⊢ ψ ==> χ) : 𝓢 ⊢ φ ⋎ ψ ==> χ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.or₃'' d₁ d₂ = LO.Entailment.or₃⨀d₁⨀d₂

theorem LO.Entailment.or₃''! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ ==> χ) (d₂ : 𝓢 ⊢! ψ ==> χ) : 𝓢 ⊢! φ ⋎ ψ ==> χ

def LO.Entailment.or₃''' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ ==> χ) (d₂ : 𝓢 ⊢ ψ ==> χ) (d₃ : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ χ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.or₃''' d₁ d₂ d₃ = LO.Entailment.or₃⨀d₁⨀d₂⨀d₃

def LO.Entailment.orCases {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ ==> χ) (d₂ : 𝓢 ⊢ ψ ==> χ) (d₃ : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ χ

Alias of LO.Entailment.or₃'''.

---

Imported declaration from the Incompleteness formalization.

Equations

• @LO.Entailment.orCases = @LO.Entailment.or₃'''

theorem LO.Entailment.or₃'''! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ ==> χ) (d₂ : 𝓢 ⊢! ψ ==> χ) (d₃ : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! χ

theorem LO.Entailment.or_cases! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ ==> χ) (d₂ : 𝓢 ⊢! ψ ==> χ) (d₃ : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! χ

Alias of LO.Entailment.or₃'''!.

class LO.Entailment.HasAxiomEFQ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• efq (φ : F) : 𝓢 ⊢ Axioms.EFQ φ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.efq {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢ ⊥ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.efq = LO.Entailment.HasAxiomEFQ.efq φ

@[simp]

theorem LO.Entailment.efq! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢! ⊥ ==> φ

def LO.Entailment.efq' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomEFQ 𝓢] (b : 𝓢 ⊢ ⊥) : 𝓢 ⊢ φ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.efq'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomEFQ 𝓢] (h : 𝓢 ⊢! ⊥) : 𝓢 ⊢! φ

class LO.Entailment.HasAxiomLEM {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• lem (φ : F) : 𝓢 ⊢ Axioms.LEM φ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.lem {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [HasAxiomLEM 𝓢] : 𝓢 ⊢ φ ⋎ ∼φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.lem = LO.Entailment.HasAxiomLEM.lem φ

@[simp]

theorem LO.Entailment.lem! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [HasAxiomLEM 𝓢] : 𝓢 ⊢! φ ⋎ ∼φ

class LO.Entailment.HasAxiomDNE {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.dne = LO.Entailment.HasAxiomDNE.dne φ

@[simp]

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

def LO.Entailment.dne' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomDNE 𝓢] (b : 𝓢 ⊢ ∼∼φ) : 𝓢 ⊢ φ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.dne'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomDNE 𝓢] (h : 𝓢 ⊢! ∼∼φ) : 𝓢 ⊢! φ

class LO.Entailment.HasAxiomWeakLEM {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• wlem (φ : F) : 𝓢 ⊢ Axioms.WeakLEM φ

  Imported declaration from the Incompleteness formalization.

def LO.Entailment.wlem {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [HasAxiomWeakLEM 𝓢] : 𝓢 ⊢ ∼φ ⋎ ∼∼φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.wlem = LO.Entailment.HasAxiomWeakLEM.wlem φ

@[simp]

theorem LO.Entailment.wlem! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [HasAxiomWeakLEM 𝓢] : 𝓢 ⊢! ∼φ ⋎ ∼∼φ

class LO.Entailment.HasAxiomDummett {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• dummett (φ ψ : F) : 𝓢 ⊢ Axioms.Dummett φ ψ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.dummett = LO.Entailment.HasAxiomDummett.dummett φ ψ

@[simp]

theorem LO.Entailment.dummett! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [HasAxiomDummett 𝓢] : 𝓢 ⊢! Axioms.Dummett φ ψ

class LO.Entailment.HasAxiomPeirce {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• peirce (φ ψ : F) : 𝓢 ⊢ Axioms.Peirce φ ψ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.peirce = LO.Entailment.HasAxiomPeirce.peirce φ ψ

@[simp]

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

class LO.Entailment.NegationEquiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Negation ∼φ is equivalent to φ ==> ⊥ on system.

This is weaker asssumption than "introducing ∼φ as an abbreviation of φ ==> ⊥" (NegAbbrev).

• negEquiv (φ : F) : 𝓢 ⊢ Axioms.NegEquiv φ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.negEquiv = LO.Entailment.NegationEquiv.negEquiv φ

@[simp]

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

class LO.Entailment.HasAxiomElimContra {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• elimContra (φ ψ : F) : 𝓢 ⊢ Axioms.ElimContra φ ψ

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.elimContra = LO.Entailment.HasAxiomElimContra.elimContra φ ψ

@[simp]

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

class LO.Entailment.Minimal {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) extends LO.Entailment.ModusPonens 𝓢, LO.Entailment.NegationEquiv 𝓢, LO.Entailment.HasAxiomVerum 𝓢, LO.Entailment.HasAxiomImply₁ 𝓢, LO.Entailment.HasAxiomImply₂ 𝓢, LO.Entailment.HasAxiomAndElim 𝓢, LO.Entailment.HasAxiomAndInst 𝓢, LO.Entailment.HasAxiomOrInst 𝓢, LO.Entailment.HasAxiomOrElim 𝓢 : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : F) : 𝓢 ⊢ Axioms.NegEquiv φ
• verum : 𝓢 ⊢ Axioms.Verum
• imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
• imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
• and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
• and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
• and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
• or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
• or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
• or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ

class LO.Entailment.Intuitionistic {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) extends LO.Entailment.Minimal 𝓢, LO.Entailment.HasAxiomEFQ 𝓢 : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : F) : 𝓢 ⊢ Axioms.NegEquiv φ
• verum : 𝓢 ⊢ Axioms.Verum
• imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
• imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
• and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
• and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
• and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
• or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
• or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
• or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
• efq (φ : F) : 𝓢 ⊢ Axioms.EFQ φ

class LO.Entailment.Classical {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] (𝓢 : S) extends LO.Entailment.Minimal 𝓢, LO.Entailment.HasAxiomDNE 𝓢 : Type (max u_2 u_3)

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : F) : 𝓢 ⊢ Axioms.NegEquiv φ
• verum : 𝓢 ⊢ Axioms.Verum
• imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
• imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
• and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
• and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
• and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
• or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
• or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
• or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
• dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ

def LO.Entailment.negEquiv'.mp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢ ∼φ → 𝓢 ⊢ φ ==> ⊥

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.negEquiv'.mp h = LO.Entailment.and₁' LO.Entailment.negEquiv⨀h

def LO.Entailment.negEquiv'.mpr {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢ φ ==> ⊥ → 𝓢 ⊢ ∼φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.negEquiv'.mpr h = LO.Entailment.and₂' LO.Entailment.negEquiv⨀h

theorem LO.Entailment.negEquiv'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢! ∼φ ↔ 𝓢 ⊢! φ ==> ⊥

def LO.Entailment.iffIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (b₁ : 𝓢 ⊢ φ ==> ψ) (b₂ : 𝓢 ⊢ ψ ==> φ) : 𝓢 ⊢ φ <=> ψ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.iffIntro b₁ b₂ = LO.Entailment.andIntro b₁ b₂

theorem LO.Entailment.iff_intro! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (h₁ : 𝓢 ⊢! φ ==> ψ) (h₂ : 𝓢 ⊢! ψ ==> φ) : 𝓢 ⊢! φ <=> ψ

Imported declaration from the Incompleteness formalization.

theorem LO.Entailment.and_intro_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢! φ ⋏ ψ ↔ 𝓢 ⊢! φ ∧ 𝓢 ⊢! ψ

theorem LO.Entailment.iff_intro_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢! φ <=> ψ ↔ 𝓢 ⊢! φ ==> ψ ∧ 𝓢 ⊢! ψ ==> φ

theorem LO.Entailment.provable_iff_of_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] (h : 𝓢 ⊢! φ <=> ψ) : 𝓢 ⊢! φ ↔ 𝓢 ⊢! ψ

def LO.Entailment.impId {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (φ : F) : 𝓢 ⊢ φ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.impId φ = LO.Entailment.imply₂⨀LO.Entailment.imply₁⨀LO.Entailment.imply₁

@[simp]

theorem LO.Entailment.imp_id! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] : 𝓢 ⊢! φ ==> φ

Imported declaration from the Incompleteness formalization.

def LO.Entailment.iffId {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (φ : F) : 𝓢 ⊢ φ <=> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.iffId φ = LO.Entailment.and₃' (LO.Entailment.impId φ) (LO.Entailment.impId φ)

@[simp]

theorem LO.Entailment.iff_id! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] : 𝓢 ⊢! φ <=> φ

Imported declaration from the Incompleteness formalization.

@[implicit_reducible]

instance LO.Entailment.instNegationEquivOfNegAbbrevOfHasAxiomImply₁OfHasAxiomImply₂OfHasAxiomAndInst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [NegAbbrev F] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] [HasAxiomAndInst 𝓢] : NegationEquiv 𝓢

Equations

• LO.Entailment.instNegationEquivOfNegAbbrevOfHasAxiomImply₁OfHasAxiomImply₂OfHasAxiomAndInst = { negEquiv := fun (φ : F) => ⋯.mpr (LO.Entailment.iffId (φ ==> ⊥)) }

def LO.Entailment.notbot {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] [NegationEquiv 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ ∼⊥

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.notbot = LO.Entailment.negEquiv'.mpr (LO.Entailment.impId ⊥)

@[simp]

theorem LO.Entailment.notbot! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] [NegationEquiv 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢! ∼⊥

def LO.Entailment.mdp₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomImply₂ 𝓢] (bqr : 𝓢 ⊢ φ ==> ψ ==> χ) (bq : 𝓢 ⊢ φ ==> ψ) : 𝓢 ⊢ φ ==> χ

Imported declaration from the Incompleteness formalization.

Equations

• bqr⨀₁bq = LO.Entailment.imply₂⨀bqr⨀bq

theorem LO.Entailment.mdp₁! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomImply₂ 𝓢] (hqr : 𝓢 ⊢! φ ==> ψ ==> χ) (hq : 𝓢 ⊢! φ ==> ψ) : 𝓢 ⊢! φ ==> χ

def LO.Entailment.«term_⨀₁_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀₁_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₁_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₁") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀₁__1» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀₁__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₁__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₁") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.mdp₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] {s : F} [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (bqr : 𝓢 ⊢ φ ==> ψ ==> χ ==> s) (bq : 𝓢 ⊢ φ ==> ψ ==> χ) : 𝓢 ⊢ φ ==> ψ ==> s

Imported declaration from the Incompleteness formalization.

Equations

• bqr⨀₂bq = LO.Entailment.imply₁' LO.Entailment.imply₂⨀₁bqr⨀₁bq

theorem LO.Entailment.mdp₂! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] {s : F} [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (hqr : 𝓢 ⊢! φ ==> ψ ==> χ ==> s) (hq : 𝓢 ⊢! φ ==> ψ ==> χ) : 𝓢 ⊢! φ ==> ψ ==> s

def LO.Entailment.«term_⨀₂_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀₂_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₂_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₂") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀₂__1» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀₂__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₂__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₂") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.mdp₃ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] {s t : F} [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (bqr : 𝓢 ⊢ φ ==> ψ ==> χ ==> s ==> t) (bq : 𝓢 ⊢ φ ==> ψ ==> χ ==> s) : 𝓢 ⊢ φ ==> ψ ==> χ ==> t

Imported declaration from the Incompleteness formalization.

Equations

• bqr⨀₃bq = LO.Entailment.imply₁' (LO.Entailment.imply₁' LO.Entailment.imply₂)⨀₂bqr⨀₂bq

theorem LO.Entailment.mdp₃! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] {s t : F} [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (hqr : 𝓢 ⊢! φ ==> ψ ==> χ ==> s ==> t) (hq : 𝓢 ⊢! φ ==> ψ ==> χ ==> s) : 𝓢 ⊢! φ ==> ψ ==> χ ==> t

def LO.Entailment.«term_⨀₃_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀₃_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₃_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₃") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀₃__1» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀₃__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₃__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₃") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.mdp₄ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] {s t u : F} [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (bqr : 𝓢 ⊢ φ ==> ψ ==> χ ==> s ==> t ==> u) (bq : 𝓢 ⊢ φ ==> ψ ==> χ ==> s ==> t) : 𝓢 ⊢ φ ==> ψ ==> χ ==> s ==> u

Imported declaration from the Incompleteness formalization.

Equations

• bqr⨀₄bq = LO.Entailment.imply₁' (LO.Entailment.imply₁' (LO.Entailment.imply₁' LO.Entailment.imply₂))⨀₃bqr⨀₃bq

theorem LO.Entailment.mdp₄! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] {s t u : F} [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (hqr : 𝓢 ⊢! φ ==> ψ ==> χ ==> s ==> t ==> u) (hq : 𝓢 ⊢! φ ==> ψ ==> χ ==> s ==> t) : 𝓢 ⊢! φ ==> ψ ==> χ ==> s ==> u

def LO.Entailment.«term_⨀₄_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀₄_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₄_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₄") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀₄__1» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.«term_⨀₄__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₄__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₄") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.impTrans'' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (bpq : 𝓢 ⊢ φ ==> ψ) (bqr : 𝓢 ⊢ ψ ==> χ) : 𝓢 ⊢ φ ==> χ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.impTrans'' bpq bqr = LO.Entailment.imply₂⨀LO.Entailment.imply₁' bqr⨀bpq

theorem LO.Entailment.imp_trans''! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (hpq : 𝓢 ⊢! φ ==> ψ) (hqr : 𝓢 ⊢! ψ ==> χ) : 𝓢 ⊢! φ ==> χ

theorem LO.Entailment.unprovable_imp_trans''! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (hpq : 𝓢 ⊢! φ ==> ψ) : 𝓢 ⊬ φ ==> χ → 𝓢 ⊬ ψ ==> χ

def LO.Entailment.iffTrans'' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (h₁ : 𝓢 ⊢ φ <=> ψ) (h₂ : 𝓢 ⊢ ψ <=> χ) : 𝓢 ⊢ φ <=> χ

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.iff_trans''! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (h₁ : 𝓢 ⊢! φ <=> ψ) (h₂ : 𝓢 ⊢! ψ <=> χ) : 𝓢 ⊢! φ <=> χ

theorem LO.Entailment.unprovable_iff! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (H : 𝓢 ⊢! φ <=> ψ) : 𝓢 ⊬ φ ↔ 𝓢 ⊬ ψ

def LO.Entailment.imply₁₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (φ ψ χ : F) : 𝓢 ⊢ φ ==> ψ ==> χ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.imply₁₁ φ ψ χ = LO.Entailment.impTrans'' LO.Entailment.imply₁ LO.Entailment.imply₁

@[simp]

theorem LO.Entailment.imply₁₁! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (φ ψ χ : F) : 𝓢 ⊢! φ ==> ψ ==> χ ==> φ

def LO.Entailment.implyAnd {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (bq : 𝓢 ⊢ φ ==> ψ) (br : 𝓢 ⊢ φ ==> χ) : 𝓢 ⊢ φ ==> ψ ⋏ χ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.implyAnd bq br = LO.Entailment.imply₁' LO.Entailment.and₃⨀₁bq⨀₁br

theorem LO.Entailment.imply_and! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (hq : 𝓢 ⊢! φ ==> ψ) (hr : 𝓢 ⊢! φ ==> χ) : 𝓢 ⊢! φ ==> ψ ⋏ χ

def LO.Entailment.andComm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (φ ψ : F) : 𝓢 ⊢ φ ⋏ ψ ==> ψ ⋏ φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.andComm φ ψ = LO.Entailment.implyAnd LO.Entailment.and₂ LO.Entailment.and₁

theorem LO.Entailment.and_comm! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] : 𝓢 ⊢! φ ⋏ ψ ==> ψ ⋏ φ

def LO.Entailment.andComm' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (h : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ψ ⋏ φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.andComm' h = LO.Entailment.andComm φ ψ⨀h

theorem LO.Entailment.and_comm'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (h : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ψ ⋏ φ

def LO.Entailment.iffComm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (φ ψ : F) : 𝓢 ⊢ φ <=> ψ ==> ψ <=> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.iffComm φ ψ = LO.Entailment.andComm (φ ==> ψ) (ψ ==> φ)

theorem LO.Entailment.iff_comm! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] : 𝓢 ⊢! φ <=> ψ ==> ψ <=> φ

def LO.Entailment.iffComm' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (h : 𝓢 ⊢ φ <=> ψ) : 𝓢 ⊢ ψ <=> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.iffComm' h = LO.Entailment.iffComm φ ψ⨀h

theorem LO.Entailment.iff_comm'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (h : 𝓢 ⊢! φ <=> ψ) : 𝓢 ⊢! ψ <=> φ

def LO.Entailment.andImplyIffImplyImply {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (φ ψ χ : F) : 𝓢 ⊢ (φ ⋏ ψ ==> χ) <=> (φ ==> ψ ==> χ)

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.and_imply_iff_imply_imply! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] : 𝓢 ⊢! (φ ⋏ ψ ==> χ) <=> (φ ==> ψ ==> χ)

def LO.Entailment.andImplyIffImplyImply'.mp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ ==> χ) : 𝓢 ⊢ φ ==> ψ ==> χ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.andImplyIffImplyImply'.mp d = LO.Entailment.and₁' (LO.Entailment.andImplyIffImplyImply φ ψ χ)⨀d

def LO.Entailment.andImplyIffImplyImply'.mpr {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] (d : 𝓢 ⊢ φ ==> ψ ==> χ) : 𝓢 ⊢ φ ⋏ ψ ==> χ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.andImplyIffImplyImply'.mpr d = LO.Entailment.and₂' (LO.Entailment.andImplyIffImplyImply φ ψ χ)⨀d

theorem LO.Entailment.and_imply_iff_imply_imply'! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomImply₂ 𝓢] : 𝓢 ⊢! φ ⋏ ψ ==> χ ↔ 𝓢 ⊢! φ ==> ψ ==> χ

def LO.Entailment.implyLeftVerum {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomVerum 𝓢] [HasAxiomImply₁ 𝓢] : 𝓢 ⊢ φ ==> ⊤

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.implyLeftVerum = LO.Entailment.imply₁' LO.Entailment.verum

@[simp]

theorem LO.Entailment.implyLeftVerum! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomImply₁ 𝓢] [HasAxiomVerum 𝓢] : 𝓢 ⊢! φ ==> ⊤

@[implicit_reducible]

instance LO.Entailment.instDeductiveExplosionOfModusPonensOfHasAxiomEFQ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] [(𝓢 : S) → ModusPonens 𝓢] [(𝓢 : S) → HasAxiomEFQ 𝓢] : DeductiveExplosion S

Equations

• LO.Entailment.instDeductiveExplosionOfModusPonensOfHasAxiomEFQ = { dexp := fun {𝓢 : S} (b : 𝓢 ⊢ ⊥) (x : F) => LO.Entailment.efq⨀b }

def LO.Entailment.conj₂Nth {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (n : ℕ) (hn : n < Γ.length) : 𝓢 ⊢ ⋀Γ ==> Γ[n]

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.conj₂Nth [] x x_1 = ⋯.elim
• LO.Entailment.conj₂Nth [ψ] 0 x_3 = LO.Entailment.impId ψ
• LO.Entailment.conj₂Nth (φ :: ψ :: Γ) 0 x_3 = LO.Entailment.and₁
• LO.Entailment.conj₂Nth (φ :: ψ :: Γ) n.succ hn = LO.Entailment.impTrans'' LO.Entailment.and₂ (LO.Entailment.conj₂Nth (ψ :: Γ) n ⋯)

theorem LO.Entailment.conj₂_nth! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (n : ℕ) (hn : n < Γ.length) : 𝓢 ⊢! ⋀Γ ==> Γ[n]

Imported declaration from the Incompleteness formalization.

def LO.Entailment.generalConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} {φ : F} (h : φ ∈ Γ) : 𝓢 ⊢ Γ.conj ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.generalConj h_2 = ⋯.elim
• LO.Entailment.generalConj h_2 = if e : φ = ψ then LO.Entailment.cast ⋯ LO.Entailment.and₁ else have this := ⋯; LO.Entailment.impTrans'' LO.Entailment.and₂ (LO.Entailment.generalConj this)

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

def LO.Entailment.conjIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (b : (φ : F) → φ ∈ Γ → 𝓢 ⊢ φ) : 𝓢 ⊢ Γ.conj

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.conjIntro [] b_2 = LO.Entailment.verum
• LO.Entailment.conjIntro (ψ :: Γ_2) b_2 = LO.Entailment.andIntro (b_2 ψ ⋯) (LO.Entailment.conjIntro Γ_2 fun (ψ_1 : F) (hq : ψ_1 ∈ Γ_2) => b_2 ψ_1 ⋯)

def LO.Entailment.implyConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢ φ ==> ψ) : 𝓢 ⊢ φ ==> Γ.conj

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.implyConj φ [] b_2 = LO.Entailment.imply₁' LO.Entailment.verum
• LO.Entailment.implyConj φ (ψ :: Γ_2) b_2 = LO.Entailment.implyAnd (b_2 ψ ⋯) (LO.Entailment.implyConj φ Γ_2 fun (ψ_1 : F) (hq : ψ_1 ∈ Γ_2) => b_2 ψ_1 ⋯)

def LO.Entailment.conjImplyConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : List F} (h : Δ ⊆ Γ) : 𝓢 ⊢ Γ.conj ==> Δ.conj

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.conjImplyConj h = LO.Entailment.implyConj Γ.conj Δ fun (x : F) (hq : x ∈ Δ) => LO.Entailment.generalConj ⋯

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.generalConj' h = LO.Entailment.cast ⋯ (LO.Entailment.conj₂Nth Γ (List.idxOf φ Γ) ⋯)

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

def LO.Entailment.conjIntro' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (b : (φ : F) → φ ∈ Γ → 𝓢 ⊢ φ) : 𝓢 ⊢ ⋀Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.conjIntro' [] b_2 = LO.Entailment.verum
• LO.Entailment.conjIntro' [ψ] b_2 = b_2 (⋀[ψ]) ⋯
• LO.Entailment.conjIntro' (ψ :: χ :: Γ_2) b_2 = ⋯.mpr (LO.Entailment.andIntro (b_2 ψ ⋯) (LO.Entailment.conjIntro' (χ :: Γ_2) fun (φ_1 : F) (a : φ_1 ∈ χ :: Γ_2) => b_2 φ_1 ⋯))

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

def LO.Entailment.implyConj' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢ φ ==> ψ) : 𝓢 ⊢ φ ==> ⋀Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.implyConj' φ [] b_2 = LO.Entailment.imply₁' LO.Entailment.verum
• LO.Entailment.implyConj' φ [ψ] b_2 = b_2 (⋀[ψ]) ⋯
• LO.Entailment.implyConj' φ (ψ :: χ :: Γ_2) b_2 = ⋯.mpr (LO.Entailment.implyAnd (b_2 ψ ⋯) (LO.Entailment.implyConj' φ (χ :: Γ_2) fun (ψ_1 : F) (hq : ψ_1 ∈ χ :: Γ_2) => b_2 ψ_1 ⋯))

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

def LO.Entailment.conjImplyConj' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : List F} (h : Δ ⊆ Γ) : 𝓢 ⊢ ⋀Γ ==> ⋀Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.conjImplyConj' h = LO.Entailment.implyConj' (⋀Γ) Δ fun (x : F) (hq : x ∈ Δ) => LO.Entailment.generalConj' ⋯

@[reducible]

def LO.Entailment.Minimal.ofEquiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {G : Type u_3} {T : Type u_4} [Entailment G T] [LogicalConnective G] (𝓢 : S) [Entailment.Minimal 𝓢] (𝓣 : T) (f : G →ˡᶜ F) (e : (φ : G) → 𝓢 ⊢ f φ ≃ 𝓣 ⊢ φ) : Entailment.Minimal 𝓣

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible]

def LO.Entailment.Classical.ofEquiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment F S] {G : Type u_3} {T : Type u_4} [Entailment G T] [LogicalConnective G] (𝓢 : S) [Entailment.Classical 𝓢] (𝓣 : T) (f : G →ˡᶜ F) (e : (φ : G) → 𝓢 ⊢ f φ ≃ 𝓣 ⊢ φ) : Entailment.Classical 𝓣

Imported declaration from the Incompleteness formalization.

Equations

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