Here is the completeness axiom defined in the Coq standard library.
Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.
Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m.
Definition is_lub (E:R -> Prop) (m:R) :=
is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).
Axiom completeness :
forall E:R -> Prop,
bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.
Suppose I add in
Axiom supremum :forall E:R -> Prop,
(exists l : R,is_upper_bound E l) ->
(exists x : R, E x) ->
{ m:R | is_lub E m /\ (forall x:R, x<m -> exists y:R,(E y /\ y >x))}.
Is this required? (i.e does it follow from the others) Would there be any issues with consistency? Also, why is this not the definition in the standard library (I guess this part is subjective).
Your
supremum
axiom is equivalent to the law of excluded middle, in other words by introducing this axiom you are bringing classical logic to the table.The
completeness
axiom already implies a weak form of the law of excluded middle, as shown by the means of thesig_not_dec
lemma (Rlogic
module), which states the decidability of negated formulas:supremum
axiom implies LEMLet's use the standard proof of the
sig_not_dec
lemma to show that with the stronger completeness axiom (supremum
) we can derive the strong form of the law of excluded middle.LEM implies
supremum
axiomNow, let us show that the strong version of LEM implies the
supremum
axiom. We do this by showing that in constructive setting we can derive a negated form ofsupremum
where theexists y:R, E y /\ y > x
part gets replaced with~ (forall y, y > x -> ~ E y)
, and then using the usual classical facts we show that the original statement holds as well.