Foundation.Logic.HilbertStyle.Lukasiewicz

source

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

Type

top : ⊤ = ∼⊥
neg : ∀ {p : F}, ∼p = p ➝ ⊥
or : ∀ {p q : F}, p ⋎ q = ∼p ➝ q
and : ∀ {p q : F}, p ⋏ q = ∼(p ➝ ∼q)

Instances

source

theorem LO.LukasiewiczAbbrev.top {F : Type u_1} [LO.LogicalConnective F] [self : LO.LukasiewiczAbbrev F] :

⊤ = ∼⊥

source

theorem LO.LukasiewiczAbbrev.neg {F : Type u_1} [LO.LogicalConnective F] [self : LO.LukasiewiczAbbrev F] {p : F} :

∼p = p ➝ ⊥

source

theorem LO.LukasiewiczAbbrev.or {F : Type u_1} [LO.LogicalConnective F] [self : LO.LukasiewiczAbbrev F] {p : F} {q : F} :

p ⋎ q = ∼p ➝ q

source

theorem LO.LukasiewiczAbbrev.and {F : Type u_1} [LO.LogicalConnective F] [self : LO.LukasiewiczAbbrev F] {p : F} {q : F} :

p ⋏ q = ∼(p ➝ ∼q)

source

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

LO.NegAbbrev F

Equations

LO.instNegAbbrevOfLukasiewiczAbbrev = { neg := ⋯ }

source

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)

Instances

source

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

Instances For

source

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 }

source

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

𝓢 ⊢ ∼∼p ➝ p

Equations

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

Instances For

source

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 (p : F) => LO.System.Lukasiewicz.dne }

source

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

𝓢 ⊢ p ➝ ∼∼p

Equations

LO.System.Lukasiewicz.dni = let_fun d₁ := LO.System.elim_contra; let_fun d₂ := LO.System.Lukasiewicz.dne; d₁⨀d₂

Instances For

source

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

𝓢 ⊢ q

Equations

LO.System.Lukasiewicz.explode h₁ h₂ = let_fun d₁ := LO.System.imply₁; let_fun this := d₁⨀h₂; LO.System.elim_contra⨀this⨀h₁

Instances For

source

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

𝓢 ⊢ p ➝ r

Equations

LO.System.Lukasiewicz.explodeHyp h₁ h₂ = let_fun this := LO.System.dhyp p LO.System.imply₁; let_fun this := this⨀₁h₂; let_fun this := LO.System.dhyp p LO.System.elim_contra⨀₁this; this⨀₁h₁

Instances For

source

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

𝓢 ⊢ p ➝ q ➝ s

Equations

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

Instances For

source

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

𝓢 ⊢ ⊥ ➝ p

Equations

LO.System.Lukasiewicz.efq = let_fun this := LO.System.Lukasiewicz.explodeHyp; this (⋯.mpr LO.System.imply₁) (⋯.mpr LO.System.imply₁)

Instances For

source

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 (p : F) => LO.System.Lukasiewicz.efq }

source

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

𝓢 ⊢ q ➝ p ➝ r

Equations

LO.System.Lukasiewicz.impSwap h = LO.System.dhyp q h⨀₂LO.System.imply₁

Instances For

source

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

𝓢 ⊢ (p ➝ q) ➝ p ➝ q

Equations

LO.System.Lukasiewicz.mdpIn₁ = LO.System.impId (p ➝ q)

Instances For

source

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

𝓢 ⊢ p ➝ (p ➝ q) ➝ q

Equations

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

Instances For

source

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} {p : F} {q : F} {r : F} [LO.System.Lukasiewicz 𝓢] :

𝓢 ⊢ (p ➝ q ➝ r) ➝ (p ➝ q) ➝ p ➝ r

Equations

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

Instances For

source

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} {p : F} {q : F} {r : F} [LO.System.Lukasiewicz 𝓢] :

𝓢 ⊢ (p ➝ q) ➝ (p ➝ q ➝ r) ➝ p ➝ r

Equations

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

Instances For

source

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

𝓢 ⊢ (q ➝ r) ➝ p ➝ r

Equations

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

Instances For

source

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

𝓢 ⊢ (p ➝ q) ➝ p ➝ r

Equations

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

Instances For

source

def LO.System.Lukasiewicz.impTrans₂ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {p : F} {q : F} {r : F} [LO.System.Lukasiewicz 𝓢] :

𝓢 ⊢ (q ➝ r) ➝ (p ➝ q) ➝ p ➝ r

Equations

LO.System.Lukasiewicz.impTrans₂ = LO.System.impTrans'' (LO.System.Lukasiewicz.impSwap (LO.System.dhyp p (LO.System.impId (q ➝ r)))) LO.System.Lukasiewicz.mdp₂In₁

Instances For

source

def LO.System.Lukasiewicz.impTrans₁ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {p : F} {q : F} {r : F} [LO.System.Lukasiewicz 𝓢] :

𝓢 ⊢ (p ➝ q) ➝ (q ➝ r) ➝ p ➝ r

Equations

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

Instances For

source

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

𝓢 ⊢ (p ➝ q) ➝ p ➝ r

Equations

LO.System.Lukasiewicz.dhypBoth h = LO.System.imply₂⨀LO.System.dhyp p h

Instances For

source

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

𝓢 ⊢ ∼p ➝ p ➝ q

Equations

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

Instances For

source

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

𝓢 ⊢ p ➝ ∼p ➝ q

Equations

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

Instances For

source

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

𝓢 ⊢ (p ➝ q) ➝ ∼q ➝ ∼p

Equations

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

Instances For

source

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

𝓢 ⊢ p ➝ q → 𝓢 ⊢ ∼q ➝ ∼p

Equations

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

Instances For

source

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

𝓢 ⊢ p ⋏ q ➝ p

Equations

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

Instances For

source

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 (p q : F) => LO.System.Lukasiewicz.andElim₁ }

source

def LO.System.Lukasiewicz.andElim₂ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {p : F} {q : F} [LO.System.Lukasiewicz 𝓢] :

𝓢 ⊢ p ⋏ q ➝ q

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)

Instances For

source

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 (p q : F) => LO.System.Lukasiewicz.andElim₂ }

source

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

𝓢 ⊢ (p₁ ➝ q) ➝ p₁ ⋏ p₂ ➝ q

Equations

LO.System.Lukasiewicz.andImplyLeft = LO.System.Lukasiewicz.impSwap (LO.System.dhyp (p₁ ⋏ p₂) (LO.System.impId (p₁ ➝ q)))⨀₂LO.System.dhyp (p₁ ➝ q) LO.System.Lukasiewicz.andElim₁

Instances For

source

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

𝓢 ⊢ p₁ ⋏ p₂ ➝ q

Equations

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

Instances For

source

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

𝓢 ⊢ (p₂ ➝ q) ➝ p₁ ⋏ p₂ ➝ q

Equations

LO.System.Lukasiewicz.andImplyRight = LO.System.Lukasiewicz.impSwap (LO.System.dhyp (p₁ ⋏ p₂) (LO.System.impId (p₂ ➝ q)))⨀₂LO.System.dhyp (p₂ ➝ q) LO.System.Lukasiewicz.andElim₂

Instances For

source

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

𝓢 ⊢ p₁ ⋏ p₂ ➝ q

Equations

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

Instances For

source

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

𝓢 ⊢ p ⋏ q

Equations

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

Instances For

source

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

𝓢 ⊢ p ➝ q ➝ p ⋏ q

Equations

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

Instances For

source

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 (p q : F) => LO.System.Lukasiewicz.andInst }

source

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

𝓢 ⊢ p ➝ p ⋎ q

Equations

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

Instances For

source

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 (p q : F) => LO.System.Lukasiewicz.orInst₁ }

source

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

𝓢 ⊢ q ➝ p ⋎ q

Equations

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

Instances For

source

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 (p q : F) => LO.System.Lukasiewicz.orInst₂ }

source

def LO.System.Lukasiewicz.orElim {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.LukasiewiczAbbrev F] [LO.System F S] {𝓢 : S} {p : F} {q : F} {r : F} [LO.System.Lukasiewicz 𝓢] :

𝓢 ⊢ (p ➝ r) ➝ (q ➝ r) ➝ p ⋎ q ➝ r

Equations

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

Instances For

source

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 (p q r : F) => LO.System.Lukasiewicz.orElim }

source

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