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