Axioms

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.Verum = ⊤

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.NegEquiv φ = ∼φ <=> (φ ==> ⊥)

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.EFQ φ = ⊥ ==> φ

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termEFQAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termEFQAx = Lean.ParserDescr.node `LO.Axioms.termEFQAx 1024 (Lean.ParserDescr.symbol "EFQAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termLEMAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termLEMAx = Lean.ParserDescr.node `LO.Axioms.termLEMAx 1024 (Lean.ParserDescr.symbol "LEMAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termWLEMAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termWLEMAx = Lean.ParserDescr.node `LO.Axioms.termWLEMAx 1024 (Lean.ParserDescr.symbol "WLEMAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termDummettAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termDummettAx = Lean.ParserDescr.node `LO.Axioms.termDummettAx 1024 (Lean.ParserDescr.symbol "DummettAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termDNEAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termDNEAx = Lean.ParserDescr.node `LO.Axioms.termDNEAx 1024 (Lean.ParserDescr.symbol "DNEAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termPeirceAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termPeirceAx = Lean.ParserDescr.node `LO.Axioms.termPeirceAx 1024 (Lean.ParserDescr.symbol "PeirceAx")