Fixed point Lemma
in [Logic]
|
From: Daryl McCullough on 6 May 2010 15:33 apoorv says... >It is easy even for me to see that S(a,a,y) where a is a given number >can be coded. >What i am unable to see is that there is a formula S(x,x,y) where x >can have any arbitrary value >and there are no bounds on the length of the formula that x may >represent. Well, that's exactly what Godel explained in his classic paper, and some variant of that is explained in every textbook on mathematical logic. One of the most basic facts that you need for Godel's proof is that all computable functions are representable by a formula in arithmetic. The operation of substituting a term for a variable in a formula is certainly computable, so there is a corresponding formula representing it. >> Yes, if you like, you can make a more complicated substitution formula: >> >> S'(x,y,z,w) >> >> which says that w is the code of the result of substituting >> the numeral corresponding to x for variable number y in the >> formula whose code is z. There is no point in introducing >> this complication. It doesn't change anything. The fixed point >> lemma goes through just the same. >> >> Pick a variable, say "x", it will have some code, say 57. >> Then let P be the formula >> >> forall w, S'(x,57,x,w) --> Phi(w) > This is not clear. Are we substituting x for the variable whose code >is 57 i.e x, in the formula whose code is x? >would this not give w=x? No! No! No! Do you understand the difference between the two different uses of 'x' in the following two sentences? 1. x+1=58 2. code('x')+1=58 In sentence 1, 'x' is being used as a variable. So sentence 1 is not a closed sentence. It has a free variable in it. It's neither true nor false. In sentence 2, 'x' is being used as the name of a variable. code('x') is some natural number. We are supposing that code('x') = 57. So, sentence 2 is *true*. So it is not true that forall w, S'(x,57,x,w) <-> w=x But it is true that forall w, S'(code('x'),57,code('x'),w) <-> w=code('x') -- Daryl McCullough Ithaca, NY
From: apoorv on 7 May 2010 13:34 On May 7, 12:33 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > apoorv says... > > >It is easy even for me to see that S(a,a,y) where a is a given number > >can be coded. > >What i am unable to see is that there is a formula S(x,x,y) where x > >can have any arbitrary value > >and there are no bounds on the length of the formula that x may > >represent. > > Well, that's exactly what Godel explained in his classic paper, > and some variant of that is explained in every textbook on mathematical > logic. > > One of the most basic facts that you need for Godel's proof is > that all computable functions are representable by a formula in > arithmetic. The operation of substituting a term for a variable > in a formula is certainly computable, so there is a corresponding > formula representing it. > > > > >> Yes, if you like, you can make a more complicated substitution formula: > > >> S'(x,y,z,w) > > >> which says that w is the code of the result of substituting > >> the numeral corresponding to x for variable number y in the > >> formula whose code is z. There is no point in introducing > >> this complication. It doesn't change anything. The fixed point > >> lemma goes through just the same. > > >> Pick a variable, say "x", it will have some code, say 57. > >> Then let P be the formula > > >> forall w, S'(x,57,x,w) --> Phi(w) > > This is not clear. Are we substituting x for the variable whose code > >is 57 i.e x, in the formula whose code is x? > >would this not give w=x? > > No! No! No! Do you understand the difference between the > two different uses of 'x' in the following two sentences? > > 1. x+1=58 > 2. code('x')+1=58 > > In sentence 1, 'x' is being used as a variable. So sentence > 1 is not a closed sentence. It has a free variable in it. > It's neither true nor false. > > In sentence 2, 'x' is being used as the name of a variable. code('x') is > some natural number. We are supposing that code('x') = 57. So, sentence > 2 is *true*. This is clear to me. > So it is not true that > > forall w, S'(x,57,x,w) <-> w=x There is some subtle point here that is completely escaping me. S'(x,57,x,w) says that -- w is the code of the result of substituting the numeral corresponding to x for the variable number 57 in the formula whose code is x. Is it possible to clarify this more with the help of some simple coding? > But it is true that > > forall w, S'(code('x'),57,code('x'),w) <-> w=code('x') How does one read this? w is the code of the result of substituting the numeral corresponding to code('x') [is this 57?] in the variable number 57 [is this x?] in the formula whose code is code ('x') [57?]. But 57 is the code of a variable and not that of a formula. Again, I am afraid, I am missing something which in all probability is quite obvious to you.Please clarify. -apoorv
From: Daryl McCullough on 7 May 2010 23:12 apoorv says... > >On May 7, 12:33=A0am, stevendaryl3...(a)yahoo.com (Daryl McCullough) >wrote: >> So it is not true that >> >> forall w, S'(x,57,x,w) <-> w=x > There is some subtle point here that is completely escaping me. >S'(x,57,x,w) says that -- w is the code of the result of substituting >the numeral corresponding to x for the variable >number 57 in the formula whose code is x. Is it possible to clarify >this more with the help of some simple coding? Okay. Let's just use the ASCII coding that I mentioned earlier. Let Phi be the formula x=0 It's code is given by: x --> 120 = --> 61 0 --> 48 Put it all together (adding 0s as padding, so that each code is three digits) gives the code of Phi as: 120061048 We'll write that as code(Phi) for short. Now, the formula Phi has 'x' as a free variable If we replace x in Phi by 120061048, we get a new formula (call it Phi'): 120061048=0 Phi' has a much longer code, which we can work out 1 --> 49 2 --> 50 0 --> 48 0 --> 48 6 --> 54 1 --> 49 0 --> 48 4 --> 52 8 --> 56 = --> 61 0 --> 48 Putting it all together (with padding) gives: 49050048048054049048052056061048 So code(Phi') = that huge number. So we conclude: 49050048048054049048052056061048 is the code of the formula (namely, Phi') resulting from replacing the variable whose code is 120 (namely,"x") by 120061048 (the code of Phi) in the formula (again, Phi) whose code is 120061048. By the way we defined our formula S', S'(x,y,z,w) means that w is the code of the formula resulting from replacing the variable whose code is y by the numeral for x in the formula whose code is z. (I may have switched the roles for x and y, I don't remember). So in our case, x = 120061048, y = 120, z = 120061048, and w = 49050048048054049048052056061048 So we conclude: S'(120061048,120,120061048,49050048048054049048052056061048) is true. -- Daryl McCullough Ithaca, NY
From: apoorv on 9 May 2010 03:08 On May 8, 8:12 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > apoorv says... > > > > >On May 7, 12:33=A0am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >> So it is not true that > > >> forall w, S'(x,57,x,w) <-> w=x > > There is some subtle point here that is completely escaping me. > >S'(x,57,x,w) says that -- w is the code of the result of substituting > >the numeral corresponding to x for the variable > >number 57 in the formula whose code is x. Is it possible to clarify > >this more with the help of some simple coding? > > Okay. Let's just use the ASCII coding that I mentioned earlier. > > Let Phi be the formula > > x=0 > > It's code is given by: > > x --> 120 > = --> 61 > 0 --> 48 > > Put it all together (adding 0s as padding, so that each code is > three digits) gives the code of Phi as: > > 120061048 > > We'll write that as code(Phi) for short. > > Now, the formula Phi has 'x' as a free variable > If we replace x in Phi by 120061048, we > get a new formula (call it Phi'): > > 120061048=0 > > Phi' has a much longer code, which we can work out > 1 --> 49 > 2 --> 50 > 0 --> 48 > 0 --> 48 > 6 --> 54 > 1 --> 49 > 0 --> 48 > 4 --> 52 > 8 --> 56 > = --> 61 > 0 --> 48 > > Putting it all together (with padding) gives: > > 49050048048054049048052056061048 > > So code(Phi') = that huge number. > > So we conclude: > > 49050048048054049048052056061048 > is the code of the formula (namely, Phi') resulting from replacing > the variable whose code is 120 (namely,"x") by 120061048 (the code > of Phi) in the formula (again, Phi) whose code is 120061048. > > By the way we defined our formula S', > S'(x,y,z,w) means that w is the code of the formula resulting > from replacing the variable whose code is y by the numeral for > x in the formula whose code is z. (I may have switched the roles > for x and y, I don't remember). > > So in our case, x = 120061048, > y = 120, > z = 120061048, > and > w = 49050048048054049048052056061048 > > So we conclude: > > S'(120061048,120,120061048,49050048048054049048052056061048) > > is true. > > -- > Daryl McCullough > Ithaca, NY x in the above computation has appeared as a code for an arbitrary formula with a free variable and also as the free variable in that very formula. The computation above leads to the sentence S'(120061048,120,120061048,49050048048054049048052056061048) which has no variable free. What we are looking for is a formula S'(x,y,x,w) which has a variable free. Suppose, as a simple coding , an arbitrary constant 'a' codes the formula Fa(x).[read a as a subscript to F]. Thus, 1 codes F1(x) ,2 codes F2(x) and so on. Now a is an arbitrary constant and could be generalized , but not to x. Otherwise we would have x coding Fx(x) so that 1would code the sentence F1(1) and not the formula F1(x) and so on. Further, as x codes Fx(x), the replacement of x in Fx(x) by the variable whose code is 120, i.e x returns Fx(x) only and we get w=x. So, if x is the free variable occurring in the formulas, then the constant 'a' representing the code of an arbitrary formula cannot be generalized to x. So, should we have our substitution formula as S'(x,y,x,w) with y not being the same as the variable x? -apoorv
From: Daryl McCullough on 9 May 2010 09:22
apoorv says... >What we are looking for is a formula S'(x,y,x,w) which has a variable >free. I didn't know we were looking for that. The formula S' will be pretty complicated, but Godel's paper (or any textbook describing Godel's theorem) shows how to construct it. >Suppose, as a simple coding , an arbitrary constant 'a' codes the >formula Fa(x).[read a as a subscript to F]. >Thus, 1 codes F1(x) ,2 codes F2(x) and so on. >Now a is an arbitrary constant and could be generalized , but not to >x. I think you are getting confused about variables and numbers. Codes are natural numbers. A variable can't be a code. However, you can use variables to *stand* for actual numbers. If I say something like: "Let Phi be any formula. Let its code be x." I don't literally mean that Phi's code is the variable x. Phi will be some formula, and its code will be some natural number. But I haven't specified *which* natural number. So I use the variable x to mean some unspecified natural number. Do you understand Java programming? Then maybe Java would help you to understand what is going on. We need functions that map back and forth between statements (represented as strings) and naturals (I'll use the Java type of int). Let's first introduce the numerals corresponding to integers. Luckily, this is a built-in Java function. String numeral(int x) { Integer i = new Integer(x); return i.toString(); } I also need a function that given an integer returns the corresponding variable. I'm just going to assume that our variables are x_0, x_1, x_2, ... String variable(int x) { return "x_" + numeral(x); } We also need a substitution function. This is built-in to Java, too. String stringSub(String x, String y, String z) { return z.replaceAll(y,x); } (Note, this is a bad way to substitute for variables, because it doesn't take into account the difference between free and bound variables, but I don't care.) Now, we need functions mapping back and forth between ints and strings. You can't actually do it with int, because an int can't be bigger than some maximum value which is much too small to code big strings. But again, I don't care. Let's just assume that there are functions: int code(String x) { return the ASCII code for string x; } String decode(int x) { return the string whose ASCII code is x; } Now, we can define a function purely on ints as follows: int sub(int x, int y, int z) { String s1 = numeral(x); String s2 = variable(y); String s3 = decode(z); String s4 = stringSub(s1,s2,s3); return code(s4); } Okay, now the function sub(x,y,z) takes three naturals and returns a natural. Now, assuming that we have a language for arithmetic that includes the function sub(x,y,z) as a built-in function, then we can define our formula S'(x,y,z,w) as follows: S'(x,y,z,w) <-> sub(x,y,z)=w In terms of this S', we can define a fixed point operator. Here's the Java code for this: String fixedPoint(String Q) { String Q1 = stringSub("x_1",0,Q); // The point of doing this is that if Q has free variable x_0, // then Q1 will have free variable x_1. For example, if Q // were the formula x_0=1, then Q1 would be x_1=1. String Q2 = "forall x_1 (sub(x_0,0,x_0) = x_1) -> " + Q1; // Note. If Q were the formula x_0=1, then Q2 would be // forall x_1 (sub(x_0,0,x_0) = x_1) -> x_1=1 int q2 = code(Q2); String numeral = numeral(q2); String Q3 = stringSub(numeral,0,Q2); return Q3; } Now, let's try to go through the steps of finding the fixed point of the simple formula "x_0=1". So we evaluate fixedPoint("x_0=1"). First, we construct Q1, to get "x_1=1". Next, we construct Q2, to get "forall x_1 (sub(x_0,0,x_0) = x_1) -> x_1=1". Next, we compute the code of Q2, which is some ungodly number. Then we compute the numeral for that code (just the base-ten string representing that number). Let's just suppose that it turns out to be "1234567" (it'll actually be much huger than that). Now, we construct Q3, to get "forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=1". Now, let's start figuring out what Q3 says. We can easily see that Q3 is equivalent to sub(1234567,0,1234567)=1. So let's compute sub(1234567,0,1234567): From the Java definition of sub(x,y,z), we see that first we have to construct s1, which is the numeral corresponding to the first argument, 1234567. So s1 = "1234567" Next, we have to compute s2, which is the variable corresponding to the second argument, 0. That variable is just "x_0". So s2 = "x_0" Next, we have to compute s3 by decoding the third argument, 1234567. We already assumed that that number was the code for "forall x_1 (sub(x_0,0,x_0) = x_1) -> x_1=1". So decoding it gives: s3 = "forall x_1 (sub(x_0,0,x_0) = x_1) -> x_1=1" 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. So we have sub(1234567,0,1234567) = code(Q3) So putting it all together, we have: 1. Q3 == forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=1 2. Q3 <-> sub(1234567,0,1234567)=1 3. sub(1234567,0,1234567) = code(Q3) 4. Q3 <-> code(Q3)=1 So Q3 is the fixed point of the formula x_0 = 1. If you replace the variable x_0 in that formula by the code(Q3), you'll get a statement that is equivalent to Q3 -- Daryl McCullough Ithaca, NY |