headers
Vladimir Voevodsky | 19 Jul 2012 16:43
Favicon

[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.
Permalink | Reply | 0 comments |
headers
Vladimir Voevodsky | 19 Jul 2012 16:44
Favicon

[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.
Permalink | Reply | 0 comments |
headers
Vladimir Voevodsky | 19 Jul 2012 17:16
Favicon

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.
Permalink | Reply | 0 comments |
headers
Vladimir Voevodsky | 20 Jul 2012 23:58
Favicon

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.
> 
>
Permalink | Reply | 0 comments |
headers
Sergei Soloviev | 21 Jul 2012 00:39
Picon
Picon
Favicon

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.
> 
>
Permalink | Reply | 0 comments |

Gmane