All Questions

The factorial function is primitive recursive, and therefore definable by a $\Sigma_1$ formula. Is it also definable by a $\Delta_0$ formula (i.e. bounded quantifiers)? If not, why?

I recently became interested in some problems concerning decidability of extensions of Presburger arithmetic. However, being a number-theorist rather than a logician, I am confused by some notational ...

Can theories stronger than $\sf PA$ manage to define functions from the naturals to the naturals, that $\sf PA$ cannot? If so, what are examples of those functions?

Motivation: Many "weak" arithmetic functions and/or relations ("relations" for short) are equivalent with relations explicitly definable by relations which were recursively defined by them beforehand (...