@[reducible, inline]

abbrev LO.Axioms.Verum {F : Type u_1} [LO.LogicalConnective F] : F

Equations

• LO.Axioms.Verum = ⊤

@[reducible, inline]

abbrev LO.Axioms.Verum.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.Verum.set = {LO.Axioms.Verum}

@[reducible, inline]

abbrev LO.Axioms.Imply₁ {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.Imply₁ φ ψ = φ ➝ ψ ➝ φ

@[reducible, inline]

abbrev LO.Axioms.Imply₁.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.Imply₁.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.Imply₁ φ ψ = x}

@[reducible, inline]

abbrev LO.Axioms.Imply₂ {F : Type u_1} [LO.LogicalConnective F] (φ ψ χ : F) : F

Equations

• LO.Axioms.Imply₂ φ ψ χ = (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ

@[reducible, inline]

abbrev LO.Axioms.Imply₂.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.Imply₂.set = {x : F | ∃ (φ : F) (ψ : F) (χ : F), LO.Axioms.Imply₂ φ ψ χ = x}

@[reducible, inline]

abbrev LO.Axioms.ElimContra {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.ElimContra φ ψ = (∼ψ ➝ ∼φ) ➝ φ ➝ ψ

@[reducible, inline]

abbrev LO.Axioms.ElimContra.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.ElimContra.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.ElimContra φ ψ = x}

@[reducible, inline]

abbrev LO.Axioms.AndElim₁ {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.AndElim₁ φ ψ = φ ⋏ ψ ➝ φ

@[reducible, inline]

abbrev LO.Axioms.AndElim₁.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.AndElim₁.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.AndElim₁ φ ψ = x}

@[reducible, inline]

abbrev LO.Axioms.AndElim₂ {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.AndElim₂ φ ψ = φ ⋏ ψ ➝ ψ

@[reducible, inline]

abbrev LO.Axioms.AndElim₂.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.AndElim₂.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.AndElim₂ φ ψ = x}

@[reducible, inline]

abbrev LO.Axioms.AndInst {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.AndInst φ ψ = φ ➝ ψ ➝ φ ⋏ ψ

@[reducible, inline]

abbrev LO.Axioms.AndInst.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.AndInst.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.AndInst φ ψ = x}

@[reducible, inline]

abbrev LO.Axioms.OrInst₁ {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.OrInst₁ φ ψ = φ ➝ φ ⋎ ψ

@[reducible, inline]

abbrev LO.Axioms.OrInst₁.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.OrInst₁.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.OrInst₁ φ ψ = x}

@[reducible, inline]

abbrev LO.Axioms.OrInst₂ {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.OrInst₂ φ ψ = ψ ➝ φ ⋎ ψ

@[reducible, inline]

abbrev LO.Axioms.OrInst₂.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.OrInst₂.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.OrInst₂ φ ψ = x}

@[reducible, inline]

abbrev LO.Axioms.OrElim {F : Type u_1} [LO.LogicalConnective F] (φ ψ χ : F) : F

Equations

• LO.Axioms.OrElim φ ψ χ = (φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ

@[reducible, inline]

abbrev LO.Axioms.OrElim.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.OrElim.set = {x : F | ∃ (φ : F) (ψ : F) (χ : F), LO.Axioms.OrElim φ ψ χ = x}

@[reducible, inline]

abbrev LO.Axioms.NegEquiv {F : Type u_1} [LO.LogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.NegEquiv φ = ∼φ ⭤ (φ ➝ ⊥)

@[reducible, inline]

abbrev LO.Axioms.NegEquiv.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.NegEquiv.set = {x : F | ∃ (φ : F), LO.Axioms.NegEquiv φ = x}

@[reducible, inline]

abbrev LO.Axioms.EFQ {F : Type u_1} [LO.LogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.EFQ φ = ⊥ ➝ φ

@[reducible, inline]

abbrev LO.Axioms.EFQ.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗘𝗙𝗤 = {x : F | ∃ (φ : F), LO.Axioms.EFQ φ = x}

def LO.Axioms.«term𝗘𝗙𝗤» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗘𝗙𝗤» = Lean.ParserDescr.node `LO.Axioms.«term𝗘𝗙𝗤» 1024 (Lean.ParserDescr.symbol "𝗘𝗙𝗤")

@[reducible, inline]

abbrev LO.Axioms.LEM {F : Type u_1} [LO.LogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.LEM φ = φ ⋎ ∼φ

@[reducible, inline]

abbrev LO.Axioms.LEM.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗟𝗘𝗠 = {x : F | ∃ (φ : F), LO.Axioms.LEM φ = x}

def LO.Axioms.«term𝗟𝗘𝗠» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗟𝗘𝗠» = Lean.ParserDescr.node `LO.Axioms.«term𝗟𝗘𝗠» 1024 (Lean.ParserDescr.symbol "𝗟𝗘𝗠")

@[reducible, inline]

abbrev LO.Axioms.WeakLEM {F : Type u_1} [LO.LogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.WeakLEM φ = ∼φ ⋎ ∼∼φ

@[reducible, inline]

abbrev LO.Axioms.WeakLEM.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗪𝗟𝗘𝗠 = {x : F | ∃ (φ : F), LO.Axioms.WeakLEM φ = x}

def LO.Axioms.«term𝗪𝗟𝗘𝗠» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗪𝗟𝗘𝗠» = Lean.ParserDescr.node `LO.Axioms.«term𝗪𝗟𝗘𝗠» 1024 (Lean.ParserDescr.symbol "𝗪𝗟𝗘𝗠")

@[reducible, inline]

abbrev LO.Axioms.Dummett {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.Dummett φ ψ = (φ ➝ ψ) ⋎ (ψ ➝ φ)

@[reducible, inline]

abbrev LO.Axioms.Dummett.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗗𝘂𝗺 = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.Dummett φ ψ = x}

def LO.Axioms.«term𝗗𝘂𝗺» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗗𝘂𝗺» = Lean.ParserDescr.node `LO.Axioms.«term𝗗𝘂𝗺» 1024 (Lean.ParserDescr.symbol "𝗗𝘂𝗺")

@[reducible, inline]

abbrev LO.Axioms.DNE {F : Type u_1} [LO.LogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.DNE φ = ∼∼φ ➝ φ

@[reducible, inline]

abbrev LO.Axioms.DNE.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗗𝗡𝗘 = {x : F | ∃ (φ : F), LO.Axioms.DNE φ = x}

def LO.Axioms.«term𝗗𝗡𝗘» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗗𝗡𝗘» = Lean.ParserDescr.node `LO.Axioms.«term𝗗𝗡𝗘» 1024 (Lean.ParserDescr.symbol "𝗗𝗡𝗘")

@[reducible, inline]

abbrev LO.Axioms.Peirce {F : Type u_1} [LO.LogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.Peirce φ ψ = ((φ ➝ ψ) ➝ φ) ➝ φ

@[reducible, inline]

abbrev LO.Axioms.Peirce.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗣𝗲 = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.Peirce φ ψ = x}

def LO.Axioms.«term𝗣𝗲» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗣𝗲» = Lean.ParserDescr.node `LO.Axioms.«term𝗣𝗲» 1024 (Lean.ParserDescr.symbol "𝗣𝗲")