The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 12/21/2012 06:47 AM, Daniel de Rauglaudre wrote:
> 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.
>    

Probably the issue is that the above Coq terminology is applied in the 
context of constructive logic, where we identify proof and computation, 
by definition.  When proofs are computations, then an instance of the 
law of the excluded middle really is a decision procedure.  However, in 
mainstream math, there is no inherent connection between proof and 
computation, so there is no reason to connect excluded middle with 
decidability.