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

Equations

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

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

Equations

• ⋯ = ⋯

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

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ

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

Alias of LO.System.ModusPonens.mdp.

Equations

• @LO.System.mdp = @LO.System.ModusPonens.mdp

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

Equations

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

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

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

Equations

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

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

• verum : 𝓢 ⊢ LO.Axioms.Verum

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

Equations

• LO.System.verum = LO.System.HasAxiomVerum.verum

@[simp]

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

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

@[deprecated LO.System.imply₁']

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

Equations

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

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

Alias of LO.System.and₁'.

Equations

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

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

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

Alias of LO.System.and₁'!.

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

Equations

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

@[simp]

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

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

Equations

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

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

Alias of LO.System.and₂'.

Equations

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

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

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

Alias of LO.System.and₂'!.

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

Alias of LO.System.and₃'.

Equations

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

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

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

Alias of LO.System.and₃'!.

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

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

Equations

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

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

Alias of LO.System.or₃'''.

Equations

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

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

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

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

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

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

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

Equations

• LO.System.efq = LO.System.HasAxiomEFQ.efq φ

@[simp]

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

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

Equations

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

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

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

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

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

Equations

• LO.System.lem = LO.System.HasAxiomLEM.lem φ

@[simp]

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

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

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

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

Equations

• LO.System.dne = LO.System.HasAxiomDNE.dne φ

@[simp]

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

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

Equations

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

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

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

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

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

Equations

• LO.System.wlem = LO.System.HasAxiomWeakLEM.wlem φ

@[simp]

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

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

class LO.System.NegationEquiv {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System 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).

• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ

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

Equations

• LO.System.neg_equiv = LO.System.NegationEquiv.neg_equiv φ

@[simp]

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

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

• elim_contra : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.ElimContra φ ψ

def LO.System.elim_contra {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.HasAxiomElimContra 𝓢] : 𝓢 ⊢ (∼ψ ➝ ∼φ) ➝ φ ➝ ψ

Equations

• LO.System.elim_contra = LO.System.HasAxiomElimContra.elim_contra φ ψ

@[simp]

theorem LO.System.elim_contra! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.HasAxiomElimContra 𝓢] : 𝓢 ⊢! (∼ψ ➝ ∼φ) ➝ φ ➝ ψ

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

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

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

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

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

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

def LO.System.neg_equiv'.mp {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndElim 𝓢] [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ ∼φ → 𝓢 ⊢ φ ➝ ⊥

Equations

• LO.System.neg_equiv'.mp h = LO.System.and₁' LO.System.neg_equiv⨀h

def LO.System.neg_equiv'.mpr {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndElim 𝓢] [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ φ ➝ ⊥ → 𝓢 ⊢ ∼φ

Equations

• LO.System.neg_equiv'.mpr h = LO.System.and₂' LO.System.neg_equiv⨀h

theorem LO.System.neg_equiv'! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndElim 𝓢] [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! ∼φ ↔ 𝓢 ⊢! φ ➝ ⊥

def LO.System.iffIntro {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndInst 𝓢] (b₁ : 𝓢 ⊢ φ ➝ ψ) (b₂ : 𝓢 ⊢ ψ ➝ φ) : 𝓢 ⊢ φ ⭤ ψ

Equations

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

def LO.System.iff_intro! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndInst 𝓢] (h₁ : 𝓢 ⊢! φ ➝ ψ) (h₂ : 𝓢 ⊢! ψ ➝ φ) : 𝓢 ⊢! φ ⭤ ψ

Equations

• ⋯ = ⋯

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

theorem LO.System.iff_intro_iff {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndInst 𝓢] [LO.System.HasAxiomAndElim 𝓢] : 𝓢 ⊢! φ ⭤ ψ ↔ 𝓢 ⊢! φ ➝ ψ ∧ 𝓢 ⊢! ψ ➝ φ

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

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

Equations

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

@[simp]

def LO.System.imp_id! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] : 𝓢 ⊢! φ ➝ φ

Equations

• ⋯ = ⋯

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

Equations

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

@[simp]

def LO.System.iff_id! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndInst 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] : 𝓢 ⊢! φ ⭤ φ

Equations

• ⋯ = ⋯

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

Equations

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

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

Equations

• LO.System.notbot = LO.System.neg_equiv'.mpr (LO.System.impId ⊥)

@[simp]

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

Equations

• LO.System.iffTrans'' h₁ h₂ = LO.System.iffIntro (LO.System.impTrans'' (LO.System.and₁' h₁) (LO.System.and₁' h₂)) (LO.System.impTrans'' (LO.System.and₂' h₂) (LO.System.and₂' h₁))

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

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

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

Equations

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

@[simp]

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

def LO.System.iffComm {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndInst 𝓢] [LO.System.HasAxiomAndElim 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] (φ ψ : F) : 𝓢 ⊢ φ ⭤ ψ ➝ ψ ⭤ φ

Equations

• LO.System.iffComm φ ψ = LO.System.andComm (φ ➝ ψ) (ψ ➝ φ)

theorem LO.System.iff_comm! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndInst 𝓢] [LO.System.HasAxiomAndElim 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] : 𝓢 ⊢! φ ⭤ ψ ➝ ψ ⭤ φ

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

def LO.System.imply_left_verum {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomVerum 𝓢] [LO.System.HasAxiomImply₁ 𝓢] : 𝓢 ⊢ φ ➝ ⊤

Equations

• LO.System.imply_left_verum = LO.System.imply₁' LO.System.verum

@[simp]

theorem LO.System.imply_left_verum! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomVerum 𝓢] : 𝓢 ⊢! φ ➝ ⊤

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

Equations

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

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

Equations

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

def LO.System.conj₂_nth! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.ModusPonens 𝓢] [LO.System.Minimal 𝓢] (Γ : List F) (n : ℕ) (hn : n < Γ.length) : 𝓢 ⊢! ⋀Γ ➝ Γ[n]

Equations

• ⋯ = ⋯

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

• LO.System.Minimal.ofEquiv 𝓢 𝓣 f e = LO.System.Minimal.mk

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

Equations

• LO.System.Classical.ofEquiv 𝓢 𝓣 f e = LO.System.Classical.mk