2

With Coq's axioms of real numbers completeness and total_order_T, using the same technique as in the standard lib lemma Un_cv_crit_lub, I managed to prove

Lemma NatForallDec : forall (f : nat -> bool),
    { forall n:nat, f n = false } + { ~forall n:nat, f n = false }.

and

Lemma NatForallDecIncr : forall (f : nat -> bool),
    (forall n m:nat, f n = true -> n <= m -> f m = true)
    -> { forall n:nat, f n = false } + { exists n:nat, f n = true }.

That is disturbing because it looks like some sort of oracle : if a proposition f about the natural numbers is decidable for each number, then the infinite conjunction of f becomes decidable too. So the axioms of the real numbers say that we can extract an algorithm which makes an infinite number of decisions in finite time...

Are there other examples of excluded middle that follow from the axioms of real numbers, and that have little to do with real numbers ?

And concerning real numbers, can a least upper bound be realized as a convergent sequence ?

Definition Cv_lub (A : R -> Prop) (l : R) (n : nat) :
  is_lub A l
  -> { x : R | A x /\ (l - x <= 1 / INR n)%R }.
V. Semeria
  • 3,128
  • 1
  • 10
  • 25
  • 1
    Here is a related [question](https://stackoverflow.com/q/41326216/2747511) you might find useful. – Anton Trunov Jan 10 '19 at 13:36
  • 1
    @AntonTrunov Yes indeed, that's the answer I was looking for. I didn't imagine the axioms of the real numbers were so tightly coupled with classical logic. Isn't there a way to do real numbers in a constructive setting ? – V. Semeria Jan 10 '19 at 15:45
  • Sure! One of the most famous treatments is "Foundations of Constructive Analysis" by Errett Bishop. His definitions are different. – Anton Trunov Jan 10 '19 at 19:03
  • 1
    @AntonTrunov Ah the same Bishop :) I asked this question about the reals because I am currently implementing his constructive measure theory here : https://github.com/coq/coq/pull/9185 – V. Semeria Jan 10 '19 at 21:45
  • Oh yeah, I saw your PR :) I guess it would be more consistent to start with Bishop's definitions of the basics things. Nevertheless, I think what you do is very valuable for the Coq community. – Anton Trunov Jan 11 '19 at 14:29

0 Answers0