coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] question (cont.), Vladimir Voevodsky, 07/19/2012
- [Coq-Club] Re: question (cont.), Vladimir Voevodsky, 07/19/2012
- Re: [Coq-Club] Re: question (cont.), Cody Roux, 07/19/2012
- Re: [Coq-Club] Re: question (cont.), Arnaud Spiwack, 07/20/2012
- Re: [Coq-Club] Re: question (cont.), Jean Goubault-Larrecq, 07/20/2012
- Re: [Coq-Club] Re: question (cont.), Cody Roux, 07/20/2012
- Re: [Coq-Club] Re: question (cont.), Jean Goubault-Larrecq, 07/20/2012
- Re: [Coq-Club] Re: question (cont.), Jean Goubault-Larrecq, 07/20/2012
- Re: [Coq-Club] Re: question (cont.), Cody Roux, 07/20/2012
- Re: [Coq-Club] Re: question (cont.), Jean Goubault-Larrecq, 07/20/2012
- [Coq-Club] Re: question (cont.), Vladimir Voevodsky, 07/19/2012
Archive powered by MHonArc 2.6.18.