Vladimir Voevodsky | 19 Jul 16:43 2012

[TYPES] a question

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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.

Vladimir Voevodsky | 19 Jul 16:44 2012

[TYPES] question (cont.)

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Sorry, I forgot to mention that there is also induction. V.

Vladimir Voevodsky | 19 Jul 17:16 2012

Re: [TYPES] question (cont.)

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

> 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.

Vladimir Voevodsky | 20 Jul 23:58 2012

Re: [TYPES] a question

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Many thanks to everybody who provided suggestions on my, not so well formulated, question.

It appears to me now after more thinking and some Wikipedia searches :), that the system which I had in mind is
equivalent to Primitive Recursive Arithmetic and, as I have been told, the provability of sentences in
this system is undecidable. 

Vladimir.

On Jul 19, 2012, at 10:43 AM, Vladimir Voevodsky wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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.
> 
> 

Sergei Soloviev | 21 Jul 00:39 2012
Picon
Picon

Re: [TYPES] question (cont.)

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Vladimir,

do you include equality? 

Best

Sergei Soloviev 

 
On Thursday, July 19, 2012 17:16 CEST, Vladimir Voevodsky <vladimir@...>
wrote: 

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> > 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.
> 
> 


Gmane