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!

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

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

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

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

```
21 Jul 00:39 2012

### Re: [TYPES] question (cont.)

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

do you include equality?

Best

Sergei Soloviev

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