coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] a question

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: types-list AT lists.seas.upenn.edu, Coq Club <coq-club AT inria.fr>
Cc: Vladimir Voevodsky <vladimir AT ias.edu>
Subject: [Coq-Club] a question
Date: Thu, 19 Jul 2012 10:43:10 -0400
Envelope-to: types-list AT lists.seas.upenn.edu, coq-club AT inria.fr, vladimir AT ias.edu

Hello,

does any one know if the system of natural arithmetic with equality,
addition, multiplication, exponentiation (or without exponentiation),
"forall" quantifier, implication and conjunction is decidable? There is no
existential quantifier and no negation.

Thanks!
Vladimir.

[Coq-Club] a question, Vladimir Voevodsky, 07/19/2012
- [Coq-Club] Re: [TYPES] a question, Brian Huffman, 07/19/2012
- [Coq-Club] Re: [TYPES] a question, Vladimir Voevodsky, 07/20/2012