On explicit definability in arithmetic
Lou van den Dries · Cambridge University Press eBooks · 2017
. 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 1 ( x ) , …, t n ( x ) with x = ( x 1 , …, x m ), such that each set is definable in M by 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 in M . Remarks on explicit definability. (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].