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 : {p q : F} → 𝓢 ⊢ p ➝ q → 𝓢 ⊢ p → 𝓢 ⊢ q

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 ∼p is equivalent to p ➝ ⊥ on system.

This is weaker asssumption than "introducing ∼p as an abbreviation of p ➝ ⊥" (NegAbbrev).

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

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

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₁ : (p q : F) → 𝓢 ⊢ LO.Axioms.Imply₁ p q

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₂ : (p q r : F) → 𝓢 ⊢ LO.Axioms.Imply₂ p q r

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 : (p q : F) → 𝓢 ⊢ LO.Axioms.ElimContra p q

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₁ : (p q : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ p q

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₂ : (p q : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ p q

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₃ : (p q : F) → 𝓢 ⊢ LO.Axioms.AndInst p q

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₁ : (p q : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ p q

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₂ : (p q : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ p q

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₃ : (p q r : F) → 𝓢 ⊢ LO.Axioms.OrElim p q r

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 : (p : F) → 𝓢 ⊢ LO.Axioms.EFQ p

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 : (p : F) → 𝓢 ⊢ LO.Axioms.LEM p

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 : (p : F) → 𝓢 ⊢ LO.Axioms.DNE p

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 : (p : F) → 𝓢 ⊢ LO.Axioms.WeakLEM p

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 : (p q : F) → 𝓢 ⊢ LO.Axioms.GD p q

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 : (p q : F) → 𝓢 ⊢ LO.Axioms.Peirce p q

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

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)

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)

def LO.System.mdp {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.ModusPonens 𝓢] {p : F} {q : F} : 𝓢 ⊢ p ➝ q → 𝓢 ⊢ p → 𝓢 ⊢ q

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} {p : F} {q : F} [LO.System.ModusPonens 𝓢] : 𝓢 ⊢! p ➝ q → 𝓢 ⊢! p → 𝓢 ⊢! q

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.cast {S : Type u_1} {F : Type u_2} [LO.System F S] {𝓢 : S} {p : F} {q : F} (e : p = q) (b : 𝓢 ⊢ p) : 𝓢 ⊢ q

Equations

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

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 𝓢] : 𝓢 ⊢! ⊤

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

Equations

• LO.System.imply₁ = LO.System.HasAxiomImply₁.imply₁ p q

@[simp]

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

def LO.System.imply₂ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} : 𝓢 ⊢ (p ➝ q ➝ r) ➝ (p ➝ q) ➝ p ➝ r

Equations

• LO.System.imply₂ = LO.System.HasAxiomImply₂.imply₂ p q r

@[simp]

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

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

Equations

• LO.System.and₁ = LO.System.HasAxiomAndElim₁.and₁ p q

@[simp]

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

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

Equations

• LO.System.and₂ = LO.System.HasAxiomAndElim₂.and₂ p q

@[simp]

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

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

Equations

• LO.System.and₃ = LO.System.HasAxiomAndInst.and₃ p q

@[simp]

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

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

Equations

• LO.System.or₁ = LO.System.HasAxiomOrInst₁.or₁ p q

@[simp]

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

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

Equations

• LO.System.or₂ = LO.System.HasAxiomOrInst₂.or₂ p q

@[simp]

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

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

Equations

• LO.System.or₃ = LO.System.HasAxiomOrElim.or₃ p q r

@[simp]

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

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

Equations

• LO.System.efq = LO.System.HasAxiomEFQ.efq p

@[simp]

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

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

Equations

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

@[simp]

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

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

Equations

• LO.System.lem = LO.System.HasAxiomLEM.lem p

@[simp]

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

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

Equations

• LO.System.dne = LO.System.HasAxiomDNE.dne p

@[simp]

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

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

Equations

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

@[simp]

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

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

Equations

• LO.System.wlem = LO.System.HasAxiomWeakLEM.wlem p

@[simp]

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

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

Equations

• LO.System.dummett = LO.System.HasAxiomDummett.dummett p q

@[simp]

theorem LO.System.dummett! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} {p : F} {q : F} [LO.System.HasAxiomDummett 𝓢] : 𝓢 ⊢! LO.Axioms.GD p q

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

Equations

• LO.System.peirce = LO.System.HasAxiomPeirce.peirce p q

@[simp]

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

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

Equations

• LO.System.elim_contra = LO.System.HasAxiomElimContra.elim_contra p q

@[simp]

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

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.HasAxiomImply₁ 𝓢] {p : F} {q : F} (h : 𝓢 ⊢ p) : 𝓢 ⊢ q ➝ p

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] {p : F} {q : F} (d : 𝓢 ⊢! p) : 𝓢 ⊢! q ➝ p

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

Equations

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

theorem LO.System.dhyp! {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] {p : F} {q : F} (b : 𝓢 ⊢! p) : 𝓢 ⊢! q ➝ p

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.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} (d₁ : 𝓢 ⊢ p ➝ q ➝ r) (d₂ : 𝓢 ⊢ p ➝ q) (d₃ : 𝓢 ⊢ p) : 𝓢 ⊢ r

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} (d₁ : 𝓢 ⊢! p ➝ q ➝ r) (d₂ : 𝓢 ⊢! p ➝ q) (d₃ : 𝓢 ⊢! p) : 𝓢 ⊢! r

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

Equations

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

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

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

Alias of LO.System.and₁'.

Equations

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

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

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] {p : F} {q : F} (d : 𝓢 ⊢ p ⋏ q) : 𝓢 ⊢ q

Equations

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

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

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

Alias of LO.System.and₂'.

Equations

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

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

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} (d₁ : 𝓢 ⊢ p) (d₂ : 𝓢 ⊢ q) : 𝓢 ⊢ p ⋏ q

Equations

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

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

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

Alias of LO.System.and₃'.

Equations

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

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

Alias of LO.System.and₃'!.

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

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} (h₁ : 𝓢 ⊢! p ➝ q) (h₂ : 𝓢 ⊢! q ➝ p) : 𝓢 ⊢! p ⭤ q

Equations

• ⋯ = ⋯

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

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

theorem LO.System.provable_iff_of_iff {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓢 : S} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] {p : F} {q : F} (h : 𝓢 ⊢! p ⭤ q) : 𝓢 ⊢! p ↔ 𝓢 ⊢! q

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

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomOrInst₁ 𝓢] {p : F} {q : F} (d : 𝓢 ⊢! p) : 𝓢 ⊢! p ⋎ q

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

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomOrInst₂ 𝓢] {q : F} {p : F} (d : 𝓢 ⊢! q) : 𝓢 ⊢! p ⋎ q

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

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomOrElim 𝓢] {p : F} {r : F} {q : F} (d₁ : 𝓢 ⊢! p ➝ r) (d₂ : 𝓢 ⊢! q ➝ r) : 𝓢 ⊢! p ⋎ q ➝ r

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

Equations

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

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

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

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

Equations

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

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

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

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₂ 𝓢] (p : F) : 𝓢 ⊢ p ➝ p

Equations

• LO.System.impId p = 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} : 𝓢 ⊢! p ➝ p

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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] (p : F) : 𝓢 ⊢ p ⭤ p

Equations

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

@[simp]

def LO.System.iff_id! {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.HasAxiomAndInst 𝓢] {p : F} : 𝓢 ⊢! p ⭤ p

Equations

• ⋯ = ⋯

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

Equations

• LO.System.neg_equiv = LO.System.NegationEquiv.neg_equiv p

@[simp]

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

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

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢ p ➝ ⊥ → 𝓢 ⊢ ∼p

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] {p : F} [LO.System.NegationEquiv 𝓢] : 𝓢 ⊢! ∼p ↔ 𝓢 ⊢! p ➝ ⊥

instance LO.System.instNegationEquivOfNegAbbrev {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.HasAxiomAndInst 𝓢] [LO.NegAbbrev F] : LO.System.NegationEquiv 𝓢

Equations

• LO.System.instNegationEquivOfNegAbbrev = { neg_equiv := fun (p : F) => ⋯.mpr (LO.System.iffId (p ➝ ⊥)) }

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

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} (hqr : 𝓢 ⊢! p ➝ q ➝ r) (hq : 𝓢 ⊢! p ➝ q) : 𝓢 ⊢! p ➝ r

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} {s : F} (bqr : 𝓢 ⊢ p ➝ q ➝ r ➝ s) (bq : 𝓢 ⊢ p ➝ q ➝ r) : 𝓢 ⊢ p ➝ q ➝ s

Equations

• bqr⨀₂bq = LO.System.dhyp p 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} {s : F} (hqr : 𝓢 ⊢! p ➝ q ➝ r ➝ s) (hq : 𝓢 ⊢! p ➝ q ➝ r) : 𝓢 ⊢! p ➝ q ➝ 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} {s : F} {t : F} (bqr : 𝓢 ⊢ p ➝ q ➝ r ➝ s ➝ t) (bq : 𝓢 ⊢ p ➝ q ➝ r ➝ s) : 𝓢 ⊢ p ➝ q ➝ r ➝ t

Equations

• bqr⨀₃bq = LO.System.dhyp p (LO.System.dhyp q 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} {s : F} {t : F} (hqr : 𝓢 ⊢! p ➝ q ➝ r ➝ s ➝ t) (hq : 𝓢 ⊢! p ➝ q ➝ r ➝ s) : 𝓢 ⊢! p ➝ q ➝ r ➝ 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} {s : F} {t : F} {u : F} (bqr : 𝓢 ⊢ p ➝ q ➝ r ➝ s ➝ t ➝ u) (bq : 𝓢 ⊢ p ➝ q ➝ r ➝ s ➝ t) : 𝓢 ⊢ p ➝ q ➝ r ➝ s ➝ u

Equations

• bqr⨀₄bq = LO.System.dhyp p (LO.System.dhyp q (LO.System.dhyp r 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} {s : F} {t : F} {u : F} (hqr : 𝓢 ⊢! p ➝ q ➝ r ➝ s ➝ t ➝ u) (hq : 𝓢 ⊢! p ➝ q ➝ r ➝ s ➝ t) : 𝓢 ⊢! p ➝ q ➝ r ➝ 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] {p : F} {q : F} {r : F} (bpq : 𝓢 ⊢ p ➝ q) (bqr : 𝓢 ⊢ q ➝ r) : 𝓢 ⊢ p ➝ r

Equations

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

theorem LO.System.imp_trans''! {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₂ 𝓢] {p : F} {q : F} {r : F} (hpq : 𝓢 ⊢! p ➝ q) (hqr : 𝓢 ⊢! q ➝ r) : 𝓢 ⊢! p ➝ r

theorem LO.System.unprovable_imp_trans''! {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₂ 𝓢] {p : F} {q : F} {r : F} (hpq : 𝓢 ⊢! p ➝ q) : 𝓢 ⊬ p ➝ r → 𝓢 ⊬ q ➝ r

def LO.System.iffTrans'' {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.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} {r : F} (h₁ : 𝓢 ⊢ p ⭤ q) (h₂ : 𝓢 ⊢ q ⭤ r) : 𝓢 ⊢ p ⭤ r

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} {r : F} (h₁ : 𝓢 ⊢! p ⭤ q) (h₂ : 𝓢 ⊢! q ⭤ r) : 𝓢 ⊢! p ⭤ r

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

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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] (p : F) (q : F) (r : F) : 𝓢 ⊢ p ➝ q ➝ r ➝ p

Equations

• LO.System.imply₁₁ p q r = 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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] (p : F) (q : F) (r : F) : 𝓢 ⊢! p ➝ q ➝ r ➝ p

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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [DecidableEq F] {Γ : List F} {p : F} (h : p ∈ Γ) : 𝓢 ⊢ Γ.conj ➝ p

Equations

• LO.System.generalConj h_2 = ⋯.elim
• LO.System.generalConj h_2 = if e : p = q 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [DecidableEq F] {Γ : List F} {p : F} (h : p ∈ Γ) : 𝓢 ⊢! Γ.conj ➝ p

def LO.System.implyAnd {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.HasAxiomAndInst 𝓢] {p : F} {q : F} {r : F} (bq : 𝓢 ⊢ p ➝ q) (br : 𝓢 ⊢ p ➝ r) : 𝓢 ⊢ p ➝ q ⋏ r

Equations

• LO.System.implyAnd bq br = LO.System.dhyp p LO.System.and₃⨀₁bq⨀₁br

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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] (p : F) (q : F) : 𝓢 ⊢ p ⋏ q ➝ q ⋏ p

Equations

• LO.System.andComm p q = 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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} : 𝓢 ⊢! p ⋏ q ➝ q ⋏ p

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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} (h : 𝓢 ⊢ p ⋏ q) : 𝓢 ⊢ q ⋏ p

Equations

• LO.System.andComm' h = LO.System.andComm p q⨀h

theorem LO.System.and_comm'! {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.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} (h : 𝓢 ⊢! p ⋏ q) : 𝓢 ⊢! q ⋏ p

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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] (p : F) (q : F) : 𝓢 ⊢ p ⭤ q ➝ q ⭤ p

Equations

• LO.System.iffComm p q = LO.System.andComm (p ➝ q) (q ➝ p)

theorem LO.System.iff_comm! {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.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} : 𝓢 ⊢! p ⭤ q ➝ q ⭤ p

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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} (h : 𝓢 ⊢ p ⭤ q) : 𝓢 ⊢ q ⭤ p

Equations

• LO.System.iffComm' h = LO.System.iffComm p q⨀h

theorem LO.System.iff_comm'! {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.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} (h : 𝓢 ⊢! p ⭤ q) : 𝓢 ⊢! q ⭤ p

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.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] (p : F) (q : F) (r : F) : 𝓢 ⊢ (p ⋏ q ➝ r) ⭤ (p ➝ q ➝ r)

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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} {r : F} : 𝓢 ⊢! (p ⋏ q ➝ r) ⭤ (p ➝ q ➝ r)

def LO.System.andImplyIffImplyImply'.mp {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.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} {r : F} (d : 𝓢 ⊢ p ⋏ q ➝ r) : 𝓢 ⊢ p ➝ q ➝ r

Equations

• LO.System.andImplyIffImplyImply'.mp d = LO.System.and₁' (LO.System.andImplyIffImplyImply p q r)⨀d

def LO.System.andImplyIffImplyImply'.mpr {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.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} {r : F} (d : 𝓢 ⊢ p ➝ q ➝ r) : 𝓢 ⊢ p ⋏ q ➝ r

Equations

• LO.System.andImplyIffImplyImply'.mpr d = LO.System.and₂' (LO.System.andImplyIffImplyImply p q r)⨀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} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} {r : F} : 𝓢 ⊢! p ⋏ q ➝ r ↔ 𝓢 ⊢! p ➝ q ➝ r

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.HasAxiomVerum 𝓢] [LO.System.HasAxiomAndInst 𝓢] [DecidableEq F] (Γ : List F) (b : (p : F) → p ∈ Γ → 𝓢 ⊢ p) : 𝓢 ⊢ Γ.conj

Equations

• LO.System.conjIntro [] b_2 = LO.System.verum
• LO.System.conjIntro (q :: Γ_2) b_2 = LO.System.andIntro (b_2 q ⋯) (LO.System.conjIntro Γ_2 fun (q_1 : F) (hq : q_1 ∈ Γ_2) => b_2 q_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.HasAxiomVerum 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] [DecidableEq F] (p : F) (Γ : List F) (b : (q : F) → q ∈ Γ → 𝓢 ⊢ p ➝ q) : 𝓢 ⊢ p ➝ Γ.conj

Equations

• LO.System.implyConj p [] b_2 = LO.System.dhyp p LO.System.verum
• LO.System.implyConj p (q :: Γ_2) b_2 = LO.System.implyAnd (b_2 q ⋯) (LO.System.implyConj p Γ_2 fun (q_1 : F) (hq : q_1 ∈ Γ_2) => b_2 q_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.HasAxiomVerum 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] [DecidableEq F] {Γ : List F} {Δ : List F} (h : Δ ⊆ Γ) : 𝓢 ⊢ Γ.conj ➝ Δ.conj

Equations

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

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.generalConj' {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.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [DecidableEq F] {Γ : List F} {p : F} (h : p ∈ Γ) : 𝓢 ⊢ ⋀Γ ➝ p

Equations

• LO.System.generalConj' h_2 = ⋯.elim
• LO.System.generalConj' h_2 = ⋯.mpr (LO.System.impId q)
• LO.System.generalConj' h_2 = ⋯.mpr (if e : p = q then ⋯.mpr LO.System.and₁ else let_fun this := ⋯; LO.System.impTrans'' LO.System.and₂ (LO.System.generalConj' this))

theorem LO.System.generate_conj'! {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.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [DecidableEq F] {Γ : List F} {p : F} (h : p ∈ Γ) : 𝓢 ⊢! ⋀Γ ➝ p

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.HasAxiomVerum 𝓢] [LO.System.HasAxiomAndInst 𝓢] [DecidableEq F] (Γ : List F) (b : (p : F) → p ∈ Γ → 𝓢 ⊢ p) : 𝓢 ⊢ ⋀Γ

Equations

• LO.System.conjIntro' [] b_2 = LO.System.verum
• LO.System.conjIntro' [q] b_2 = b_2 (⋀[q]) ⋯
• LO.System.conjIntro' (q :: r :: Γ_2) b_2 = ⋯.mpr (LO.System.andIntro (b_2 q ⋯) (LO.System.conjIntro' (r :: Γ_2) fun (p : F) (a : p ∈ r :: Γ_2) => b_2 p ⋯))

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.HasAxiomVerum 𝓢] [LO.System.HasAxiomAndInst 𝓢] [DecidableEq F] {Γ : List F} (b : ∀ p ∈ Γ, 𝓢 ⊢! p) : 𝓢 ⊢! ⋀Γ

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.HasAxiomVerum 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] [DecidableEq F] (p : F) (Γ : List F) (b : (q : F) → q ∈ Γ → 𝓢 ⊢ p ➝ q) : 𝓢 ⊢ p ➝ ⋀Γ

Equations

• LO.System.implyConj' p [] b_2 = LO.System.dhyp p LO.System.verum
• LO.System.implyConj' p [q] b_2 = b_2 (⋀[q]) ⋯
• LO.System.implyConj' p (q :: r :: Γ_2) b_2 = ⋯.mpr (LO.System.implyAnd (b_2 q ⋯) (LO.System.implyConj' p (r :: Γ_2) fun (q_1 : F) (hq : q_1 ∈ r :: Γ_2) => b_2 q_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.HasAxiomVerum 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] [DecidableEq F] (p : F) (Γ : List F) (b : ∀ q ∈ Γ, 𝓢 ⊢! p ➝ q) : 𝓢 ⊢! p ➝ ⋀Γ

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.HasAxiomVerum 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] [DecidableEq F] {Γ : List 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) (φ : G →ˡᶜ F) (e : (p : G) → 𝓢 ⊢ φ p ≃ 𝓣 ⊢ p) : LO.System.Minimal 𝓣

Equations

• LO.System.Minimal.ofEquiv 𝓢 𝓣 φ 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) (φ : G →ˡᶜ F) (e : (p : G) → 𝓢 ⊢ φ p ≃ 𝓣 ⊢ p) : LO.System.Classical 𝓣

Equations

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