Stronger completeness axiom for real numbers in Coq

Link:: https://stackoverflow.com/q/41326216

Display all goals and responses

Question

Here is the completeness axiom defined in the Coq standard library.

is_upper_bound = 
fun (E : R -> Prop) (m : R) =>
forall x : R, E x -> (x <= m)%R
     : (R -> Prop) -> R -> Prop

Arguments is_upper_bound _%function_scope _%R_scopebound = 
fun E : R -> Prop => exists m : R, is_upper_bound E m
     : (R -> Prop) -> Prop

Arguments bound _%function_scopeis_lub = 
fun (E : R -> Prop) (m : R) =>
is_upper_bound E m /\
(forall b : R, is_upper_bound E b -> (m <= b)%R)
     : (R -> Prop) -> R -> Prop

Arguments is_lub _%function_scope _%R_scopecompleteness
     : forall E : R -> Prop,
       bound E ->
       (exists x : R, E x) -> {m : R | is_lub E m}

Suppose I add in

Open Scope R_scope.

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).

Answer

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 the sig_not_dec lemma (Rlogic module), which states the decidability of negated formulas:

sig_not_dec
     : forall P : Prop, {~ ~ P} + {~ P}

supremum axiom implies LEM

Let'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.

Require Import Coq.Reals.RIneq.

Lemma supremum_implies_lem : forall P : Prop, P \/ ~ P.forall P : Prop, P \/ ~ P
Proof.forall P : Prop, P \/ ~ P
  intros P.P: Prop
P \/ ~ P
  set (E := fun x => x = 0 \/ (x = 1 /\ P)).P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
P \/ ~ P
  destruct (supremum E) as (x & H & Hclas).P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
exists l : R, is_upper_bound E l
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
exists x : R, E x
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
P \/ ~ P
  exists 1.P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
is_upper_bound E 1
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
exists x : R, E x
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
P \/ ~ P intros x [->|[-> _]].P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
0 <= 1
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
1 <= 1
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
exists x : R, E x
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
P \/ ~ P
  apply Rle_0_1.P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
1 <= 1
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
exists x : R, E x
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
P \/ ~ P apply Rle_refl.P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
exists x : R, E x
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
P \/ ~ P exists 0; now left.P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
P \/ ~ P
  destruct (Rle_lt_dec 1 x) as [H'|H'].P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': 1 <= x
P \/ ~ P
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': x < 1
P \/ ~ P
  -P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': 1 <= x
P \/ ~ P left.P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': 1 <= x
P
    pose proof (Rlt_le_trans 0 1 x Rlt_0_1 H') as Hx0.P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': 1 <= x
Hx0: 0 < x
P
    destruct (Hclas 0 Hx0) as (y & [contra | (_ & Hp)] & Hy0).P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': 1 <= x
Hx0: 0 < x
y: R
contra: y = 0
Hy0: y > 0
P
P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': 1 <= x
Hx0: 0 < x
y: R
Hp: P
Hy0: y > 0
P
    +P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': 1 <= x
Hx0: 0 < x
y: R
contra: y = 0
Hy0: y > 0
P now apply Rgt_not_eq in Hy0.
    +P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': 1 <= x
Hx0: 0 < x
y: R
Hp: P
Hy0: y > 0
P exact Hp.
  -P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': x < 1
P \/ ~ P right.P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': x < 1
~ P intros HP.P: Prop
E:= fun x : R => x = 0 \/ x = 1 /\ P: R -> Prop
x: R
H: is_lub E x
Hclas: forall x0 : R,
x0 < x -> exists y : R, E y /\ y > x0
H': x < 1
HP: P
False
    apply (Rlt_not_le _ _ H'), H; now right.
Qed.

LEM implies supremum axiom

Now, 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 of supremum where the exists 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.

Require Import Classical.

Lemma helper (z : R) (E : R -> Prop) :
  (forall y, y > z -> ~ E y) -> is_upper_bound E z.z: R
E: R -> Prop
(forall y : R, y > z -> ~ E y) -> is_upper_bound E z
Proof.z: R
E: R -> Prop
(forall y : R, y > z -> ~ E y) -> is_upper_bound E z
  intros H x Ex.z: R
E: R -> Prop
H: forall y : R, y > z -> ~ E y
x: R
Ex: E x
x <= z
  destruct (Rle_dec x z).z: R
E: R -> Prop
H: forall y : R, y > z -> ~ E y
x: R
Ex: E x
r: x <= z
x <= z
z: R
E: R -> Prop
H: forall y : R, y > z -> ~ E y
x: R
Ex: E x
n: ~ x <= z
x <= z
  -z: R
E: R -> Prop
H: forall y : R, y > z -> ~ E y
x: R
Ex: E x
r: x <= z
x <= z assumption.
  -z: R
E: R -> Prop
H: forall y : R, y > z -> ~ E y
x: R
Ex: E x
n: ~ x <= z
x <= z specialize (H x (Rnot_le_gt x z n)); contradiction.
Qed.

Lemma 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)}.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)}
Proof.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)}
  intros E Hbound Hnonempty.E: R -> Prop
Hbound: exists l : R, is_upper_bound E l
Hnonempty: exists x : R, E x
{m : R
| is_lub E m /\
  (forall x : R, x < m -> exists y : R, E y /\ y > x)}
  pose proof (completeness E Hbound Hnonempty) as [m Hlub].E: R -> Prop
Hbound: exists l : R, is_upper_bound E l
Hnonempty: exists x : R, E x
m: R
Hlub: is_lub E m
{m : R
| is_lub E m /\
  (forall x : R, x < m -> exists y : R, E y /\ y > x)}
  clear Hbound Hnonempty.E: R -> Prop
m: R
Hlub: is_lub E m
{m : R
| is_lub E m /\
  (forall x : R, x < m -> exists y : R, E y /\ y > x)}
  exists m.E: R -> Prop
m: R
Hlub: is_lub E m
is_lub E m /\
(forall x : R, x < m -> exists y : R, E y /\ y > x) split; auto.E: R -> Prop
m: R
Hlub: is_lub E m
forall x : R, x < m -> exists y : R, E y /\ y > x
  intros x Hlt.E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
exists y : R, E y /\ y > x
  assert (~ (forall y, y > x -> ~ E y)) as Hclass.E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
~ (forall y : R, y > x -> ~ E y)
E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
Hclass: ~ (forall y : R, y > x -> ~ E y)
exists y : R, E y /\ y > x
  intro Hcontra; apply helper in Hcontra.E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
Hcontra: is_upper_bound E x
False
E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
Hclass: ~ (forall y : R, y > x -> ~ E y)
exists y : R, E y /\ y > x
  destruct Hlub as [Hup Hle].E: R -> Prop
m: R
Hup: is_upper_bound E m
Hle: forall b : R, is_upper_bound E b -> m <= b
x: R
Hlt: x < m
Hcontra: is_upper_bound E x
False
E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
Hclass: ~ (forall y : R, y > x -> ~ E y)
exists y : R, E y /\ y > x
  specialize (Hle x Hcontra).E: R -> Prop
m: R
Hup: is_upper_bound E m
x: R
Hle: m <= x
Hlt: x < m
Hcontra: is_upper_bound E x
False
E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
Hclass: ~ (forall y : R, y > x -> ~ E y)
exists y : R, E y /\ y > x
  apply Rle_not_lt in Hle; contradiction.E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
Hclass: ~ (forall y : R, y > x -> ~ E y)
exists y : R, E y /\ y > x
  (* classical part starts here *)
  apply not_all_ex_not in Hclass as [y Hclass]; exists y.E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
y: R
Hclass: ~ (y > x -> ~ E y)
E y /\ y > x
  apply imply_to_and in Hclass as [Hyx HnotnotEy].E: R -> Prop
m: R
Hlub: is_lub E m
x: R
Hlt: x < m
y: R
Hyx: y > x
HnotnotEy: ~ ~ E y
E y /\ y > x
  now apply NNPP in HnotnotEy.
Qed.