The Coq mailing list

[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/