Take the usual theory of First Order Peano Arithmetic with the signature $(0, s, +, \times)$. Now consider these two questions:
- Take the set of PA theorems which don't involve '$\times$'. Is there a nice axiomatisation of this set with axioms in the signature $(0, s, +)$?
- Take the set of PA theorems which don't involve '$+$'. Is there a nice axiomatisation of this set with axioms in the signature $(0, s, \times)$?
The answer to the first question is familiar -- think Presburger arithmetic. We just need to delete the axioms involving multiplication from PA to get what we want.
But what's the answer to the second question? The PA theorems which don't involve `$+$' are effectively enumerable so are axiomatisable. But elegantly? Removing axioms involving addition from PA won't leave us with enough axioms for multiplication.
Note the question isn't about Skolem arithmetic in the usual sense of the set of first-order truths in the signature $(1, \times)$. Nor is about the set of first-order truths in the signature $(0, s, \times)$. The question, to repeat, is about axiomatising in $(0, s, \times)$ the set of theorems of PA which only involve that non-logical vocabulary. Is there a known nice way of doing this?
[I'm not sure how interesting the question is -- but it was put to me, and I realised I didn't know the answer. Also I had a senior moment in a previous shot at asking the intended question -- so thanks to comments from @Arthur and @Peter for gently pointing that out!]
