class LO.LukasiewiczAbbrev (F : Type u_1) [LO.LogicalConnective F] : Prop

• top : ⊤ = ∼⊥
• neg : ∀ {φ : F}, ∼φ = φ ➝ ⊥
• or : ∀ {φ ψ : F}, φ ⋎ ψ = ∼φ ➝ ψ
• and : ∀ {φ ψ : F}, φ ⋏ ψ = ∼(φ ➝ ∼ψ)

instance LO.instNegAbbrevOfLukasiewiczAbbrev {F : Type u_1} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] : LO.NegAbbrev F

Equations

• ⋯ = ⋯

class LO.System.Lukasiewicz {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓢 : S) [LO.LukasiewiczAbbrev F] extends LO.System.ModusPonens 𝓢, LO.System.HasAxiomImply₁ 𝓢, LO.System.HasAxiomImply₂ 𝓢, LO.System.HasAxiomElimContra 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• elim_contra : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.ElimContra φ ψ

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

Equations

• LO.System.Lukasiewicz.verum = ⋯.mpr (LO.System.impId ⊥)

instance LO.System.Lukasiewicz.instHasAxiomVerum {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} [LO.System.Lukasiewicz 𝓢] : LO.System.HasAxiomVerum 𝓢

Equations

• LO.System.Lukasiewicz.instHasAxiomVerum = { verum := LO.System.Lukasiewicz.verum }

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

Equations

• LO.System.Lukasiewicz.dne = LO.System.imply₁' LO.System.elim_contra⨀₁(LO.System.imply₁' LO.System.elim_contra⨀₁LO.System.imply₁)⨀₁LO.System.impId (∼∼φ)

instance LO.System.Lukasiewicz.instHasAxiomDNE {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} [LO.System.Lukasiewicz 𝓢] : LO.System.HasAxiomDNE 𝓢

Equations

• LO.System.Lukasiewicz.instHasAxiomDNE = { dne := fun (φ : F) => LO.System.Lukasiewicz.dne }

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

Equations

• LO.System.Lukasiewicz.dni = LO.System.elim_contra⨀LO.System.Lukasiewicz.dne

def LO.System.Lukasiewicz.explode {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.Lukasiewicz 𝓢] (h₁ : 𝓢 ⊢ φ) (h₂ : 𝓢 ⊢ ∼φ) : 𝓢 ⊢ ψ

Equations

• LO.System.Lukasiewicz.explode h₁ h₂ = LO.System.elim_contra⨀(LO.System.imply₁⨀h₂)⨀h₁

def LO.System.Lukasiewicz.explodeHyp {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ χ : F} [LO.System.Lukasiewicz 𝓢] (h₁ : 𝓢 ⊢ φ ➝ ψ) (h₂ : 𝓢 ⊢ φ ➝ ∼ψ) : 𝓢 ⊢ φ ➝ χ

Equations

• LO.System.Lukasiewicz.explodeHyp h₁ h₂ = LO.System.imply₁' LO.System.elim_contra⨀₁(LO.System.imply₁' LO.System.imply₁⨀₁h₂)⨀₁h₁

def LO.System.Lukasiewicz.explodeHyp₂ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ χ s : F} [LO.System.Lukasiewicz 𝓢] (h₁ : 𝓢 ⊢ φ ➝ ψ ➝ χ) (h₂ : 𝓢 ⊢ φ ➝ ψ ➝ ∼χ) : 𝓢 ⊢ φ ➝ ψ ➝ s

Equations

• LO.System.Lukasiewicz.explodeHyp₂ h₁ h₂ = LO.System.imply₁' (LO.System.imply₁' LO.System.elim_contra)⨀₂(LO.System.imply₁' (LO.System.imply₁' LO.System.imply₁)⨀₂h₂)⨀₂h₁

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

Equations

• LO.System.Lukasiewicz.efq = LO.System.Lukasiewicz.explodeHyp (⋯.mpr LO.System.imply₁) (⋯.mpr LO.System.imply₁)

instance LO.System.Lukasiewicz.instHasAxiomEFQ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} [LO.System.Lukasiewicz 𝓢] : LO.System.HasAxiomEFQ 𝓢

Equations

• LO.System.Lukasiewicz.instHasAxiomEFQ = { efq := fun (φ : F) => LO.System.Lukasiewicz.efq }

def LO.System.Lukasiewicz.impSwap {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ χ : F} [LO.System.Lukasiewicz 𝓢] (h : 𝓢 ⊢ φ ➝ ψ ➝ χ) : 𝓢 ⊢ ψ ➝ φ ➝ χ

Equations

• LO.System.Lukasiewicz.impSwap h = LO.System.imply₁' h⨀₂LO.System.imply₁

def LO.System.Lukasiewicz.mdpIn₁ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ (φ ➝ ψ) ➝ φ ➝ ψ

Equations

• LO.System.Lukasiewicz.mdpIn₁ = LO.System.impId (φ ➝ ψ)

def LO.System.Lukasiewicz.mdpIn₂ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ φ ➝ (φ ➝ ψ) ➝ ψ

Equations

• LO.System.Lukasiewicz.mdpIn₂ = LO.System.Lukasiewicz.impSwap LO.System.Lukasiewicz.mdpIn₁

def LO.System.Lukasiewicz.mdp₂In₁ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ χ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ

Equations

• LO.System.Lukasiewicz.mdp₂In₁ = LO.System.imply₂

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

Equations

• LO.System.Lukasiewicz.mdp₂In₂ = LO.System.Lukasiewicz.impSwap LO.System.Lukasiewicz.mdp₂In₁

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

Equations

• LO.System.Lukasiewicz.impTrans'₁ bpq = LO.System.Lukasiewicz.impSwap (LO.System.impTrans'' bpq LO.System.Lukasiewicz.mdpIn₂)

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

Equations

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

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

Equations

• LO.System.Lukasiewicz.impTrans₂ = LO.System.impTrans'' (LO.System.Lukasiewicz.impSwap (LO.System.imply₁' (LO.System.impId (ψ ➝ χ)))) LO.System.Lukasiewicz.mdp₂In₁

def LO.System.Lukasiewicz.impTrans₁ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ χ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ (φ ➝ ψ) ➝ (ψ ➝ χ) ➝ φ ➝ χ

Equations

• LO.System.Lukasiewicz.impTrans₁ = LO.System.Lukasiewicz.impSwap LO.System.Lukasiewicz.impTrans₂

def LO.System.Lukasiewicz.dhypBoth {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ χ : F} [LO.System.Lukasiewicz 𝓢] (h : 𝓢 ⊢ ψ ➝ χ) : 𝓢 ⊢ (φ ➝ ψ) ➝ φ ➝ χ

Equations

• LO.System.Lukasiewicz.dhypBoth h = LO.System.imply₂⨀LO.System.imply₁' h

def LO.System.Lukasiewicz.explode₂₁ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ ∼φ ➝ φ ➝ ψ

Equations

• LO.System.Lukasiewicz.explode₂₁ = ⋯.mpr (LO.System.Lukasiewicz.dhypBoth LO.System.Lukasiewicz.efq)

def LO.System.Lukasiewicz.explode₁₂ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ φ ➝ ∼φ ➝ ψ

Equations

• LO.System.Lukasiewicz.explode₁₂ = LO.System.Lukasiewicz.impSwap LO.System.Lukasiewicz.explode₂₁

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

Equations

• LO.System.Lukasiewicz.contraIntro = ⋯.mpr LO.System.Lukasiewicz.impTrans₁

def LO.System.Lukasiewicz.contraIntro' {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ ∼ψ ➝ ∼φ

Equations

• LO.System.Lukasiewicz.contraIntro' h = LO.System.Lukasiewicz.contraIntro⨀h

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

Equations

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

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

Equations

• LO.System.Lukasiewicz.andElim₂ = ⋯.mpr (let_fun this := LO.System.imply₁; let_fun this := LO.System.Lukasiewicz.contraIntro' this; LO.System.impTrans'' this LO.System.Lukasiewicz.dne)

instance LO.System.Lukasiewicz.instHasAxiomAndElim {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} [LO.System.Lukasiewicz 𝓢] : LO.System.HasAxiomAndElim 𝓢

Equations

• LO.System.Lukasiewicz.instHasAxiomAndElim = { and₁ := fun (φ ψ : F) => LO.System.Lukasiewicz.andElim₁, and₂ := fun (φ ψ : F) => LO.System.Lukasiewicz.andElim₂ }

def LO.System.Lukasiewicz.andImplyLeft {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ₁ φ₂ ψ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ (φ₁ ➝ ψ) ➝ φ₁ ⋏ φ₂ ➝ ψ

Equations

• LO.System.Lukasiewicz.andImplyLeft = LO.System.Lukasiewicz.impSwap (LO.System.imply₁' (LO.System.impId (φ₁ ➝ ψ)))⨀₂LO.System.imply₁' LO.System.Lukasiewicz.andElim₁

def LO.System.Lukasiewicz.andImplyLeft' {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ₁ φ₂ ψ : F} [LO.System.Lukasiewicz 𝓢] (h : 𝓢 ⊢ φ₁ ➝ ψ) : 𝓢 ⊢ φ₁ ⋏ φ₂ ➝ ψ

Equations

• LO.System.Lukasiewicz.andImplyLeft' h = LO.System.Lukasiewicz.andImplyLeft⨀h

def LO.System.Lukasiewicz.andImplyRight {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ₁ φ₂ ψ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ (φ₂ ➝ ψ) ➝ φ₁ ⋏ φ₂ ➝ ψ

Equations

• LO.System.Lukasiewicz.andImplyRight = LO.System.Lukasiewicz.impSwap (LO.System.imply₁' (LO.System.impId (φ₂ ➝ ψ)))⨀₂LO.System.imply₁' LO.System.Lukasiewicz.andElim₂

def LO.System.Lukasiewicz.andImplyRight' {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ₁ φ₂ ψ : F} [LO.System.Lukasiewicz 𝓢] (h : 𝓢 ⊢ φ₂ ➝ ψ) : 𝓢 ⊢ φ₁ ⋏ φ₂ ➝ ψ

Equations

• LO.System.Lukasiewicz.andImplyRight' h = LO.System.Lukasiewicz.andImplyRight⨀h

def LO.System.Lukasiewicz.andInst'' {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.Lukasiewicz 𝓢] (hp : 𝓢 ⊢ φ) (hq : 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⋏ ψ

Equations

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

def LO.System.Lukasiewicz.andInst {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {φ ψ : F} [LO.System.Lukasiewicz 𝓢] : 𝓢 ⊢ φ ➝ ψ ➝ φ ⋏ ψ

Equations

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

instance LO.System.Lukasiewicz.instHasAxiomAndInst {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} [LO.System.Lukasiewicz 𝓢] : LO.System.HasAxiomAndInst 𝓢

Equations

• LO.System.Lukasiewicz.instHasAxiomAndInst = { and₃ := fun (φ ψ : F) => LO.System.Lukasiewicz.andInst }

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

Equations

• LO.System.Lukasiewicz.orInst₁ = ⋯.mpr LO.System.Lukasiewicz.explode₁₂

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

Equations

• LO.System.Lukasiewicz.orInst₂ = ⋯.mpr LO.System.imply₁

instance LO.System.Lukasiewicz.instHasAxiomOrInst {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} [LO.System.Lukasiewicz 𝓢] : LO.System.HasAxiomOrInst 𝓢

Equations

• LO.System.Lukasiewicz.instHasAxiomOrInst = { or₁ := fun (φ ψ : F) => LO.System.Lukasiewicz.orInst₁, or₂ := fun (φ ψ : F) => LO.System.Lukasiewicz.orInst₂ }

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

Equations

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

instance LO.System.Lukasiewicz.instHasAxiomOrElim {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} [LO.System.Lukasiewicz 𝓢] : LO.System.HasAxiomOrElim 𝓢

Equations

• LO.System.Lukasiewicz.instHasAxiomOrElim = { or₃ := fun (φ ψ χ : F) => LO.System.Lukasiewicz.orElim }

instance LO.System.Lukasiewicz.instClassical {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} [LO.System.Lukasiewicz 𝓢] : LO.System.Classical 𝓢

Equations

• LO.System.Lukasiewicz.instClassical = LO.System.Classical.mk