Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: question (cont.)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: question (cont.)


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Vladimir Voevodsky <vladimir AT ias.edu>
  • Cc: types-list AT lists.seas.upenn.edu, Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Re: question (cont.)
  • Date: Fri, 20 Jul 2012 08:00:03 +0200

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.






Archive powered by MHonArc 2.6.18.

Top of Page