The Coq mailing list

[roconnor AT theorem.ca]

It is well-known that one cannot prove the infinite pigeon hole principle 
constructively, but consider the following:

Definition classicOr A B := ~(~A/\~B).

Section Pigeon.

Variable P : nat -> Prop.
Variable Q : nat -> Prop.
Hypothesis P1 : forall n m, n <= m -> P m -> P n.
Hypothesis Q1 : forall n m, n <= m -> Q m -> Q n.
Hypothesis PQ : forall n, {P n}+{Q n}.

Theorem InfinitePigeonHole : classicOr (forall n, P n) (forall n, Q n).

Is it possible to constructively prove the above theorem?  I haven't been 
able to figure out a proof.  Also, because the conclusion of the above 
theorem is False, I cannot see how to create a Browerian counter-example 
either.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''