Library Stdlib.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 PeanoNat.
Require Import Zabs.
Require Import Zorder.
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}.