As mentioned earlier, a formal system consists of a language, a set of axioms, and a set of rules of inference. We have a language for arithmetic but we don’t yet have axioms or rules of inference. There are a variety of possible choices which tend to known collectively as Peano arithmetic, after the first person to introduce such a system. The particular version used below is essentially that of Hofstadter.
There are two types axioms and rules of inference, logical axioms and rules of inference and arithmetic axioms and rules of inference.
For the logical part we’ll just borrow from the system we’ve already developed. The only change is that in place of parameters we now have numerical expressions and instead of predicates we now have Boolean expressions. In other words, in place of a first order logic statement like \[ \{ [ ∃ x . ( f x ) ] ⊃ [ ¬ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) ] \} \] we have statements like \[ \{ [ ∃ x . ( ∃ y . \{ x = y + y \} ) ] ⊃ [ ¬ ( ∀ x . \{ ¬ [ ( ∃ y . \{ x = y + y \} ) ∨ ( ∃ y . \{ x = y' \} ) ] \} ) ] \} . \] We’ve replaced the generic predicates \({ ( f x ) }\) and \({ ( g x ) }\) with the specific expressions \({ ( ∃ y . \{ x = y + y \} ) }\) and \({ ( ∃ y . \{ x = y' \} ) }\). The first is the translation into our language of the statement that \({ x }\) is even and the second is the translation of the statement that \({ x }\) is positive. We could have replaced them with any other Boolean expressions. Indeed that’s the point of logic: to determine which statements are universally true simply because of their form, without reference to the meaning of their components.
The rules of inference which deal with quantifiers involve introducing eliminating parameters. As stated above, numerical expressions take the role of parameters. Those expressions could be variables or could be more complicated expressions.
For example, one of our arithmetic axioms will be \[ [ ∀ x . \{ ∀ y . [ ( x + y )' = ( x + y ' ) ] \} ] \] One of our rules for quantifiers in first order logic allowed us to take a universal quantifier followed by a variable and an expression, remove the quantifier and variable, and replace all free occurrences of the variable in the expression with a parameter. We can do the same in arithmetic, except now we need to replace the variable with a numerical expression, like \({ 0 '' }\). So from the axiom above we can deduce \[ \{ ∀ y . [ ( 0 '' + y )' = ( 0 '' + y ' ) ] \} . \] The terminology may be unfamiliar but the underlying idea should not be: since we have a statement which is true for all natural numbers \({ x }\) it is true in particular for 2, a.k.a. \({ 0 '' }\).
Other than the two changes described above, for parameters and predicates, the logical structure is just that of first order logic. What’s new is the arithmetic axioms and rules of inference.
We’ll use the following five axioms for arithmetic:
Before reading further you might find it useful to translate each of these into words and convince yourself that it’s true.
The first axiom says that there’s no natural number which, when incremented, gives 0, i.e. that 0 is not the successor of any natural number. The second says that 0 is an identity element for addition, or at least is a right identity element. The fact that it’s a left identity element as well will be a theorem rather than an axiom The third axiom tells us that incrementing a sum is the same as incrementing one of the summands, specifically the second summand. The fact that incrementing the first summand would also work is again a theorem rather than an axiom. The second and third axioms together are best thought of as a recursive definition of addition. If we know how to add 0 to a number and know how to add the successor of any number to a number then we know how to add any number to it. The fourth axiom tells us that 0 multiplied by anything is still 0. Again, there’s a counterpart with the multiplicands in the other order which will be a theorem rather than an axiom. The fourth and fifth axioms are essentially a recursive definition of multiplication. The fourth axiom tells us how to multiply by 0 and the fifth axiom allows us to get, one step at a time, from multiplication by 0 to multiplication by any natural number.
There are also some arithmetic rules of inference.
The first two rules of inference say that equality is reflexive and transitive. The third is a special case of a general principle that if two quantities are equal then the results of applying the same operation to both are also equal. The particular special case is that where the operation in question is incrementing. The converse of the general principle is not true in general. It’s not true, for example, that if two numbers give the same product when multiplied by 0 then they are equal. The converse does hold for incrementing though: if two numbers have the same successor then they are equal.