Fixed point Lemma
in [Logic]
|
From: Aatu Koskensilta on 11 May 2010 09:44 apoorv <sudhir_sh(a)hotmail.com> writes: > So we have one substitution formula for replacing the free variable v > and another for replacing the free variable x in a given formula? Why not have a peek in a logic text? -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: apoorv on 11 May 2010 13:55 On May 9, 6:22 pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > 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. Then in what sense is x used when we say -x is a variable.? > 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, we construct Q3, to get > "forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=1". > > So we have > sub(1234567,0,1234567) = code(Q3) So, Q3 is "forall x_1 (code (Q3) = x_1) -> x_1=1". So, for returning Q3, the program computes code Q3 and hence Q3. I am not sure, but will not the program get into a loop? -apoorv
From: Daryl McCullough on 11 May 2010 19:48 apoorv says... > >On May 9, 6:22=A0pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: >> Now, we construct Q3, to get >> "forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=3D1". >> >> So we have > >> sub(1234567,0,1234567) = code(Q3) > >So, Q3 is "forall x_1 (code (Q3) = x_1) -> x_1=1". No, I just said that Q3 is "forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=1". You can't substitute equals for equals inside a string. Even if 2+2=4, that doesn't mean that the string "2+2" is equal to the string "4". For example, the first character in the string "2+2" is '2', while the first character in the string "4" is '4'. -- Daryl McCullough Ithaca, NY
From: apoorv on 12 May 2010 01:30 On May 12, 4:48 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > apoorv says... > > > > >On May 9, 6:22=A0pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > >> Now, we construct Q3, to get > >> "forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=3D1". > > >> So we have > > >> sub(1234567,0,1234567) = code(Q3) > > >So, Q3 is "forall x_1 (code (Q3) = x_1) -> x_1=1". > > No, I just said that Q3 is > > "forall x_1 (sub(1234567,0,1234567) = x_1) -> x_1=1". > > You can't substitute equals for equals inside a string. > Even if 2+2=4, that doesn't mean that the string "2+2" > is equal to the string "4". For example, the first > character in the string "2+2" is '2', while the first > character in the string "4" is '4'. > > -- > Daryl McCullough > Ithaca, NY '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. -apoorv
From: Daryl McCullough on 12 May 2010 06:15
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 |