Documentation

Foundation.Logic.Axioms

@[reducible, inline]
abbrev LO.Axioms.Verum {F : Type u_1} [LogicalConnective F] :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Imply₁ {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Imply₂ {F : Type u_1} [LogicalConnective F] (φ ψ χ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.ElimContra {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.AndElim₁ {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.AndElim₂ {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.AndInst {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.OrInst₁ {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.OrInst₂ {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.OrElim {F : Type u_1} [LogicalConnective F] (φ ψ χ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.NegEquiv {F : Type u_1} [LogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.EFQ {F : Type u_1} [LogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.LEM {F : Type u_1} [LogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.WeakLEM {F : Type u_1} [LogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Dummett {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.DNE {F : Type u_1} [LogicalConnective F] (φ : F) :
F
Equations
@[reducible, inline]
Equations
@[reducible, inline]
abbrev LO.Axioms.Peirce {F : Type u_1} [LogicalConnective F] (φ ψ : F) :
F
Equations
@[reducible, inline]
Equations