The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

This is emphatically not true of the natural numbers.

It is true of the “one-point compacification” of the natural numbers (sometimes called co-natural numbers):

CoInductive CN : Type :=
| O : CN
| S : CN -> CN

In fact, for this one-point compacification of the natural number we get a slightly stronger (and, frankly, more useful):

forall P, (forall a:CN, P n \/ ~P n) -> (forall a:CN, P a) \/ exists a:CN, ~P a

Martin Escardó & Paulo Oliva have spend quite some energy studying this latter property.

This [ http://www.cs.bham.ac.uk/~mhe/papers/exhaustive.pdf ], I believe, may be a good, rather programming-oriented, starting point.

​

On 3 July 2016 at 21:56, Jonathan Leivent <jonikelee AT gmail.com> wrote:

I hit another constructive goal that is messing with my classical logic encumbered brain - a form of excluded middle at a point vs. overall:

  A : Type
  P : A -> Prop
  emp : forall a : A, P a \/ ~ P a
  ============================
  (forall a : A, P a) \/ ~ (forall a : A, P a)

I would think this is not provable in Coq in general, but it is certainly true for many A and P.  What properties of A and/or P make this true?  I would think it is true for example on any type A such that one can enumerate the elements somehow - such as nat, or maybe any inductive type.  But, I don't even see how to prove it if A is nat for arbitrary P.  It's trivial to prove if A is bool for arbitrary P, and probably so for any other finite type.

How does one go about such proofs when A is not finite - what other hypotheses about A and/or P are needed to make headway?

-- Jonathan