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 Giuseppe Peano, the first person to introduce such a system.
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.
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 '' }\).
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. To main soundness we need to avoid variable capture, which was discussed earlier in the context of substitution in first order logic, when an expression involving variables is substituted for a variable. Otherwise we would be able to deduce the false statement \[ [ ∀ z . ( ∀ y . \{ ∃ z . [ ( z + y ) = z ] \} ) ] \] from the true statement \[ [ ∀ x . ( ∀ y . \{ ∃ z . [ ( x + y ) = z ] \} ) ] . \]
Other than the 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 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 is the existence of \({ 0 }\). The second says that every natural number has a successor. The third axiom says that \({ 0 }\) is not the successor of any natural number. The fourth 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 fifth 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 fourth and fifth 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 sixth 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 sixth and seventh axioms are essentially a recursive definition of multiplication. The sixth axiom tells us how to multiply by 0 and the seventh axiom allows us to get, one step at a time, from multiplication by 0 to multiplication by any natural number. The eighth and ninth axioms define subtraction in terms of addition. The remaining axioms just express the other arithmetic relations in terms of equality.
There are also three arithmetic rules of inference.
The first part of the first rule is actually redundant. It follows from one of our equality rules in first order logic. More generally, if we have \({ ( X = Y ) }\) then we can deduce an equality between any two expressions which differ only in that one has \({ X }\) everywhere the other has \({ Y }\) and vice versa. The interesting part of the first rule is therefore the “and vice versa” part. The third rule is just says that bounded quantifiers are a shorthand notation, as explained when they were first introduced.