The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Sep 18, 2014 at 5:05 AM, Alan Schmitt
<alan.schmitt AT polytechnique.org>
 wrote:
> Hello Daniel,
>
> My courses on logic are very far, so I have a question about one of your
> axioms.
>
> On 2014-09-15 17:55, Daniel de Rauglaudre 
> <daniel.de_rauglaudre AT inria.fr>
>  writes:
>
>> 5/ ∀ P : nat → Prop, { ∃ n, P n } + { ∀ n, ¬P n }.
>
> Isn't it too strong? If I take "P k" to be "function F terminate when
> given input k", doesn't this mean you can decide termination?

I don't think it's inconsistent.  For one thing, it can be deduced
from the normal law of excluded middle plus
constructive_definite_description.  For another, all the ways I can
think of to formalize the contradiction would require feeding a
function to itself, which should hopefully be impossible in Coq's
strongly typed system or else you could create the classic infinite
loop (fun x => x x) (fun x => x x).  Ex:

Parameter classic_dec : forall P:Prop, {P} + {~P}.
Fixpoint contradiction (n:nat) : bool :=
if classic_dec (exists n:nat, contradiction n = true) then
  false
else
  true.

is rejected due to not being well-founded.

If you try building up from the bottom, then for example, all the
contradiction says is that classic_dec on termination of Turing
machines is not computable within Turing machines; classic_dec on
termination of (Turing machines with oracle of termination of a Turing
machine) is not computable with any Turing machine and the oracle of
termination of a Turing machine; etc.

Of course, I could be wrong, but given these heuristic arguments, I'd
have to see a proof of inconsistency within Coq in order to believe
it's inconsistent.
-- 
Daniel Schepler