The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

Le 21/12/12 12:47, Daniel de Rauglaudre a écrit :
> 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".

Daniel,

others already have pinpointed the problem: "decidable"
means different things in different (but connected, alas)
contexts.

The meaning of "decidable" is as you describe above in
intuitionistic logic circles.  Decidability applies to
formulae.  And indeed, "classical logic is when all
propositions are decidable", in this sense.

In all other areas of computer science, "decidable" applies
to languages, not formulae.  A language L \subseteq \Sigma^*
is decidable iff there is a terminating Turing machine
that, on input x, will eventually accept iff x is in L
(and reject otherwise).

There are connections between the two notions.  One
of the most famous is that if you can prove
\forall x : N^k. \exists y : N. P(x,y) in
intuitionistic (first-order) Peano arithmetic,
then there is a terminating program (=Turing machine)
that, on input x, will return an y such that P(x,y).
  In fact, the program can be obtained from
an intuitionistic proof by just looking at the
proof as a lambda-term, erasing all non-computational
information (in Coq, do extraction, i.e., keep only the
Set-kinded things, and remove the Prop-kinded ones),
and translating the lambda-term to a Turing machine
doing the same computation (up to standard encodings
of integers).

Best,

-- Jean.