Foundation.Logic.HilbertStyle.Basic

source

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

𝓢 ⊢ ψ

Equations

LO.System.cast e b = e ▸ b

source

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

𝓢 ⊢! ψ

Equations

⋯ = ⋯

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ

Alias of LO.System.ModusPonens.mdp.

Equations

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

source

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

source

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

𝓢 ⊢! φ ➝ ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ

source

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

source

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

Type u_3

verum : 𝓢 ⊢ Axioms.Verum

Instances

source

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

𝓢 ⊢ ⊤

Equations

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

source

@[simp]

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

𝓢 ⊢! ⊤

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ φ ➝ ψ ➝ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ➝ ψ ➝ φ

source

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

𝓢 ⊢ ψ ➝ φ

Equations

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

source

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

𝓢 ⊢! ψ ➝ φ

source

@[deprecated LO.System.imply₁']

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

𝓢 ⊢ ψ ➝ φ

Equations

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

source

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

Type (max u_2 u_3)

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

Instances

source

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

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

Equations

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

source

@[simp]

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

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

source

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

𝓢 ⊢ χ

Equations

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

source

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

𝓢 ⊢! χ

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ φ ⋏ ψ ➝ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ⋏ ψ ➝ φ

source

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

𝓢 ⊢ φ

Equations

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

source

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

𝓢 ⊢ φ

Alias of LO.System.and₁'.

Equations

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

source

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

𝓢 ⊢! φ

source

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

𝓢 ⊢! φ

Alias of LO.System.and₁'!.

source

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

𝓢 ⊢ φ ⋏ ψ ➝ ψ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ⋏ ψ ➝ ψ

source

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

𝓢 ⊢ ψ

Equations

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

source

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

𝓢 ⊢ ψ

Alias of LO.System.and₂'.

Equations

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

source

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

𝓢 ⊢! ψ

source

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

𝓢 ⊢! ψ

Alias of LO.System.and₂'!.

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ φ ➝ ψ ➝ φ ⋏ ψ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ➝ ψ ➝ φ ⋏ ψ

source

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

𝓢 ⊢ φ ⋏ ψ

Equations

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

source

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

𝓢 ⊢ φ ⋏ ψ

Alias of LO.System.and₃'.

Equations

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

source

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

𝓢 ⊢! φ ⋏ ψ

source

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

𝓢 ⊢! φ ⋏ ψ

Alias of LO.System.and₃'!.

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ φ ➝ φ ⋎ ψ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ➝ φ ⋎ ψ

source

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

𝓢 ⊢ φ ⋎ ψ

Equations

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

source

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

𝓢 ⊢! φ ⋎ ψ

source

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

𝓢 ⊢ ψ ➝ φ ⋎ ψ

Equations

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

source

@[simp]

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

𝓢 ⊢! ψ ➝ φ ⋎ ψ

source

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

𝓢 ⊢ φ ⋎ ψ

Equations

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

source

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

𝓢 ⊢! φ ⋎ ψ

source

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

Type (max u_2 u_3)

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

Instances

source

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

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

Equations

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

source

@[simp]

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

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

source

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

𝓢 ⊢ φ ⋎ ψ ➝ χ

Equations

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

source

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

𝓢 ⊢! φ ⋎ ψ ➝ χ

source

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

𝓢 ⊢ χ

Equations

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

source

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

𝓢 ⊢ χ

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

Equations

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

source

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

𝓢 ⊢! χ

source

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

𝓢 ⊢! χ

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

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ ⊥ ➝ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! ⊥ ➝ φ

source

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

𝓢 ⊢ φ

Equations

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

source

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

𝓢 ⊢! φ

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ φ ⋎ ∼φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ⋎ ∼φ

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ ∼∼φ ➝ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! ∼∼φ ➝ φ

source

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

𝓢 ⊢ φ

Equations

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

source

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

𝓢 ⊢! φ

source

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

Type (max u_2 u_3)

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

Instances

source

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

𝓢 ⊢ ∼φ ⋎ ∼∼φ

Equations

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

source

@[simp]

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

𝓢 ⊢! ∼φ ⋎ ∼∼φ

source

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

Type (max u_2 u_3)

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

Instances

source

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

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

Equations

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

source

@[simp]

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

𝓢 ⊢! Axioms.Dummett φ ψ

source

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

Type (max u_2 u_3)

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

Instances

LO.System.instHasAxiomPeirceOfHasAxiomDNE

source

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

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

Equations

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

source

@[simp]

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

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

source

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

Instances

source

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

𝓢 ⊢ ∼φ ⭤ (φ ➝ ⊥)

Equations

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

source

@[simp]

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

𝓢 ⊢! ∼φ ⭤ (φ ➝ ⊥)

source

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

Type (max u_2 u_3)

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

Instances

LO.System.instHasAxiomElimContraOfHasAxiomDNE

source

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

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

Equations

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

source

@[simp]

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

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

source

class LO.System.Minimal {S : Type u_1} {F : Type u_2} [LogicalConnective F] [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) : 𝓢 ⊢ 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 φ ψ χ

Instances

source

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

Type (max u_2 u_3)

mdp {φ ψ : F} : 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
neg_equiv (φ : 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 φ

Instances

source

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

Type (max u_2 u_3)

mdp {φ ψ : F} : 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
neg_equiv (φ : 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 φ

Instances

source

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

𝓢 ⊢ ∼φ → 𝓢 ⊢ φ ➝ ⊥

Equations

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

source

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

𝓢 ⊢ φ ➝ ⊥ → 𝓢 ⊢ ∼φ

Equations

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

source

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

𝓢 ⊢! ∼φ ↔ 𝓢 ⊢! φ ➝ ⊥

source

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

𝓢 ⊢ φ ⭤ ψ

Equations

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

source

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

𝓢 ⊢! φ ⭤ ψ

Equations

⋯ = ⋯

source

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

𝓢 ⊢! φ ⋏ ψ ↔ 𝓢 ⊢! φ ∧ 𝓢 ⊢! ψ

source

theorem LO.System.iff_intro_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] :

𝓢 ⊢! φ ⭤ ψ ↔ 𝓢 ⊢! φ ➝ ψ ∧ 𝓢 ⊢! ψ ➝ φ

source

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

𝓢 ⊢! φ ↔ 𝓢 ⊢! ψ

source

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

𝓢 ⊢ φ ➝ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ➝ φ

Equations

⋯ = ⋯

source

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

𝓢 ⊢ φ ⭤ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ⭤ φ

Equations

⋯ = ⋯

source

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

NegationEquiv 𝓢

Equations

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

source

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

𝓢 ⊢ ∼⊥

Equations

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

source

@[simp]

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

𝓢 ⊢! ∼⊥

source

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

𝓢 ⊢ φ ➝ χ

Equations

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

source

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

𝓢 ⊢! φ ➝ χ

source

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

source

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

source

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

𝓢 ⊢ φ ➝ ψ ➝ s

Equations

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

source

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

𝓢 ⊢! φ ➝ ψ ➝ s

source

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

source

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

source

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

𝓢 ⊢ φ ➝ ψ ➝ χ ➝ t

Equations

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

source

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

𝓢 ⊢! φ ➝ ψ ➝ χ ➝ t

source

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

source

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

source

def LO.System.mdp₄ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] {s t u : F} [HasAxiomImply₁ 𝓢] [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

source

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

𝓢 ⊢! φ ➝ ψ ➝ χ ➝ s ➝ u

source

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

source

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

source

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

𝓢 ⊢ φ ➝ χ

Equations

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

source

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

𝓢 ⊢! φ ➝ χ

source

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

𝓢 ⊬ φ ➝ χ → 𝓢 ⊬ ψ ➝ χ

source

def LO.System.iffTrans'' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} {φ ψ χ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImply₁ 𝓢] [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₁))

source

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

𝓢 ⊢! φ ⭤ χ

source

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

𝓢 ⊬ φ ↔ 𝓢 ⊬ ψ

source

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

𝓢 ⊢ φ ➝ ψ ➝ χ ➝ φ

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ➝ ψ ➝ χ ➝ φ

source

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

𝓢 ⊢ φ ➝ ψ ⋏ χ

Equations

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

source

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

𝓢 ⊢! φ ➝ ψ ⋏ χ

source

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

𝓢 ⊢ φ ⋏ ψ ➝ ψ ⋏ φ

Equations

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

source

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

𝓢 ⊢! φ ⋏ ψ ➝ ψ ⋏ φ

source

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

𝓢 ⊢ ψ ⋏ φ

Equations

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

source

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

𝓢 ⊢! ψ ⋏ φ

source

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

𝓢 ⊢ φ ⭤ ψ ➝ ψ ⭤ φ

Equations

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

source

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

𝓢 ⊢! φ ⭤ ψ ➝ ψ ⭤ φ

source

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

𝓢 ⊢ ψ ⭤ φ

Equations

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

source

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

𝓢 ⊢! ψ ⭤ φ

source

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

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

Equations

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

source

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

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

source

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

𝓢 ⊢ φ ➝ ψ ➝ χ

Equations

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

source

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

𝓢 ⊢ φ ⋏ ψ ➝ χ

Equations

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

source

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

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

source

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

𝓢 ⊢ φ ➝ ⊤

Equations

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

source

@[simp]

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

𝓢 ⊢! φ ➝ ⊤

source

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

DeductiveExplosion S

Equations

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

source

def LO.System.conj₂Nth {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} [ModusPonens 𝓢] [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 ⋯)

source

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

𝓢 ⊢! ⋀Γ ➝ Γ[n]

Equations

⋯ = ⋯

source

def LO.System.generalConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} [ModusPonens 𝓢] [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)

source

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

𝓢 ⊢! Γ.conj ➝ φ

source

def LO.System.conjIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} [ModusPonens 𝓢] [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 ⋯)

source

def LO.System.implyConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} [ModusPonens 𝓢] [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 ⋯)

source

def LO.System.conjImplyConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} [ModusPonens 𝓢] [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 ⋯

source

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

𝓢 ⊢ ⋀Γ ➝ φ

Equations

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

source

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

𝓢 ⊢! ⋀Γ ➝ φ

source

def LO.System.conjIntro' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} [ModusPonens 𝓢] [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 ⋯))

source

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

𝓢 ⊢! ⋀Γ

source

def LO.System.implyConj' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] {𝓢 : S} [ModusPonens 𝓢] [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 ⋯))

source

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

𝓢 ⊢! φ ➝ ⋀Γ

source

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

𝓢 ⊢ ⋀Γ ➝ ⋀Δ

Equations

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

source

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

System.Minimal 𝓣

Equations

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

source

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

System.Classical 𝓣

Equations

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