5/5: Sean Ebels-Duggan
“Why is Arithmetic Incomplete?”
4:30-6:30 pm, Cobb 102 (campus map)
The following is optional background reading:
On the Incompleteness Theorems, Henryk Kotlarski
“Why is Arithmetic Incomplete?”
4:30-6:30 pm, Cobb 102 (campus map)
The following is optional background reading:
On the Incompleteness Theorems, Henryk Kotlarski
May 11th, 2009 at 4:28 pm
To connect the independence of consistency to fast growing functions, it might be worth looking at a constructive theory, and the proof of consistency stated as FOR ALL P either NOT Provable(P) or NOT Provable(NOT P). In this form, a constructive proof provides a choice procedure for the unprovable side of a proposition, and the running time of such a procedure (perhaps only in the cases where either P or NOT P is provable, so the choice is constrained) might be the fast-growing function in question.
I thought of this point partly because I recalled that the question of provably reducing a PI_2 formula to a PI_1 formula, which depends entirely on the growth rate of the Skolem/witness function, turns out to be the same for Classical and Constructive proofs.
May 12th, 2009 at 3:08 pm
Here’s one way to understand the independence of consistency from a computational point of view. I’m pretty sure that this one doesn’t depend on the choice of a classical vs. constructive theory.
There is a nice general theorem that “subrecursive” programming systems—systems in which all programs always halt (plus some weak assumptions about composability of programs, which are hard to avoid satisfying) cannot program their own interpreters. This is a major reason why all widely used programming languages allow infinite loops—to avoid the possibility of infinite loops they would give up the ability to write interpreters.
The provably total Turing Machines in almost any sensible theory of arithmetic form such a subrecursive programming system.
If our theory could prove FOR ALL P either NOT Provable(P) or NOT Provable(NOT P), then we could prove the termination of a TM that simultaneously searches for a proof of P and a proof of NOT Provable(P) (I’m pretty sure that I got the positives and negatives right here, but it’s confusing). By applying that program to formulae defining the functions computed by provably total TMs, we get a provably total interpreter for the provably total functions.
I’m not totally confident that I haven’t missed a loophole, but I think this is right. Not sure how satisfying it is. It certainly does not characterize provability of PI_1 formulae, but it relates independence of consistency to the provably total computable functions, which are the same ones that determine PI_2 reducibility to PI_1.
I think of the form FOR ALL P either NOT Provable(P) or NOT Provable(NOT P) as a constructive form of the statement of consistency. In a constructive theory, I suppose that we would prove this form directly. In a classical theory, it follows from the usual NOT Provable(0=1). I don’t think it makes a difference to the connection with the provably total computable functions which way we do it.
May 13th, 2009 at 3:31 pm
I think I should not have said, “simultaneoulsy searches for a proof of P and a proof of NOT Provable(P).” Rather, it should have been “a proof of NOT Provable(P) and a proof of NOT Provable(NOT P).” That’s the form that is supported directly by the formula expressing consistency. I think (still worried that I’ve missed a loophole) that the special forms of formulae expressing the values of provably total computable functions make NOT Provable(NOT P) a satisfactory substitute for P.
That is, to get an actual value of a provably total computable function, there is indeed a proof of P, and with provable consistency that yields a proof of NOT Provable (NOT P), and rules out a proof of NOT Provable(P). So, the search above indeed finds all of the values of the provably totally computable functions. It cannot find an incorrect value, because the values of the functions are provably unique, the correct value is provable, and consistency (just the fact of consistency here, I think, not its provability) rules out a contradictory proof of an incorrect value.