The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello Daniel, I am not an expert on these things but I think that the
following can help:

Be careful with the word "decidable". In the sentence "classical logic
is when all propositions are decidable", it does not mean
"turing-computable". In this context, "P is decidable" juste means
"P\/~P" is provable.

It happens that in coq WITHOUT AXIOM a proof of "P\/~P" is necessarily
a decision for P. So we say that P is decidable. But In coq + classic
axiom, proving P\/~P does not mean that there is a decision for P.
"classical logic is when all propositions are decidable" is therefore
a confusing use of the word "decidable".

All this under experts expertise of course.

Hope this helps,
Pierre

2012/12/21 Daniel de Rauglaudre 
<daniel.de_rauglaudre AT inria.fr>:
> Hi,
>
> I have a problem about the notion of "decidability" and the notion
> of "classical logic". I had an issue with fellows about that recently.
>
> In Coq, decidability and axiom of classical logic are defined as:
>     Definition decidable := λ P : Prop, P ∨ ¬ P.
>     Axiom classic : ∀ P : Prop, P ∨ ¬ P.
>
> And I thought: "classical logic is when all propositions are decidable".
>
> But my fellows say I am wrong.
>
> Perhaps I am, since, if this thought was true, that would mean that
> classical logic is contradictory since people say that there exists
> propositions which are proved to be undecidable.
>
> So I am confused. Is it possible to prove False using the axiom "classic"
> and a proof of undecidability of some well-know undecidable proposition?
>
> I am interested in explanations, not too theoretical, please, because
> even if I know Coq relatively well, having written 8,000 lines of Coq
> these couple of years, I am often confused about differences between
> meta langage and langage, Prop and Set, Prop and Type, and all that
> sort of things.
>
> Thanks!
>
> --
> Daniel de Rauglaudre
> http://pauillac.inria.fr/~ddr/