There is something a bit unsatisfying about the arguments which showed that the powers of two and the Fibonacci numbers are arithmetic. For one thing, we seem to be putting more arithmetic into our language than we are getting out of it. Both sequences are very easy to define but in order to show that their elements are an arithmetic set we needed to borrow some facts from number theory which are considerably deeper than we’d need for the definitions. The other problem is that it’s not clear how to generalise those arguments to other simple sequences, even very closely related ones. We could, for example, use the argument above with only very minor changes to show that the powers of 3 or of 5 are arithmetic sets. In fact, for any prime \({ p }\) the expression \[ [ ∀ x . ( \{ ∃ y . [ ( x · y ) = z ] \} ⊃ [ ( x = 0 ' ) ∨ \{ ∃ y . [ x = ( p · y ) ] \} ] ) ] \] says that \({ z }\) is a power of \({ p }\).
For powers of 4 we can use the fact that a number is a power of 4 if and only if it is the square of a power of 2. What about powers of 6, though? While it’s true that every power of 6 is the product of a power of 2 and a power of 3 it’s not true that every such product is a power of 6.
It would be nice to have a general principle saying that given an initial value and an arithmetic relation which uniquely determines the next element of the sequence from the current one the set of all elements of the sequence is arithmetic. This would give us a more satisfactory proof that the powers of 2 are an arithmetic set, and indeed that any geometric progression is arithmetic. With a bit more work it could also give us a more satisfactory proof that the set of Fibonacci numbers is arithmetic. This turns out to be too much to ask for, but there is a weaker principle which is true and suffices for most applications.
Consider the set of bounded expressions. Every such expression is a Boolean expression. We defined sets and relations to be arithmetic if they were defined by Boolean expressions. We can similarly describe sets or relations to be constructively arithmetic if they are defined by bounded expressions. Then every constructively arithmetic set or relation is arithmetic. Is the converse true? It might seem obvious that it’s not, since there are Boolean expressions which are not bounded. That’s not a valid argument though, since the same set or relation might be defined by more than one expression, and some might be bounded while others might not be. For example, our primality criterion \[ [ ∀ x . ( ∀ y . \{ [ ( x · y ) = z ] ⊃ [ ( x = z ) ∨ ( y = z ) ] \} ) ] \] had two ordinary, unbounded, quantifiers, but there are other expressions which identify whether \({ z }\) is prime which use only bounded quantifiers. \({ z }\) is prime if and only if it is greater than 1 and cannot be written as the product of two numbers less than \({ z }\). In other words, \[ \{ ( z > 0 ' ) ∧ [ ∀ x < z : ( ∀ y < z : \{ ¬ [ ( x · y ) = z ] \} ) ] \} . \] Now all the quantifiers are bounded, so the set of primes is not just arithmetic but also constructively arithmetic. It’s useful to know that primality is a constructively arithmetic property, so I’ll now replace our earlier primality test with this one: \[ P ( z ) ≡ \{ ( z > 0 ' ) ∧ [ ∀ x < z : ( ∀ y < z : \{ ¬ [ ( x · y ) = z ] \} ) ] \} . \] Even though the argument suggested above for the existence of sets which are arithmetic but not constructively arithmetic turned out to be invalid its conclusion is nonetheless true. There are sets which are arithmetic but not constructively arithmetic.
Now that we have the notion of constructively arithmetic sets and relations we can state our substitute principle. Given an initial value and a constructive arithmetic relation which uniquely determines the next element of the sequence from the current one the set of all elements of the sequence is arithmetic. I won’t prove this though.