So we met two important theories or machines: Classical Logic CL and Peano Arithmetic PA.
As collection of theorems, the first is a subset of the second:
PA | | | CL
Now I have chosen PA to set the things. Any theory or machine rich enough to prove elementary theorems about numbers will do. What will be important is that anybody (including possible machines) should be able to verify "mechanically" if a given proof is a proof, at least in principle (in case a given proof is 2^64 steps long).
We will interview PA about its possible (consistent) extensions.
It is Godel who showed how to make such an interview, by showing how to translate the meta-predicate of "provability" into an arithmetical sentence.
Let me be a little more specific. Don't hesitate to tell me you know all this, but it could help some others, and it could help in front of futur misunderstandings.
PA has a language. Here it is:
L_PA = {v, &, ->, not, t, f, A, E, =, +, *, SUC, 0, (, ), x,y,z,x1, y1, z1, x2, y2, ...}
We could code those symbol by the odd integer above 1. So the Godel number of "v" is 3, and this I abbreviate by ng(v)=3. So ng(&)=5, ng(->)=7, ng(not)=9, ng(t)=11, ..., ng(x)=33, ng(y)=35, etc.
So exactly in the sense that you can define the divisability predicate Div(x,y) (which is true when x divide y) only with the available symbol as in
Div(x,y) = Ez(x*z = y) (there exist a number z such that x multiplied by z gives y)
you can define the meta-predicate IS-A-VARIABLE(x), which is true when x is a number representing a variable, as Godel number. Actually, with the code we have chosen:
IS-A-VARIABLE(x) = ODD(x) & BIGGER-OR-EQUAL(x,3)
= Ey(x=2y+1) & Ez(x = z+33)
Now we want to talk about formula also with PA. I recall that there are precise formula formation rule like if A is a formula then (not A) is a formula if A and B are formula then (A & B) is a formula, etc.
To code a formula by a number, a traditional way relies on the well known fundamental theorem of arithmetic saying that all number have a unique decomposition in product of prime numbers.
So the formula "Ez(x*z = y)" will be coded by the number
2^(ng(E))*3^(ng(z))*5^(ng(())*7^ng(x)*11^(ng(*))*13^(ng(z))* ... (I let you continue) (I have also avoid the quotation mark for not wasting ink, but ng('(') is more readable than ng((), mmhh..
Now, a proof in, or by, PA ["in" if you think as PA being a theory; "by" if you think as PA as a machine (a theorem prover)] is just a sequence of formula such that they are either axioms or has been obtained from the axioms by a finite number of application of the inference rule. So, although it could be hard to *find* a proof (as unpedagogical exercice try to prove the formula (A -> A) in the systeme send yesterday), it is easy to verify a proof once the proof is given.
The point is that we can translate a proof into a number by relying a second time on the fundamental theorem of arithmetic. A proof is just a finite sequence of formula F1 F2 F3 F4 F5 ... FN (actually it will be proof of FN if F1, F2, ... are axioms or comes from axioms and preeceeding formula by application of the inference rule). Its (Godel) number will be
2^ng(F1)*3^ng(F2)*5^ng(F3) ....
Now, like we have define in PA language IS-A-VARIABLE(x) we can translate meta-predicates like IS-AN-AXIOME(x), HAS-BEEN-DERIVED-FROM-MODUS-PONENS(x,y,z), meaning z is derivable from x and y by modus ponens.
Etc. Etc. So that we can defined in PA arithmetical language
IS-A-PROOF-OF(x,y) saying that y is a translation (a godel number of) of a proof of formula (with Godel number) x.
This was the B(x,y) of yesterday.
And then the Godel formula BEW(x), that is PROVABLE(x), is just EyB(x,y) i.e. it exist a number y such that y is a proof of x, to make it short.
Now, a machine will be said to be consistent,if the machine does not prove f. "f" is a symbol with the intended meaning of an absurdity, or a contradiction. in arithmetic f could be defined by the formula (1 = 0), well actually (SUC(0) = 0).
So the consistency of the machine, or of the theory, or of PA (here) can be defined by the formula (not BEW(f)).
Godel second incompleteness theorem is that if a machine is consistent then the machine cannot prove she is consistent. Now I will explain in which sense we can say that to be consistent is the same has having a consistent extension, so you see that Godel second incompleteness explain why, as I said to John, when we ask the machine if she *do* have at least one consistent extension, she remains silent.
Well that is a little bit discouraging isn' it? How could we hope the machine to be able to give us the geometry of its consistent extensions when she remain silent on the very question of having consistent extensions at all?
But if you are patient enough with PA, she will justify her silence by proving that: if she is consistent then she cannot prove her consistency:
PA proves (not BEX(f)) ->(not BEW (not BEX(f))
I will prove Godel's theorem on the way, but I think I will first give you a map of the territory including two paths which make possible to sum up the "mathematical confirmation" in one precise mathematical formula. Well I don't know. Any question or comment?
Bruno
http://iridia.ulb.ac.be/~marchal/