Fixed point Lemma
in [Logic]
|
From: apoorv on 13 May 2010 14:38 On May 12, 3:15 pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > apoorv says... > > >'Next, we have to compute s4, stringSub(s1,s2,s3). > >So if you replace "x_0" in s3 by "1234567", you get > > >s4 = "forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=1" > > >To complete the computation of sub(1234567,0,1234567), we > >have to take the code of s4. But note: > >s4 is the same as Q3' > >Above extract from your message. > >Computation of Q3 requires computation of the string s4, which is the > >same as string Q3. > > Look, we have the string Q3. It's > > "forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=1" > > We can compute its code. > 'f' --> 102 > 'o' --> 111 > 'r' --> 114 > ... > 's' --> 115 > 'u' --> 117 > 'b' --> 98 > '(' --> 40 > ... > > So the code of Q3 is some huge, but specific number, > 102111114... > We know exactly what number it is. > > By the way we defined the sub function, we also know that > sub(1234567,0,1234567) = 102111114... > (the same number). > > So we have: > > 1. Q3 <-> forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=1 > 2. code(Q3) = 102111114... > 3. sub(1234567,0,1234567) = 1021111114... > > Therefore, from 1&3, we get > 4. Q3 <-> forall x_1 (1021111114... = x_1) -> x_1=1 > > Line 4 is equivalent to > 5. Q3 <-> 1021111114... = 1 > > By 2, we then have > 6. Q3 <-> code(Q3) = 1 > > So Q3 is a fixed point of the formula > x_0 = 1 > > -- > Daryl McCullough > Ithaca, NY I can quite see the point made above, but there is this alternative view which kind of lingers and refuses to fade away in my mind. Briefly,it is this: sub(x,y,z) as defined is a program that computes the function sub(x,y,z) (To distinguish the function and the program that computes the function ,let us call the program Psub(x,y,z) and the function it computes fsub(x,y,z) Now Psub(x_0,0,x_0) {i.e sub(x_0,0,x_0) of your post} does the following: 1)On input 100,(i.e contents of x_0 set to 100) 2) Reads the content of the variable (storage location)x_0. which is 100. 3)Decodes 100 to find the corresponding function.Lets say it is the function (of a single variable)represented by program H.In general,H must specify the variable (storage location) which would not be (the location)x_0. 4) Computes H for the input 100. 5)codes the output and returns the value. Suppose Psub(x_0,0,x_0) itself has the code 12345. Now, what happens when Psub(x-0,0,x_0) attempts to compute input 12345 ? It decodes 12345 to find the corresponding program, which is Psub(x_0,0,x_0) itself and computes it for input 12345. So, on input corresponding to its own value, Psub(x_0,0x_0) enters a loop. The same argument, suitably adapted, would apply to Q2 of your post, when it attempts to compute on an input that is its own code (1234567 in your example). So, do we not need to distinguish between the case when a given value of the variable x_0 is an input to the program Psub, and when the value merely replaces x_0 in the (java)code for that program? -apoorv
From: Daryl McCullough on 13 May 2010 15:30 apoorv says... >I can quite see the point made above, but there is this alternative >view which kind of lingers and refuses to fade away in my mind. >Briefly,it is this: sub(x,y,z) as defined is a program that computes >the function sub(x,y,z) (To distinguish the function and the program >that computes the function ,let us call the program Psub(x,y,z) and >the function it computes fsub(x,y,z) >Now Psub(x_0,0,x_0) {i.e sub(x_0,0,x_0) of your post} does the >following: >1)On input 100,(i.e contents of x_0 set to 100) >2) Reads the content of the variable (storage location)x_0. which is >100. >3)Decodes 100 to find the corresponding function. You're already completely wrong. I thought I described what sub(x,y,z) does. Here it is again: To compute sub(x,y,z): 1. Compute the string representation of input x. Call that A. 2. Compute the string representation of the variable whose code is y. Call that B. 3. Decode input z to get a third string, C. 4. Now, replace all occurrences of B appearing in C by A. Call the result D. 5. Return the code of D. So for example, suppose we want to compute sub(42,0,120095048061048) 1. First, we compute the string representation of the first input, 42, and call that A. So A is just "42". 2. Next, we compute the string representation of the variable whose code is the second input, 0. That's the string "x_0". (We assume that the variables are "x_0", "x_1", ..., and we just code them by their subscript.) So B is just "x_0". 3. Next, we decode the third argument, which is 120095048061048. Here's how we decode it: 120 --> 'x' 095 --> '_' 048 --> '0' 061 --> '=' 048 --> '0' So 120095048061048 codes the string "x_0=0". We call that C. 4. Now, replace all instances of B occurring in C by A. So we replace all instances of "x_0" in "x_0=0" by "42". The result is "42=0". Call this D. 5. Now, return the code of D. We compute the code as follows: '4' --> 052 '2' --> 050 '=' --> 061 '0' --> 048 So the code of "42=0" is 052050061048. So what we have shown is sub(42,0,120095048061048) = 052050061048 There is no computing of functions involved. We are simply going back and forth between strings and naturals. Now, the string may very well be the name of a function; it may even be the name of the function sub itself. But that doesn't make any difference. All the operations in computing sub(x,y,z) involve only string manipulations. >Suppose Psub(x_0,0,x_0) itself has the code 12345. >Now, what happens when Psub(x_0,0,x_0) attempts to compute input >12345? Nothing in particular. Psub(12345,0,12345) will work as follows: 1. First we get the string representation of the first argument. The result is just "12345". 2. We get the string representation of the variable whose code is the second argument. The result is "x_0". 3. We decode the third argument to get a string. That string is (we are assuming) "Psub(x_0,0,x_0)". 4. Now we replace "x_0" in the string computed in 3 by "12345". The result is "Psub(12345,0,12345)" 5. Now, we compute the code of the string computed in 5. 'P' --> 080 's' --> 115 'u' --> 117 'b' --> 098 '(' --> 040 etc. So the code will be some huge number that starts off 080115117098040... -- Daryl McCullough Ithaca, NY
From: apoorv on 8 Jun 2010 07:32 On May 14, 12:30 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > apoorv says... > > >I can quite see the point made above, but there is this alternative > >view which kind of lingers and refuses to fade away in my mind. > >Briefly,it is this: sub(x,y,z) as defined is a program that computes > >the function sub(x,y,z) (To distinguish the function and the program > >that computes the function ,let us call the program Psub(x,y,z) and > >the function it computes fsub(x,y,z) > >Now Psub(x_0,0,x_0) {i.e sub(x_0,0,x_0) of your post} does the > >following: > >1)On input 100,(i.e contents of x_0 set to 100) > >2) Reads the content of the variable (storage location)x_0. which is > >100. > >3)Decodes 100 to find the corresponding function. > > You're already completely wrong. I thought I described what sub(x,y,z) > does. Here it is again: > > To compute sub(x,y,z): > 1. Compute the string representation of input x. Call that A. > 2. Compute the string representation of the variable whose code is y. > Call that B. > 3. Decode input z to get a third string, C. > 4. Now, replace all occurrences of B appearing in C by A. Call the > result D. > 5. Return the code of D. > > So for example, suppose we want to compute > > sub(42,0,120095048061048) > > 1. First, we compute the string representation of the first input, > 42, and call that A. So A is just "42". > 2. Next, we compute the string representation of the variable whose code > is the second input, 0. That's the string "x_0". (We assume that the > variables are "x_0", "x_1", ..., and we just code them by their subscript..) > So B is just "x_0". > 3. Next, we decode the third argument, which is 120095048061048. Here's > how we decode it: > 120 --> 'x' > 095 --> '_' > 048 --> '0' > 061 --> '=' > 048 --> '0' > So 120095048061048 codes the string "x_0=0". We call that C. > 4. Now, replace all instances of B occurring in > C by A. So we replace all instances of "x_0" in "x_0=0" by > "42". The result is "42=0". Call this D. > 5. Now, return the code of D. We compute the code as follows: > '4' --> 052 > '2' --> 050 > '=' --> 061 > '0' --> 048 > So the code of "42=0" is 052050061048. > > So what we have shown is > sub(42,0,120095048061048) = 052050061048 > > There is no computing of functions involved. We are simply going > back and forth between strings and naturals. Now, the string may > very well be the name of a function; it may even be the name of > the function sub itself. But that doesn't make any difference. > All the operations in computing sub(x,y,z) involve only > string manipulations. > > >Suppose Psub(x_0,0,x_0) itself has the code 12345. > >Now, what happens when Psub(x_0,0,x_0) attempts to compute input > >12345? > > Nothing in particular. > Psub(12345,0,12345) will work as follows: > 1. First we get the string representation of the first argument. > The result is just "12345". > 2. We get the string representation of the variable whose code > is the second argument. The result is "x_0". > 3. We decode the third argument to get a string. That > string is (we are assuming) "Psub(x_0,0,x_0)". > 4. Now we replace "x_0" in the string computed in 3 by > "12345". The result is "Psub(12345,0,12345)" > 5. Now, we compute the code of the string computed in 5. > 'P' --> 080 > 's' --> 115 > 'u' --> 117 > 'b' --> 098 > '(' --> 040 > etc. > So the code will be some huge number that starts off > 080115117098040... > > -- > Daryl McCullough > Ithaca, NY Did not want to start with a new thread, so a belated continuation. It is still not clear to me that a variable could be replaced by a constant in (the code of ) a program and yet the resultant code would be syntactically correct and not give a compiler error. Also, a diagonaliation approach seems to give a different self referential sentence. The informal argument is : for a given coding of Turing machines, the set {x:PA proves that machine X with code x does not halt on input x} is r.e and is accepted by a machine P with code p. Then P halts on x iff PA proves that X does not halt on x. So,P does not halt on p iff PA does not prove that P does not halt on P. if we set Q as "P does not halt on p' then Q<-->PA does not prove Q. Is this argument correct? Further, if P does not halt on p and PA does not prove that it does not halt on p, then would it be correct to say that P does not halt on p nor can be detected to be in a loop at any finite instant of time?In other words, given a number a, is it that we cannot ascertain in a finite time that it is the code of the godel sentence? -apoorv
From: Daryl McCullough on 8 Jun 2010 09:50 apoorv says... >Did not want to start with a new thread, so a belated continuation. >It is still not clear to me that a variable could be replaced by a >constant in (the code of ) a program and yet the resultant code would >be syntactically correct >and not give a compiler error. Diagonalization is applied to *sentences*, not programs. Now, a sentence might *mention* a program. For example, the sentence "Program P running on input 12 produces output 42" mentions program P. But that sentence is not itself a program. The claim of the fixed point lemma is this: If Phi is any formula (in the language of arithmetic, but this is also true for many other languages) with a free variable, then there is a sentence (closed formula) G such that G <-> Phi(#G) where #G means the Godel code of G, and Phi(#G) means the result of replacing the free variable of Phi by #G. There is a related fact about programs, though. Suppose we have a program transformation F. F takes the code for a program as an input, and returns the code for a possibly modified program as an output. Then F has a fixed point, in the sense that there is a program P such that P and F(P) are different codes for the same function. This is proved using a diagonalization procedure similar to the one used by Godel. >Also, a diagonaliation approach seems to give a different self >referential sentence. >The informal argument is : >for a given coding of Turing machines, the set >{x:PA proves that machine X with code x does not halt on input x} is >r.e and is accepted by a machine P with code p. >Then P halts on x iff PA proves that X does not halt on x. >So,P does not halt on p iff PA does not prove that P does not halt on >P. That's an example of the second notion of fixed point I mentioned above. Let F be the program transformation that works as follows: If P is the code for a program, then F(P) = P', where P' behaves as follows, when given an input x: Search for a proof in PA that P never halts on input x. If such a proof is found, then return 0. Otherwise, run forever. By the fixed-point lemma, there is a program P such that P and F(P) compute the same function. That means that, on input x, If PA proves that P never halts on input x, then P returns 0. Otherwise, P never halts. So P(x) halts if and only if PA proves that it does not halt. We can actually say something more, if we use some facts about PA. If P(x) halts, then PA can certainly *prove* that it halts. And if PA is sound (never proves anything false) then we can also conclude that if PA proves that P(x) halts, then P(x) really does halt. From these facts, it follows that If PA is sound, then P(x) does not halt, but this fact is not provable in PA. >if we set Q as "P does not halt on p' then >Q<-->PA does not prove Q. >Is this argument correct? Yes. >Further, if P does not halt on p and PA does >not prove that it does not halt on p, then would it be correct to say >that P does not halt on p nor can be detected to be in a loop at any >finite instant of time?In other words, given a number a, is it that we >cannot ascertain in a finite time that it is the code of the godel >sentence? No, that doesn't follow. Knowing that Q is a Godel sentence does mean that you know that Q is true, *unless* you know that PA is sound (never proves false sentences). PA cannot prove that it is sound. -- Daryl McCullough Ithaca, NY
From: apoorv on 9 Jun 2010 02:56
On Jun 8, 6:50 pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > apoorv says... > > >Did not want to start with a new thread, so a belated continuation. > >It is still not clear to me that a variable could be replaced by a > >constant in (the code of ) a program and yet the resultant code would > >be syntactically correct > >and not give a compiler error. > > Diagonalization is applied to *sentences*, not programs. > Now, a sentence might *mention* a program. For example, > the sentence "Program P running on input 12 produces output 42" > mentions program P. But that sentence is not itself a program. > > The claim of the fixed point lemma is this: > If Phi is any formula (in the language of arithmetic, > but this is also true for many other languages) > with a free variable, then there is a sentence (closed > formula) G such that > > G <-> Phi(#G) > > where #G means the Godel code of G, and Phi(#G) means > the result of replacing the free variable of Phi by #G. > > There is a related fact about programs, though. Suppose > we have a program transformation F. F takes the code for > a program as an input, and returns the code for a possibly > modified program as an output. Then F has a fixed point, > in the sense that there is a program P such that > P and F(P) are different codes for the same function. > > This is proved using a diagonalization procedure similar to > the one used by Godel. > > >Also, a diagonaliation approach seems to give a different self > >referential sentence. > >The informal argument is : > >for a given coding of Turing machines, the set > >{x:PA proves that machine X with code x does not halt on input x} is > >r.e and is accepted by a machine P with code p. > >Then P halts on x iff PA proves that X does not halt on x. > >So,P does not halt on p iff PA does not prove that P does not halt on > >P. > > That's an example of the second notion of fixed point I > mentioned above. Let F be the program transformation that > works as follows: > > If P is the code for a program, then F(P) = P', > where P' behaves as follows, when given an input x: > > Search for a proof in PA that P never halts on input x. If > such a proof is found, then return 0. Otherwise, run forever. > > By the fixed-point lemma, there is a program P such that > P and F(P) compute the same function. That means that, on > input x, > > If PA proves that P never halts on input x, then P returns 0. > Otherwise, P never halts. > > So P(x) halts if and only if PA proves that it does not halt. > > We can actually say something more, if we use some facts about PA. > If P(x) halts, then PA can certainly *prove* that it halts. And if > PA is sound (never proves anything false) then we can also conclude > that if PA proves that P(x) halts, then P(x) really does halt. > From these facts, it follows that > > If PA is sound, then P(x) does not halt, but this fact is not > provable in PA. > > >if we set Q as "P does not halt on p' then > >Q<-->PA does not prove Q. > >Is this argument correct? > > Yes. > > >Further, if P does not halt on p and PA does > >not prove that it does not halt on p, then would it be correct to say > >that P does not halt on p nor can be detected to be in a loop at any > >finite instant of time?In other words, given a number a, is it that we > >cannot ascertain in a finite time that it is the code of the godel > >sentence? > > No, that doesn't follow. Knowing that Q is a Godel sentence does > mean that you know that Q is true, *unless* you know that PA is > sound (never proves false sentences). PA cannot prove that it is > sound. > > -- > Daryl McCullough > Ithaca, NY If PA is sound, then PA does not halt on p nor can it be detected to be in a loop at any finite instant of time.( Because if we could so detect it to be in aloop, the sequence of configurations would constitute a proof in PA that P lops on p),. So, is it that P jusst goes on forever on input p without halting or looping? So, is it that 'loops' and 'does not halt' are not equivalent? Suppose, again assuming PA to be sound, we want to test some number q for whether it is the code of the (self referential) machine P.We decode q to get Q and run Q on q. If Q halts or loops in a finite time on q, we conclude that q is not the required code. We would know that q is the required code only after 'Q has run forever without halting or looping'. That is, there is no way of identifying the code of the godel formula in finite time. Is that a correct inference? -apoorv |