On explicit definability in arithmetic

Summary

Abstract.We characterize the arithmetic functions in one variable that are explicitly definable from the familiar arithmetic operations. This characterization is deduced from algebraic properties of some non-standard rings of integers. Elementary model theory is also used to show that the greatest common divisor function and related functions are not explicitly definable from the usual arithmetic operations. It turns out that explicit definability is equivalent to computability with bounded complexity, for the recursive algorithms of Y. Moschovakis and with respect to a certain natural cost function.

Introduction.

Motivating Question:Which functions are explicitly definable in the arithmetic Structures

Here iq (“integer quotient”) and rem (“remainder”) describe

integer division with remainder,

that is, iq : and rem : are the functions such that for all we have, with.

We nowspecifywhatwe mean by explicitly definable. Let be an L-structure with distinct marked elements 0,. A function is said to be explicitly definable in M if there are L-terms t₁(x), …, t_n(x) with x = (x₁, …, x_m), such that each set

is definable inMby a quantifier-free L-formula, and these sets together cover M^m. (Throughout this paper, m and n range over

An n-ary relation is said to be explicitly definable in M if its characteristic function is explicitly definable inM.

Remarks on explicit definability.

1. (1) Connection to computation: The recursive programs on M from [7, 8] have the property that explicit definability in M is equivalent to computability by a recursive program on M in a uniformly bounded number of steps, as measured by a certain cost function. A precise statement to this effect can be found in [8].