10
$\begingroup$

Do there exist known examples of predicates $P$ (possibly functional) such that

1) $P$ admits a first-order definition in the language ${\Bbb N}(+,\times,0,1)$;

2) $P$ admits no definition that does not involve both $+$ and $\times$;

3) the theory of ${\Bbb N}(+,P,0,1)$ is decidable?

(Or

3') the theory of ${\Bbb N}(\times,P,0,1)$ is decidable?

Or even better, both.)

Last I heard (a long time ago) no one can prove the undecidability of ${\Bbb N}(+,{\rm Prime}(),0,1)$, but Alan Woods showed that standard conjectures imply the definability of multiplication in this language.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
9
$\begingroup$

From a paper by Françoise Point, "On the expansion $(N, +; 2^x)$ of Presburger arithmetic," I learned of a much more general result of Semenov, “Logical theories of one-place functions on the set of natural numbers”, Izv. Akad. Nauk SSSR Ser. Mat., 47:3 (1983), 623–658.

Semenov's result implies that Presburger arithmetic together with the function $f(x) = c^x$ is decidable for any fixed $c \geq 2$. Of course, $f$ is characterized by the fact that $f(0) = 1$ and $f(x) = c \cdot f(x-1)$ for $x > 0$. So $f$ is definable in $(N,+,\times,0,1)$.

Something about the sparseness of powers of $2$, it seems... but I haven't read the details.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Perhaps this is clear to you, but...though I agree that one can define exponentiation from (N,+,x,0,1), simply giving a recursion won't do...or one could define multiplication from addition in a similar way. One must give a two place predicate involving only the symbols (+,x,0,1) and logical apparatus satisfied precisely by pairs (x,c^x). The name "f" can't come into it. So one needs coding tricks to capture sequences in order to do recursion. $\endgroup$
    – David Feldman
    Commented Aug 4, 2012 at 18:30
  • 1
    $\begingroup$ You're right - it was misleading for me to describe the recursive definition, when it requires a more complicated formula to define $(x,c^x)$. I didn't follow the golden rule: look for every instance of "Of course" -- that's where the mistakes are. $\endgroup$
    – Marty
    Commented Aug 4, 2012 at 22:03
  • $\begingroup$ @DavidFeldman Because the combination of $+$ and $\times$ can define sequence-coding functions, a recursion like Marty's can be routinely converted into an explicit definition. In the case at hand, $c^x=y$ iff there is a (code for a) sequence $s$ of length $x+1$ such that $s_0=1$, for all $z<n$, $s_{z+1}=c\cdot s_z$, and $s_n=y$. (As far as I know, this method for turning recursions into explicit definitions is due to Dedekind.) $\endgroup$
    – Andreas Blass
    Commented Nov 12 at 19:36
  • $\begingroup$ Of course, there is a much simpler definition of "is some power of $2$" which, I guess, must also be decidable in this setting. $\endgroup$
    – cody
    Commented Nov 12 at 20:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .