New essay on Goedel's Incompleteness Theorem
in [Logic]
|
Prev: Solutions manual to Mechanical Behavior of Materials, 3E Norman E Dowling
Next: Editor of Physical Review A, Dr Gordon W.F. Drake does WRONG subtraction of 8th Class mathematics.
From: David Libert on 2 Oct 2009 03:05 Aatu Koskensilta (aatu.koskensilta(a)uta.fi) writes: > stevendaryl3016(a)yahoo.com (Daryl McCullough) writes: > >> I think perhaps what you mean is for there to be a sequence of >> different formulas G, G', G'', ... such that >> >> G == G' is not provable >> G' == G'' is not provable >> G'' == G''' is not provable >> etc. >> >> It's possible that you could construct such a sequence, [ - - -] > > We can construct such a sequence using the recursion theorem: let f be a > recursive function such that > > f(x) = [~Prov_T({e}(x+1))] > > where the square brackets take a formula to its G�del number, {} are the > Kleene brackets, and e is an index of f. For no n is f(n) the code for a > provable sentence. I don't think we can do without recursion theoretic > machinations -- in particular, the usual devices of provability logic > appear to be insufficient. I could be wrong. > > -- > Aatu Koskensilta (aatu.koskensilta(a)uta.fi) I think the answer depends on the details of how we formalize the statement in question. So in the original question above, what do we take to be the formal statement of the requirement: >> G == G' is not provable and so on for the later ones? Aatu's solution gives a reasonable version of this, and can be consdered as one reasonable affirmative answer to the orginal question. Namely for the G instance I just quoted above, Aatu's solution gives a G of form: G == ~Prov_T(t), for t a complex term derived from the recursion theorem, which the object theory proves denotes a Godel number of a sentence, hich we would then define to be sentence G'. The term t would be an evaluation using the term defined in the proof of the recursion theorem, which is similar to the proof of Godel's fixed point theorem and involves applying the universal rescursive function to 2 copies of the same variable. This evaluates in the object theory to a Godel number, in the sense that the theory proves term t is = to a term of the form a numneral: namely an iteration of the successor function symbol on constant 0, witht eh number of iterations being a Godel number of a sentence, namely G'. On the oter hand, another reasonable straightforward reading of the original question could consider >> G == G' is not provable is asking for G to be the formula ~Prov_T(#G') where #G' is a numeral term, that is successor iterated on 0 as above, for Godel bunber of G'. Aatu's solution does not give this, as the term produced in the proof of the recursion theorem is a complex term. And in fact, with usual defintions of Godel numbers, we can prove there is no such infinite descending sequence as the original question in this reading asked for. Namely consider G = ~Prov_T(#G') and G', I will argue G has a strictly larger Godel number than G'. I don't recall which numbers were picked to code characters, and different versions would disagree anyway, so I will instead agrue by cases. Consider s, the function symbol for successor. I proceed by cases, whether the Godel numbering assiugned s number 0, or a positive number. First assume it assigned s a positive number. Let g' be the Godel number of G' . Then sentence G has embedded in it a succession of nested s applications, in length g'. So the rigthmost s occuurrence has g' -1 many s 's before it. The #G term occurs inside the G sentence, so there is a least one symbol in G before the #G term. So the rightmost s occurrence has at least g' many symbols to the left of it. Actually for the next step I just realized I didn't need that final + 1 adjustment but I will leave it in as extra room in case there was some boundary condition to arise. So from the g' - 1 earlier symbols, the rightmost s is coded by at least a power of the g' th prime. But the g' 'th prime is > g' . And s had code >0, so the Godel number for G includes a factor of a positive power of a number > g' . So G has Godel number > g' . That completes the case successor symbol s with positive code. So suppose s had code 0. So the other symbols of the language don't have code 0. G as a well formed sentence doesn't have final synbol s, ie all s occurrences must apply to arguments. So consider the final symbol of G. It is not s, so it has positive code (since s is assumed to have 0 code). So the final symbol of G is a positive power of a prime, the length of G 'th prime. But this prime is > length of G. And G included an iteration of successor g' many times, so G has length > g'. So the factor cloding the final G symbol is a positive power of a number > g' . So the overall product is > g' . That rooduct is the Giodel number for G . The concludes the proof, G has strictly larger Godel number than G'. But apply the same proof to every successive step of the omega sequence: G , G', G'' ... . So the respective Godel numbers of these give an infinite descending sequence of integers. So no seqeunce as required on the numeral reading of the question. -- David Libert ah170(a)FreeNet.Carleton.CA
From: Aatu Koskensilta on 2 Oct 2009 06:29 ah170(a)FreeNet.Carleton.CA (David Libert) writes: > On the oter hand, another reasonable straightforward reading of the > original question could consider > > >> G == G' is not provable > > is asking for G to be the formula ~Prov_T(#G') where #G' is a > numeral term, that is successor iterated on 0 as above, for Godel > bunber of G'. As you note, on that reading there is no sequence of the sort asked for. It didn't occur to me to consider that reading partly because this is rather obvious but mostly because the G�del sentence of a theory itself has the form ~Prov(t) for a complex term t. (The impossibility also holds generally, not only for "usual definitions of G�del numbers".) This is related to the following question that sometimes suggests itself to people pondering the incompleteness theorem and the diagonal lemma: Why can't we simply stipulate that 0 is the code for ~Prov(0) and do without the diagonal lemma? -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechen kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: David Libert on 2 Oct 2009 07:40 Aatu Koskensilta (aatu.koskensilta(a)uta.fi) writes: > ah170(a)FreeNet.Carleton.CA (David Libert) writes: > >> On the oter hand, another reasonable straightforward reading of the >> original question could consider >> >> >> G == G' is not provable >> >> is asking for G to be the formula ~Prov_T(#G') where #G' is a >> numeral term, that is successor iterated on 0 as above, for Godel >> bunber of G'. > > As you note, on that reading there is no sequence of the sort asked > for. It didn't occur to me to consider that reading partly because > this is rather obvious but mostly because the G�del sentence of a > theory itself has the form ~Prov(t) for a complex term t. (The > impossibility also holds generally, not only for "usual definitions of > G�del numbers".) This is related to the following question that > sometimes suggests itself to people pondering the incompleteness > theorem and the diagonal lemma: > > Why can't we simply stipulate that 0 is the code for ~Prov(0) and do > without the diagonal lemma? > > -- > Aatu Koskensilta (aatu.koskensilta(a)uta.fi) Thanks for your followup. This has led me to some further intersting questions related to all this. I just checked back to Daryl's original question, and I see he specified the formulas of G, G', G'' are to be different. When I first read his question, I thought of the numeral reading and didn't notice that specification. The numeral reading gets that back independently, as you note the "numeral" version of Godel's theorem is impossible. Anyway, one point is if we drop the requirement the G 's be distinct, and we allow complex terms instead of numerals, another solution is the constant sequence of the usual Godel sentence. Returning to your example, from th recursion theorem, in fact your example does satisfy Daryl's requirement that the formulas be distinct. Namely all the formulas will refer to the same omega sequence of formulas, by the magic of the recursion theorem. The n'th sentence will say: I am talking about the n+1 st sentence of this common sequence, namely it will have a complex term that hard codes n+1 as an index into the sequence. So as n varies, the various sentences will hard code different values of n+1 as the index into the sequence to find what they are talking about, so with these n+1 references varying the sentences will be distinct, as required. But now the following is interesting. Even though they are distinct sentences, the object theory T each one is equivalent to each other one. So mod T provable equivalence, they are not distinct after all. This does not mess up your example, since they were only required to be syntactically distinct, but is an interesting property nonetheless. To see that last claim of all being equivalent, let Gs be the usual Godel sentence for T. (I use Gs as Godel-sentence since the problem statement already used G in its own sequence). Then there is a proof, not required in proving the usual Godel theorem, but interesting in a second look back at it to see side issues, that for Con(T) the usual formalization of the consistency of T (help! save me from George! :-) ) , T |- Gs <-> Con(T). I will imitate that proof for the G, G', G'' sequence. We know a little bit less about these members than we did about Gs, but it turns out we know enough to carry outr a version of that usual proof copied over. So I will discuss the G case from the sequence. The others are all similar. So to argue in T. I want to relate G to Con(T). So in T, I will first assume G and conclude Con(T), then as a second case in T I will assume ~G and conclude ~Con(T). This will be enough to esablish the required equivalernce. So we are in T. Assume G. G is ~Prov_T(t) where t is a comlex term for G'. So by this we have inside T that something is not "provable" from T according to the Prov_T coding of provability. So inside T, about Prov_T and Con(T), we invoke the argument if something isn't provable then the theopry is consistent, the formalized version of this inside T. Next back to T, and assume ~G. So ie assume Prov_T(t), for t a complex tern for G' Godel number. Inside T, we exapand out what t is about namely sentence ~Prov_T(t'') for t'' a complex term for G''. But G'' was itself ~Prov_T(t''') for a complex term t''' for G'''. So once more not merely inside T, but inside the Prov_T predicate inside T, we have T doesn't prove something, ie G'''. So 2 levels in, what T proves about its Prov_T predicate, we do the double formalization again that if something isn't provable then the theory is consitent. So inside T under the current assumption we concluide Prov_T(#Con(T)). So T's formatilization of its T provablilty, it sees T as proving its own consistency. Now redo Godel's 2nd incpmpleteness theorem inside T. Inside T we see T as a theorem proving its own consistency, so by the second Godel incompleteness formalized inside T, we concluded inside T that ~Con(T). So in T we started off assuning ~G, and we have worked to a conclusion of ~Con(T). So this was the 2nd half of the equivelence. So T |- G <-> Con(T) . Similarly for every sentence in the sequence, by going 2 more levels down as I just did for G. So every sentence in your sequence is T provably equivalent to Con(T), so they are also each T provably equivalent to each other. Here is another intersting point. By the standard similar proof to the above, T |- Gs <-> Con(T) . So each sentence in your sequence is T provabily equivalent to Gs, the usual Godel sentence. But Godel's theorem tells us if T is consistent T does not prove Gs, and if T is omega-consistent, T does not prove ~Gs. But Gs is T provably equivalent to each sentence from your sequence. So we have a Godel's theorem, for your sentences too! If T is consistent it doens't prove any sentence from your sequence, and if T is omega-consistent it doens't refute any of those. So this raises the question, can we directly prove that theorem for this sequence. If so, if we had such a direct proof, we could drop out the usual Godel sentence Gs, and just go directly to your sequence. And then we would get a proof like Godel's theorem, all running like you have been saying Scott, becasue as noted the sentences are distinct. But I have not found such a proof. When I try to copy the usual Gs proof to the sequence there is a step missing. Yet the result we want is actually true, by the arguments above. But to see those arguments, in the background we use the usual Gs after all. Can it be done directly, without invoking Gs? I don't know. There is a difficult case to rule out. The sequence G G' G''. What if each second one is provable, and the others aren't? Its not so obvious that can't happen from the imdeiate definition. Maybe the statments are alternately true and false, and the true ones are also provable and the false ones aren't provable. That on the surface looks compatible witht eh basic definitions. My argument above showed that actually is impossible. But it rested on the usual 2nd incompleteness theorem which in turn invoked ther usual Gs. So it doesn't immediately help to make a self contained proof like this. Still it is quite tantalizing, that the claim in question is actually true. So these are all interesting questions, that emerged from your writing, Scott. And of course your example, Aatu. -- David Libert ah170(a)FreeNet.Carleton.CA
From: Nam Nguyen on 3 Oct 2009 13:13 Jesse F. Hughes wrote: > Nam Nguyen <namducnguyen(a)shaw.ca> writes: > >>> Shoenfield does *not* claim L(T) is determined by its axioms. Here's >>> the quote, once again: >>> >>> "We consider a language to be completely specified when its symbols >>> and formulas are specified. This makes a language a purely >>> syntactical object. Of course, most of our languages will have a >>> meaning (or several meanings); but the meaning is not considered to >>> be part of the language. We shall designate the language of a formal >>> system F by L(F)." >>> >>> "The next part of a formal system consists of its /axioms/. Our >>> only requirement on these is that each axiom shall be a formula of >>> the language of the formal system." [p. 4 in my copy of Shoenfield] >>> >>> The first part of a formal system is the language. The *next* part is >>> the axioms. Clearly, then, the axioms do not determine the language. >> You sounded like a kindergarten kid reading technical book for the first >> time, reading _too literally_ what's in the book! Where in Shoenfield's >> book did he say that if one doesn't consider language as the first >> part of formal system, one's reasoning would fall apart? > > Speaking of misreading, where did *I* say that if one doesn't consider > language as the first part of formal system, one's reasoning would > fall apart? Did I say you _literally_ say that? My point here is if my stating that _the_ language of a T is defined by T's axioms were_technically wrong_ there would be a lot of _technical_ theorems and corollaries in Schoenfield's book you could use to tear apart my FOL reasoning in my example here of T = {x+y=0}. But you couldn't. Which means that the portion in his book you cited, to refute my statement, is not technical in nature; for instance it could have been just his style of presenting the FOL matter. But all in all it it has no bearing on the order of language-axiom at all, as I've demonstrated so with my example of T = {x+y=0}. Which you've deliberately ignored of course. > > Anyway, to hell (once again) with this pointless "debate". What's new with Jesse's arguments, then and now? You jumped in *uninvited* and refuted a your opponent's *technical* statement but couldn't have any *technical* to support your own argument. So you just trashed a debate (in the thread) you had yourself created! > As you can > see, Shoenfield wrote clearly and contradicts your interpretation. On page 4. of Schoenfield book one would see his definition of "... formulas ... be the expressions which assert some facts", which of course would, as you've seemed fond to use, "violate" standard definition of a formula. (For the record he did write a different and more formal definition of formulas). As you can see, Jesse F. Hughes, authors do have a right to gloss over, to present materials in his/her own _non-technical_ way, in parts of a book. That doesn't necessarily mean they'd be wrong. But neither does it mean *you* should blindly cling on these _non-technical_ aspects of the statements, for you "technical" refuting! Hope that has been clear for you, so few months from now you don't have to jump in people's conversation uninvited and repeat the same "pointless 'debate'". You've made it a pointless debate really.
From: Nam Nguyen on 3 Oct 2009 13:33
Aatu Koskensilta wrote: > Nam Nguyen <namducnguyen(a)shaw.ca> writes: > >> You seem to have a tendency to interpret things _out of context_, >> for the worse! > > We all need a hobby. But I didn't mean that. I meant habit (i.e. tendency). Any rate, bad "hobby", Aatu! > >> Scott seemed so _desperate_ to the point he would "attack" people >> pointlessly. I just tried to console him that should it be the case >> only he and nobody else would see the (correct) truth, others don't >> have to see it and so he wouldn't need to be frustrated/desperate. > > I think being frustrated or desperate would be a perfectly natural and > appropriate reaction in such a situation, and it seems unlikely merely > contemplating the impersonal nature of mathematical truth would be of > much consolation. Oh, I don't know Aatu. It's just one's personal note to another person. No one is obliged to take it but it's free to take. Some people though do find consolation in contemplation. > In my comment I had in mind in addition to your > reassuring consolation of Scott also various more or less romantic but > historically inaccurate utterances by you about G�del, Brouwer, > Einstein etc. over the years. Is it too much to ask you to cut out this kind of "crabby" way of conversation? In the first place, I don't ever recall I ever said anything about the name "Brouwer": I don't even know what he did or wrote in what field that made him well known (though apparently he must have). Secondly, what "historically inaccurate utterances" made by me did you have in mind? Why didn't discuss at some length _then_ and wait for _years_ to _suddenly_ bring it up? You seem fond to make technical conversations sour? > Those who feel their discoveries have > been unjustly ignored, their cogent arguments met with incredulous > stares and silence, and so on, often find comfort in the idea that > various famous thinkers have in the past had to battle stagnant > orthodoxy and mindless regurgitation of received wisdom, all alone, > armed with nothing but their unwavering conviction and superb > intellect, understood and appreciated only by later generations Kind of a long sentence, I'd think. > -- alas, the historical facts do not usually support anything of the > sort. To some of those people, I suspect, it only takes _one_ case. Are you so sure historically there isn't "anything of the sort" at all? Not even one case? |