The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 21 Dec 2012 12:47:46 +0100,
Daniel de Rauglaudre 
<daniel.de_rauglaudre AT inria.fr>
 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.

For me decidability for a constant proposition tends to be meaningless.

From a classical point of view, any proposition is decidable.

What makes the notion of decidability is with parameterized proposition.

For instance, when we say that membershipness (not sure of the word) is
decidable for a language "L:X->Prop", what we mean is not:

forall x, (L x)\/(~L x)

but

exists (f : X->bool), forall x, if (f x) then L x else ~L x

That is linked to the axiom of choice.

"(forall x, exists y, R x y) -> (exists f, forall x, R x (f x))"
(commutation of quantifiers)

* forall x, (L x)\/(~L x)
is equivalent to
* forall x, exists b, if b then (L x) else (~L x)
with axiom of choice, you get
* exists f, forall x, if (f x) then (L x) else (~L x)

> 
> 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.

That is mainly a problem of definitions.

I remember some of my teachers who jokingly announced that existence of
god is decidable (in the sense there exists a Turing Machine which stops
returns 0 if god exists and 1 if god does not). Its proof was build the
constant Turing Machines returning 0, it stops, so it is a candidate.
Do the same thing returning 1. Ok, now you have two Turing Machines,
and you can proudly say, that one of the two decides existence of god.
You do not say which one, but classically one of the two does. So
existence of god is decidable.

The reasonning is right (beside the fact that "god exists" is not
something well defined). So any proposition is decidable.

The interesting stuff is when there is some parameter.
For instance the halting problem.

Any one here acknowledge that the halting problem is undecidable.
You cannot build a Turing Machine which reads the code of another
Turing Machines, stops and returns 1 if and only if this machine will
halt on any possible input.

But now, if you consider the halting problem for a single machine M, the
problem halting is decidable, and even trivial (the solution is to do
like what we did with god existence).

> 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?

No you can't, at least with the definition of decidability with Turing
Machines (which extends to lambda calculus).

> 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!
>