Formal proofs of Arithmetic
| Some related reading |
|---|
| This is not the simplest way of approaching Gödel's theorems - it goes into a lot of detail of quantification theory before getting on to its application to arithmetics. But in chapter 3 it does actually use the axioms of arithmetic to derive a number of proofs, and for that reason alone it's worth taking a look at. |
My review of Introduction to mathematical logic |
| If you are using Internet Explorer then you may have problems with some of the symbols used on this page. The best way to deal with this seems to be to install the MS Mincho font on your computer. For more information see Displaying Special Characters |
The idea of formal proofs is that they are essentially just manipulating symbols - they don't depend upon the meaning of those symbols. To specify a formal proof system, first it is necessary to describe the language that will be used, that is the symbols and how they are put together to make valid formulae. Then you need to specify what constitutes a proof - that is a list of axioms and rules of deduction. The following proof system for integer arithmetic is based on that given in Introduction to mathematical logic by Elliott Mendelson. The expression T' denotes the successor of T i.e. T+1 (1 is not a basic symbol in this system - it could be defined as 0')
First the language:
| Constant | 0 |
|---|---|
| Variable | x,y,z, x1, x2..., y1..., z1... |
| Term | Constant (i.e. 0), V,T1+T2,T1*T2,T' |
| Formula | T1=T2,¬WF,WF1⇒WF2,∀V WF |
Here V represents a variable, T,T1,T2 represent terms and WF,WF1 and WF2 represent formulae (WF stands for well-formed formula). Note that these items, which are in capital letters here, may be considered metavariables - they don't occur in actual formulae or proofs, which just contain the symbols 0,',+,*,=,¬,⇒ ∀, and the letters x, y, z, (possibly indexed by a number) representing variables. This point can be confusing when reading books on mathematical logic as they are primarily concerned with metaproofs (i.e. proofs about proofs), and tend not to contain much in the way of bare proofs.
Now comes the list of axioms and rules of deduction. Here WF(V) stands for a formula which involves the variable V, and then WF(T) stands for the formula obtained by replacing these occurrences of V with the term T.
| Ax1(WF1,WF2) | WF1⇒(WF2⇒WF1) | First are the three propositional axioms |
| Ax2(WF1,WF2,WF3) | (WF1⇒(WF2⇒WF3))⇒((WF1⇒WF2)⇒(WF1⇒WF3)) | |
| Ax3(WF1,WF2) | (¬WF2⇒¬WF1)⇒((¬WF2⇒WF1)⇒WF2) | |
| Ax4(V,T,WF) | ∀V WF(V)⇒WF(T)(T is a term free for V in WF) | Next comes two predicate axioms |
| Ax5(V,WF) | ∀V(WF1⇒WF2)⇒(WF1⇒∀V WF2) WF1 has no free occurence of V | |
| Ind(V,WF) | WF(0) ⇒((∀V (WF(V) ⇒ WF(V'))) ⇒ ∀V WF(V)) | These are the axioms of integer arithmetic |
| I1 | x=y⇒(x=z⇒y=z) | |
| I2 | x=y⇒x'=y' | |
| I3 | ¬0=x' | |
| I4 | x'=y'⇒x=y | |
| I5 | x+0=x | |
| I6 | x+y'=(x+y)' | |
| I7 | x*0=0 | |
| I8 | x*y'=(x*y)+x | |
| MP(WF1,WF2) | WF1,WF1 ⇒ WF2 |- WF2 | Finally two rules of deduction |
| Gen(V,WF) | WF |- ∀V WF |
Note that this is a very sparse proof system - it doesn't contain the symbols ∧, ∨, or ∃, - each of these can be defined in terms of the symbols given.
A proof then is a sequence of statements, each of which is either an instance of an axiom, or can be derived from earlier axioms in the sequence using the two rules of deduction. The final statement in the sequence is the result which has been proved. For an example of such a proof based on these axioms see A formal proof that 1+1=2