@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
- LO.Axioms.Imply₁ φ ψ = φ ➝ ψ ➝ φ
@[reducible, inline]
Equations
- LO.Axioms.Imply₁.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.Imply₁ φ ψ = x}
@[reducible, inline]
@[reducible, inline]
Equations
- LO.Axioms.Imply₂.set = {x : F | ∃ (φ : F) (ψ : F) (χ : F), LO.Axioms.Imply₂ φ ψ χ = x}
@[reducible, inline]
@[reducible, inline]
Equations
- LO.Axioms.ElimContra.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.ElimContra φ ψ = x}
@[reducible, inline]
Equations
- LO.Axioms.AndElim₁ φ ψ = φ ⋏ ψ ➝ φ
@[reducible, inline]
Equations
- LO.Axioms.AndElim₁.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.AndElim₁ φ ψ = x}
@[reducible, inline]
Equations
- LO.Axioms.AndElim₂ φ ψ = φ ⋏ ψ ➝ ψ
@[reducible, inline]
Equations
- LO.Axioms.AndElim₂.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.AndElim₂ φ ψ = x}
@[reducible, inline]
Equations
- LO.Axioms.AndInst φ ψ = φ ➝ ψ ➝ φ ⋏ ψ
@[reducible, inline]
Equations
- LO.Axioms.AndInst.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.AndInst φ ψ = x}
@[reducible, inline]
Equations
- LO.Axioms.OrInst₁ φ ψ = φ ➝ φ ⋎ ψ
@[reducible, inline]
Equations
- LO.Axioms.OrInst₁.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.OrInst₁ φ ψ = x}
@[reducible, inline]
Equations
- LO.Axioms.OrInst₂ φ ψ = ψ ➝ φ ⋎ ψ
@[reducible, inline]
Equations
- LO.Axioms.OrInst₂.set = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.OrInst₂ φ ψ = x}
@[reducible, inline]
@[reducible, inline]
Equations
- LO.Axioms.OrElim.set = {x : F | ∃ (φ : F) (ψ : F) (χ : F), LO.Axioms.OrElim φ ψ χ = x}
@[reducible, inline]
@[reducible, inline]
Equations
- LO.Axioms.NegEquiv.set = {x : F | ∃ (φ : F), LO.Axioms.NegEquiv φ = x}
@[reducible, inline]
Equations
- LO.Axioms.EFQ φ = ⊥ ➝ φ
@[reducible, inline]
Equations
- 𝗘𝗙𝗤 = {x : F | ∃ (φ : F), LO.Axioms.EFQ φ = x}
Equations
- LO.Axioms.«term𝗘𝗙𝗤» = Lean.ParserDescr.node `LO.Axioms.«term𝗘𝗙𝗤» 1024 (Lean.ParserDescr.symbol "𝗘𝗙𝗤")
@[reducible, inline]
Equations
- LO.Axioms.LEM φ = φ ⋎ ∼φ
@[reducible, inline]
Equations
- 𝗟𝗘𝗠 = {x : F | ∃ (φ : F), LO.Axioms.LEM φ = x}
Equations
- LO.Axioms.«term𝗟𝗘𝗠» = Lean.ParserDescr.node `LO.Axioms.«term𝗟𝗘𝗠» 1024 (Lean.ParserDescr.symbol "𝗟𝗘𝗠")
@[reducible, inline]
@[reducible, inline]
Equations
- 𝗪𝗟𝗘𝗠 = {x : F | ∃ (φ : F), LO.Axioms.WeakLEM φ = x}
Equations
- LO.Axioms.«term𝗪𝗟𝗘𝗠» = Lean.ParserDescr.node `LO.Axioms.«term𝗪𝗟𝗘𝗠» 1024 (Lean.ParserDescr.symbol "𝗪𝗟𝗘𝗠")
@[reducible, inline]
Equations
- LO.Axioms.Dummett φ ψ = (φ ➝ ψ) ⋎ (ψ ➝ φ)
@[reducible, inline]
Equations
- 𝗗𝘂𝗺 = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.Dummett φ ψ = x}
Equations
- LO.Axioms.«term𝗗𝘂𝗺» = Lean.ParserDescr.node `LO.Axioms.«term𝗗𝘂𝗺» 1024 (Lean.ParserDescr.symbol "𝗗𝘂𝗺")
@[reducible, inline]
Equations
- LO.Axioms.DNE φ = ∼∼φ ➝ φ
@[reducible, inline]
Equations
- 𝗗𝗡𝗘 = {x : F | ∃ (φ : F), LO.Axioms.DNE φ = x}
Equations
- LO.Axioms.«term𝗗𝗡𝗘» = Lean.ParserDescr.node `LO.Axioms.«term𝗗𝗡𝗘» 1024 (Lean.ParserDescr.symbol "𝗗𝗡𝗘")
@[reducible, inline]
Equations
- LO.Axioms.Peirce φ ψ = ((φ ➝ ψ) ➝ φ) ➝ φ
@[reducible, inline]
Equations
- 𝗣𝗲 = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.Peirce φ ψ = x}
Equations
- LO.Axioms.«term𝗣𝗲» = Lean.ParserDescr.node `LO.Axioms.«term𝗣𝗲» 1024 (Lean.ParserDescr.symbol "𝗣𝗲")