Library Coq.Reals.Rlogic


This module proves some logical properties of the axiomatic of Reals.
  • Decidability of arithmetical statements.
  • Derivability of the Archimedean "axiom".
  • Decidability of negated formulas.

Require Import RIneq.

Decidability of arithmetical statements

One can iterate this lemma and use classical logic to decide any statement in the arithmetical hierarchy.

Section Arithmetical_dec.

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

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

End Arithmetical_dec.

Derivability of the Archimedean axiom

This is a standard proof (it has been taken from PlanetMath). It is formulated negatively so as to avoid the need for classical logic. Using a proof of {n | ~P n}+{forall n, P n}, we can in principle also derive up and its specification. The proof above cannot be used for that purpose, since it relies on the archimed axiom.

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

Decidability of negated formulas


Lemma sig_not_dec : forall P : Prop, {not (not P)} + {not P}.