Formal proofs

It is possible, though not very pleasant, to produce formal proofs in Peano arithmetic.

Consider, for example, the following proof of the fact that \({ 2 + 2 = 4 }\), which in the language we’re using is written as \({ [ ( 0 '' + 0 '' ) = 0 '''' ] }\).

1. \({ [ ∃ x . ( x = 0 ) ] }\)
2. \({ [ ∃ y . ( y = 0 ) ] }\)
3. \({ \{ ∀ x . [ ∃ y . ( y = x ' ) ] \} }\)
4. \({ \{ [ ∃ x . ( x = 0 ) ] ⊃ [ ∃ y . ( y = 0 ' ) ] \} }\)
5. \({ [ ∃ y . ( y = 0 ' ) ] }\)
6. \({ [ ∃ x . ( x = 0 ' ) ] }\)
7. \({ \{ [ ∃ x . ( x = 0 ' ) ] ⊃ [ ∃ y . ( y = 0 '' ) ] \} }\)
8. \({ [ ∃ y . ( y = 0 '' ) ] }\)
9. \({ [ ∃ x . ( x = 0 '' ) ] }\)
10. \({ \{ ∀ x . [ ( x + 0 ) = x ] \} }\)
11. \({ \{ [ ∃ x . ( x = 0 '' ) ] ⊃ [ ( 0 '' + 0 ) = 0 '' ] \} }\)
12. \({ [ ( 0 '' + 0 ) = 0 '' ] }\)
13. \({ [ ( 0 '' + 0 ) ' = 0 ''' ] }\)
14. \({ ( ∀ x . \{ ∀ y . [ ( x + y ' ) = ( x + y ) ' ] \} ) }\)
15. \({ ( [ ∃ x . ( x = 0 '' ) ] ⊃ \{ ∀ y . [ ( 0 '' + y ' ) = ( 0 '' + y ) ' ] \} ) }\)
16. \({ \{ ∀ y . [ ( 0 '' + y ' ) = ( 0 '' + y ) ' ] \} }\)
17. \({ \{ [ ∃ y . ( y = 0 ) ] ⊃ [ ( 0 '' + 0 ' ) = ( 0 '' + 0 ) ' ] \} }\)
18. \({ [ ( 0 '' + 0 ' ) = ( 0 '' + 0 ) ' ] }\)
19. \({ [ ( 0 '' + 0 ' ) = 0 ''' ] }\)
20. \({ [ ( 0 '' + 0 ' ) ' = 0 '''' ] }\)
21. \({ \{ [ ∃ y . ( y = 0 ' ) ] ⊃ [ ( 0 '' + 0 '' ) = ( 0 '' + 0 ' ) ' ] \} }\)
22. \({ [ ( 0 '' + 0 '' ) = ( 0 '' + 0 ' ) ' ] }\)
23. \({ [ ( 0 '' + 0 '' ) = 0 '''' ] }\)

Here 1 is an axiom, and 2 is the result of substitution on 1. 3 is an axiom, 4 is obtained from 3 by one of our quantifier rules, 5 is modus ponens applied to 1 and 4, and 6 is substitution on 6. 7 is a quantifier rule applied to 3, 8 is modus ponens applied to 6 and 9, and 9 is substitution on 8. 10 is an axiom, 11 is a quantifier rule applied to 10, and 12 is modus ponens on 9 and 11. 13 is derived from 12 by one of our arithmetic rules of inference. 14 is an axiom, 15 is derive from it by a quantifier rule, and 16 is modus ponens on 9 and 15. 17 is a quantifier rule applied to 16 and 18 is modus ponens on 2 and 17. 19 is derived from 13 and 18 by one of our rules of inference for equality. 20 comes from an arithmetic rule of inference on 19. 21 is a quantifier rule applied to 16 and 22 is modus ponens on 5 and 21. Finally, 23 is one of the rules of equality applied to 20 and 22.

Statements more complicated than \({ 2 + 2 = 4 }\) have correspondingly longer proofs. The following is a proof of \[ [ ∀ x . ( ∀ y . \{ ∃ z . [ z = ( x + y ) ] \} ] ) ] , \] i.e. the fact that the sum of any two natural numbers is a natural number.

1. \({ [ ∃ x . ( x = 0 ) ] }\)
2. \({ ( 0 = 0 ) }\)
3. \({ \{ [ ∃ x . ( x = 0 ) ] ∧ ( 0 = 0 ) \} }\)
4. \({ [ ∃ x . ( x = x ) ] }\)
5. \({ [ ∃ y . ( y = y ) ] }\)
6. \({ [ ∃ z . ( z = z ) ] }\)
7. \({ ( z = z ) }\)
8. \({ \{ [ ∃ z . ( z = z ) ] ∧ ( z = z ) \} }\)
9. \({ [ ∃ z . ( z = x ) ] }\)
10. \({ [ ∃ z . ( z = w ) ] }\)
11. \({ [ ∃ x . ( x = w ) ] }\)
12. \({ \{ ∀ x . [ ∃ y . ( y = x ' ) ] \} }\)
13. \({ \{ [ ∃ x . ( x = w ) ] ⊃ [ ∃ y . ( y = w ' ) ] \} }\)
14. \({ [ ∃ y . ( y = w ' ) ] }\)
15. \({ [ ∃ z . ( z = w ' ) ] }\)
16. \({ \{ ∀ x . [ ( x + 0 ) = x ] \} }\)
17. \({ \{ [ ∃ x . ( x = x ) ] ⊃ [ ( x + 0 ) = x ] \} }\)
18. \({ [ ( x + 0 ) = x ] }\)
19. \({ ( ∃ z . \{ [ z = ( x + 0 ) ] \} ) }\)
20. \({ . \quad ( ∃ z . \{ [ z = ( x + y ) ] \} ) }\)
21. \({ . \quad ( [ ∃ z . ( z = w ) ] ∧ \{ [ w = ( x + y ) ] \} ) }\)
22. \({ . \quad [ w = ( x + y ) ] }\)
23. \({ . \quad [ w ' = ( x + y ) ' ] }\)
24. \({ . \quad ( ∀ x . \{ ∀ y . [ ( x + y ' ) = ( x + y ) ' ] \} ) }\)
25. \({ . \quad ( [ ∃ x . ( x = x ) ] ⊃ \{ ∀ y . [ ( x + y ' ) = ( x + y ) ' ] \} ) }\)
26. \({ . \quad \{ ∀ y . [ ( x + y ' ) = ( x + y ) ' ] \} }\)
27. \({ . \quad \{ [ ∃ y . ( y = y ) ] ⊃ [ ( x + y ' ) = ( x + y ) ' ] \} }\)
28. \({ . \quad [ ( x + y ' ) = ( x + y ) ' ] }\)
29. \({ . \quad [ ( x + y ) ' = ( x + y ' ) ] }\)
30. \({ . \quad [ w ' = ( x + y ' ) ] }\)
31. \({ . \quad \{ [ ∃ z . ( z = w ' ) ] ∧ [ w ' = ( x + y ' ) ] \} }\)
32. \({ . \quad \{ ∃ z . [ z = ( x + y ' ) ] \} }\)
33. \({ \{ ∃ z . [ z = ( x + y ) ] \} ⊃ \{ ∃ z . [ z = ( x + y ' ) ] \} ) }\)
34. \({ \{ ∃ z . [ z = ( x + y ) ] \} }\)
35. \({ \{ ¬ [ ∃ y . ( y = y ) ] \} ∨ \{ ∃ z . [ z = ( x + y ) ] \} }\)
36. \({ [ ∃ y . ( y = y ) ] ⊃ \{ ∃ z . [ z = ( x + y ) ] \} }\)
37. \({ ( ∀ y . \{ ∃ z . [ z = ( x + y ) ] \} ) }\)
38. \({ [ \{ ¬ [ ∃ x . ( x = x ) ] \} ∨ ( ∀ y . \{ ∃ z . [ z = ( x + y ) ] \} ] ) }\)
39. \({ \{ [ ∃ x . ( x = x ) ] ⊃ ( ∀ y . \{ ∃ z . [ z = ( x + y ) ] \} ] ) \} }\)
40. \({ [ ∀ x . ( ∀ y . \{ ∃ z . [ z = ( x + y ) ] \} ] ) ] }\)

This one is somewhat more complicated than the previous one. A hypothesis is introduced at 20 and then discharged at 33. This, together with 19, allows us to use induction at 34.

Had we used a logic with existential presuppositions the proof could have been reduced to four lines. That’s largely because such a logic assumes that any expression we can write down refers to something in the domain, so the fact that we have a notation for addition already essentially assumes that the sum of any two natural numbers is a natural number. That’s very convenient, but unfortunately the same would apply to subtraction. If we introduce a notation for subtraction into a system based on such a logic then we can give a four line proof of \[ [ ∀ x . ( ∀ y . \{ ∃ z . [ z = ( x - y ) ] \} ] ) ] , \] but unfortunately this statement is false. The difference of natural numbers need not be a natural number. Formal systems for elementary arithmetic based on first order logic with existential suppositions avoid this problem by not having a notation for subtraction. But then there are important facts about elementary arithmetic which they can’t express. For example, the correct version of the statement above is \[ ( ∀ x . \{ ∀ y . [ ( x ≥ y ) ⊃ \{ ∃ z . [ z = ( x - y ) ] \} ] \} ) , \] which says that \({ x - y }\) is a natural number if \({ x ≥ y }\). This is a theorem in our system but can’t even be stated in a system with existential suppositions.

As we saw earlier, it’s possible to give a fairly concise statement within the language of Peano arithmetic of the fact that there are infinitely primes. It’s possible to give a formal proof as well, but it’s hardly an enjoyable exercise. Logicians, though, are generally much more interesting in figuring out what can or can’t be proved within a formal system than with actually supplying proofs. In other words, they tend to live in the world of semiformal proofs rather than formal proofs.