The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Dear Vladimir,

A gizmo logicians use to spek of this sort of things is the arithmetical hierarchy (see for instance: http://en.wikipedia.org/wiki/Arithmetical_hierarchy#The_arithmetical_hierarchy_of_formulas ).

A formula with just universal quantifiers followed by a non-quantified formula is said to be Π₁. So here is a possible reformulation: is the Π₁ fragment of arithmetic decidable? (the answer is, unfortunately, that it isn't, as Cody explained)


Arnaud

On 19 July 2012 17:16, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

> Don't you have False (as 0=1 for instance) hence not A (as
> A ->False) hence exA (as forall notA -> False), hence everything?

Thanks to everybody who pointed this out to me. I'll have to think whether my question has a more sensible reformulation.

Vladimir.