Foundation.Logic.HilbertStyle.Lukasiewicz

source

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

Prop

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

Instances

LO.Modal.Formula.instLukasiewiczAbbrev

source

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

NegAbbrev F

source

class LO.System.Lukasiewicz {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] (𝓢 : S) [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) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
elim_contra (φ ψ : F) : 𝓢 ⊢ Axioms.ElimContra φ ψ

Instances

LO.Modal.Hilbert.Deduction.instLukasiewiczFormula

source

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

𝓢 ⊢ ⊤

Equations

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

source

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

HasAxiomVerum 𝓢

Equations

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

source

def LO.System.Lukasiewicz.dne {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LukasiewiczAbbrev F] [System F S] {𝓢 : S} {φ : F} [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 (∼∼φ)

source

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

HasAxiomDNE 𝓢

Equations

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

source

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

𝓢 ⊢ φ ➝ ∼∼φ

Equations

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

source

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

𝓢 ⊢ ψ

Equations

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

source

def LO.System.Lukasiewicz.explodeHyp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LukasiewiczAbbrev F] [System F S] {𝓢 : S} {φ ψ χ : F} [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₁

source

def LO.System.Lukasiewicz.explodeHyp₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LukasiewiczAbbrev F] [System F S] {𝓢 : S} {φ ψ χ s : F} [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₁

source

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

𝓢 ⊢ ⊥ ➝ φ

Equations

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

source

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

HasAxiomEFQ 𝓢

Equations

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

source

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

𝓢 ⊢ ψ ➝ φ ➝ χ

Equations

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

source

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

𝓢 ⊢ (φ ➝ ψ) ➝ φ ➝ ψ

Equations

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

source

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

𝓢 ⊢ φ ➝ (φ ➝ ψ) ➝ ψ

Equations

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

source

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

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

Equations

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

source

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

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

Equations

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

source

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

𝓢 ⊢ (ψ ➝ χ) ➝ φ ➝ χ

Equations

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

source

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

𝓢 ⊢ (φ ➝ ψ) ➝ φ ➝ χ

Equations

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

source

def LO.System.Lukasiewicz.impTrans₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LukasiewiczAbbrev F] [System F S] {𝓢 : S} {φ ψ χ : F} [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₁

source

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

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

Equations

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

source

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

𝓢 ⊢ (φ ➝ ψ) ➝ φ ➝ χ

Equations

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

source

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

𝓢 ⊢ ∼φ ➝ φ ➝ ψ

Equations

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

source

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

𝓢 ⊢ φ ➝ ∼φ ➝ ψ

Equations

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

source

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

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

Equations

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

source

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

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

Equations

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

source

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

𝓢 ⊢ φ ⋏ ψ ➝ φ

Equations

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

source

def LO.System.Lukasiewicz.andElim₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LukasiewiczAbbrev F] [System F S] {𝓢 : S} {φ ψ : F} [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)

source

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

HasAxiomAndElim 𝓢

Equations

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

source

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

𝓢 ⊢ (φ₁ ➝ ψ) ➝ φ₁ ⋏ φ₂ ➝ ψ

Equations

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

source

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

𝓢 ⊢ φ₁ ⋏ φ₂ ➝ ψ

Equations

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

source

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

𝓢 ⊢ (φ₂ ➝ ψ) ➝ φ₁ ⋏ φ₂ ➝ ψ

Equations

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

source

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

𝓢 ⊢ φ₁ ⋏ φ₂ ➝ ψ

Equations

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

source

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

𝓢 ⊢ φ ⋏ ψ

Equations

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

source

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

𝓢 ⊢ φ ➝ ψ ➝ φ ⋏ ψ

Equations

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

source

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

HasAxiomAndInst 𝓢

Equations

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

source

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

𝓢 ⊢ φ ➝ φ ⋎ ψ

Equations

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

source

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

𝓢 ⊢ ψ ➝ φ ⋎ ψ

Equations

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

source

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

HasAxiomOrInst 𝓢

Equations

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

source

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

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

Equations

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

source

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

HasAxiomOrElim 𝓢

Equations

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

source

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

System.Classical 𝓢

Equations

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