Library Coq.Reals.Rlogic


This module proves some logical properties of the axiomatics of Reals

1. Decidablity of arithmetical statements from the axiom that the order of the real numbers is decidable.
2. Derivability of the archimedean "axiom"
1- Proof of the decidablity of arithmetical statements from excluded middle and the axiom that the order of the real numbers is decidable.
Assuming a decidable predicate P n, A series is constructed whose nth term is 1/2^n if P n holds and 0 otherwise. This sum reaches 2 only if P n holds for all n, otherwise the sum is less than 2. Comparing the sum to 2 decides if forall n, P n or ~forall n, P n
One can iterate this lemma and use classical logic to decide any statement in the arithmetical hierarchy.
Contributed by Cezary Kaliszyk and Russell O'Connor

Require Import ConstructiveEpsilon.
Require Import Rfunctions.
Require Import PartSum.
Require Import SeqSeries.
Require Import RiemannInt.
Require Import Fourier.

Section Arithmetical_dec.

Variable P : nat -> Prop.
Hypothesis HP : forall n, {P n} + {~P n}.

Let ge_fun_sums_ge_lemma : (forall (m n : nat) (f : nat -> R), (lt m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).

Let ge_fun_sums_ge : (forall (m n : nat) (f : nat -> R), (le m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).

Let f:=fun n => (if HP n then (1/2)^n else 0)%R.

Lemma cauchy_crit_geometric_dec_fun : Cauchy_crit_series f.

Lemma forall_dec : {forall n, P n} + {~forall n, P n}.

Lemma sig_forall_dec : {n | ~P n}+{forall n, P n}.

End Arithmetical_dec.

2- Derivability of the Archimedean axiom


Theorem not_not_archimedean :
  forall r : R, ~ (forall n : nat, (INR n <= r)%R).