Lukasiewicz

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

Imported declaration from the Incompleteness formalization.

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

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

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
• imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
• elimContra (φ ψ : F) : 𝓢 ⊢ Axioms.ElimContra φ ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Lukasiewicz.dne = LO.Entailment.imply₁' LO.Entailment.elimContra⨀₁(LO.Entailment.imply₁' LO.Entailment.elimContra⨀₁LO.Entailment.imply₁)⨀₁LO.Entailment.impId (∼∼φ)

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Lukasiewicz.dni = LO.Entailment.elimContra⨀LO.Entailment.Lukasiewicz.dne

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Lukasiewicz.explode h₁ h₂ = LO.Entailment.elimContra⨀(LO.Entailment.imply₁⨀h₂)⨀h₁

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Lukasiewicz.explodeHyp h₁ h₂ = LO.Entailment.imply₁' LO.Entailment.elimContra⨀₁(LO.Entailment.imply₁' LO.Entailment.imply₁⨀₁h₂)⨀₁h₁

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Lukasiewicz.mdpIn₁ = LO.Entailment.impId (φ ==> ψ)

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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