# Diagonalization Fixed Point Exercises

This is the sec­ond of three sets of fixed point ex­er­cises. The first post in this se­quence is here, giv­ing con­text.

1. Re­call Can­tor’s di­ag­o­nal ar­gu­ment for the un­countabil­ity of the real num­bers. Ap­ply the same tech­nique to con­vince your­self than for any set , the car­di­nal­ity of is less than the car­di­nal­ity of the power set (i.e. there is no sur­jec­tion from to ).

2. Sup­pose that a nonempty set has a func­tion from to which lacks fixed points (i.e. for all ). Con­vince your­self that there is no sur­jec­tion from S to , for any nonempty . (We will write the set of func­tions from to ei­ther as or ; these are the same.)

3. For nonempty and , sup­pose you are given a sur­jec­tive func­tion from the set to the set of func­tions from to , and let be a func­tion from to it­self. The pre­vi­ous re­sult im­plies that there ex­ists an in such that . Can you use your proof to de­scribe in terms of and ?

4. Given sets and , let de­note the space of to­tal com­putable func­tions from to . We say that a func­tion from to is com­putable if and only if the cor­re­spond­ing func­tion (given by is com­putable. Show that there is no sur­jec­tive com­putable func­tion from the set of all strings to .

5. Show that the pre­vi­ous re­sult im­plies that there is no com­putable func­tion from which out­puts if and only if the first in­put is a code for a Tur­ing ma­chine that halts when given the sec­ond in­put.

6. Given topolog­i­cal spaces and , let be the space with the set of con­tin­u­ous func­tions from to as its un­der­ly­ing set, and with topol­ogy such that is con­tin­u­ous if and only if the cor­re­spond­ing func­tion (given by ) is con­tin­u­ous, as­sum­ing such a space ex­ists. Con­vince your­self that there is no space which con­tin­u­ously sur­jects onto , where is the cir­cle.

7. In your preferred pro­gram­ming lan­guage, write a quine, that is, a pro­gram whose out­put is a string equal to its own source code.

8. Write a pro­gram that defines a func­tion tak­ing a string as in­put, and pro­duces its out­put by ap­ply­ing to its source code. For ex­am­ple, if re­verses the given string, then the pro­gram should out­puts its source code back­wards.

9. Given two sets and of sen­tences, let be the set of all func­tions from to defined by sub­sti­tut­ing the Gödel num­ber of a sen­tence in into a fixed for­mula. Let be the set of all sen­tences in the lan­guage of ar­ith­metic with one un­bounded uni­ver­sal quan­tifier and ar­bi­trar­ily many bounded quan­tifiers, and let be the set of all for­mu­las with one free vari­ables of that same quan­tifier com­plex­ity. By rep­re­sent­ing syn­tax us­ing ar­ith­metic, it is pos­si­ble to give a func­tion that sub­sti­tutes its sec­ond ar­gu­ment into its first ar­gu­ment. Pick some cod­ing of for­mu­las as nat­u­ral num­bers, where we de­note the num­ber cod­ing for a for­mula as . Us­ing this, show that for any for­mula , there is a for­mula such that .

10. (Gödel’s sec­ond in­com­plete­ness the­o­rem) In the set , there is a for­mula such that holds iff the sen­tence is not prov­able in Peano ar­ith­metic. Us­ing this, show that Peano ar­ith­metic can­not prove its own con­sis­tency.

11. (Löb’s the­o­rem) More gen­er­ally, the di­ag­o­nal lemma states that for any for­mula with a sin­gle free vari­able, there is a for­mula such that, prov­ably, . Now, sup­pose that Peano ar­ith­metic proves that for some for­mula . Show that Peano ar­ith­metic also proves it­self. Some facts that you may need are that (a) when a sen­tence is prov­able, the sen­tence is it­self prov­able, (b) Peano ar­ith­metic proves this fact, that is, Peano ar­ith­metic proves , for any sen­tence and (c) Peano ar­ith­metic proves the fact that if and are prov­able, then is prov­able.

12. (Tarski’s the­o­rem) Show that there does not ex­ist a for­mula with one free vari­able such that for each sen­tence , the state­ment holds.

13. Look­ing back at all these ex­er­cises, think about the re­la­tion­ship be­tween them.

Please use the spoilers fea­ture—the sym­bol ‘>’ fol­lowed by ‘!’ fol­lowed by space -in your com­ments to hide all solu­tions, par­tial solu­tions, and other dis­cus­sions of the math. The com­ments will be mod­er­ated strictly to hide spoilers!

I recom­mend putting all the ob­ject level points in spoilers and in­clud­ing meta­data out­side of the spoilers, like so: “I think I’ve solved prob­lem #5, here’s my solu­tion <spoilers>” or “I’d like help with prob­lem #3, here’s what I un­der­stand <spoilers>” so that peo­ple can choose what to read.

No nominations.
No reviews.
• Ex 8: (in Python, us­ing a re­ver­sal func­tion)

def f(s):
re­turn s[::-1]

dlmt = ’”“”‘
code = “””def f(s):
re­turn s[::-1]

dlmt = ’{}’
code = {}{}{}
code = code.for­mat(dlmt, dlmt, code, dlmt)
print(f(code))”″”
code = code.for­mat(dlmt, dlmt, code, dlmt)
print(f(code))

• Ex 4

Given a com­putable func­tion , define a func­tion by the rule . Then is com­putable, how­ever, be­cause for , we have that and .

Ex 5:

We show the con­tra­pos­i­tive: given a func­tion halt, we con­struct a sur­jec­tive func­tion from to as fol­lows: enu­mer­ate all tur­ing ma­chines, such that each cor­re­sponds to a string. Given a , if does not de­code to a tur­ing ma­chine, set . If it does, let de­note that turn­ing ma­chine. Let with in­put first run halt; if halt re­turns , put out , oth­er­wise will halt on in­put ; run on and put out the re­sult.

Given a com­putable func­tion , there is a string such that im­ple­ments (if the tur­ing the­sis is true). Then , so that is sur­jec­tive.

Ex 6:

Let be a parametriza­tion of the cir­cle given by . Given and , write to de­note the point , where . First, note that, re­gard­less of the topol­ogy on , it holds true that if is con­tin­u­ous, then so is for any , be­cause given a ba­sis el­e­ment of the cir­cle, we have which is open be­cause is con­tin­u­ous.

Let be a con­tin­u­ous func­tion from to . Then is con­tin­u­ous, and so is the di­ag­o­nal func­tion . Fix any , then given by is also con­tin­u­ous, but given any , one has and thus . It fol­lows that is not sur­jec­tive.

Ex 7:

I did it in java. There’s prob­a­bly eas­ier ways to do this, es­pe­cially in other lan­guages, but it still works. It was in­cred­ibly fun to do. My ba­sic idea was to have a loop iter­ate 2 times, the first time print­ing the pro­gram, the sec­ond time print­ing the print­ing com­mand. Es­cap­ing the ” char­ac­ters is the biggest prob­lem, the main idea here was to have a string q that equals ” in the first iter­a­tion and ” + q + ” in the sec­ond. That sec­ond string (as part of the code in an ex­pres­sion where a string is printed) will print it­self in the con­sole out­put. Code:

pack­age maths;pub­lic class Quine{pub­lic static void main(String[]args){for(int i=0;i<2;i++){String o=i==1?”“+(char)34:””;String q=”“+(char)34;q=i==1?q+”+q+”+q:q;String e=i==1?o+”+e);}}}”:”Sys­tem.out.print(o+”;Sys­tem.out.print(o+”pack­age maths;pub­lic class Quine{pub­lic static void main(String[]args){for(int i=0;i<2;i++){String o=i==1?”+q+””+q+”+(char)34:”+q+”“+q+”;String q=”+q+””+q+”+(char)34;q=i==1?q+”+q+”+q+”+q+”+q:q;String e=i==1?o+”+q+”+e);}}}”+q+”:”+q+”Sys­tem.out.print(o+”+q+”;”+e);}}}

• For #6, I have what looks to me like a coun­terex­am­ple. Pos­si­bly I am us­ing the wrong defi­ni­tion of con­tin­u­ous func­tion? I am tak­ing this one as my source.

Take as the topolog­i­cal space the real line un­der the Eu­clidean topol­ogy. Let be the point in at ra­di­ans ro­ta­tion. This is sur­jec­tive; all points in are mapped to in­finitely many times. It is also con­tin­u­ous; For ev­ery and neigh­bor­hood there is a neigh­bor­hood such that ,

The par­tial func­tions f(x) from are also con­tin­u­ous by the same ar­gu­ment.

• Cur­ry­ing doesn’t pre­serve sur­jec­tivity. As a sim­ple ex­am­ple, you can eas­ily find a sur­jec­tive func­tion , but there are no sur­jec­tive func­tions .

• Ah, yes, that makes sense. I got dis­tracted by the defi­ni­tion of ’s topol­ogy

and ap­plied it to sur­jec­tivity as well as con­ti­nu­ity.

• Thoughts on #10:

I am con­fused about this ex­er­cise. The stan­dard/​mod­ern proof of Gödel’s sec­ond in­com­plete­ness the­o­rem uses the Hilbert–Ber­nays–Löb deriv­abil­ity con­di­tions, which are stated as (a), (b), (c) in ex­er­cise #11. If the ex­er­cises are meant to be solved in se­quence, this seems to im­ply that #10 is solv­able with­out us­ing the deriv­abil­ity con­di­tions. I tried do­ing this for a while with­out get­ting any­where.

Maybe an­other way to state my con­fu­sion is that I’m pretty sure that up to ex­er­cise #10, noth­ing that dis­t­in­guishes Peano ar­ith­metic from Robin­son ar­ith­metic has been in­tro­duced (it is only with the in­tro­duc­tion of the deriv­abil­ity con­di­tions in #11 that this differ­ence be­comes ap­par­ent). It looks like there is a ver­sion of the sec­ond in­com­plete­ness the­o­rem for Robin­son ar­ith­metic, but the pa­per says “The proof is by the con­struc­tion of a non­stan­dard model in which this for­mula [i.e. for­mula ex­press­ing con­sis­tency] is false”, so I’m guess­ing this proof won’t work for Peano ar­ith­metic.

• My solu­tion for #12:

Sup­pose for the sake of con­tra­dic­tion that such a for­mula ex­ists. By the di­ag­o­nal lemma ap­plied to , there is some sen­tence such that, prov­ably, . By the sound­ness of our the­ory, in fact . But by the prop­erty for we also have , which means , a con­tra­dic­tion.

This seems to be the “se­man­tic” ver­sion of the the­o­rem, where the prop­erty for is stated out­side the sys­tem. There is also a “syn­tac­tic” ver­sion where the prop­erty for is stated within the sys­tem.

• #1

Let f be such a sur­jec­tion. Con­struct a mem­ber of P(S) out­side f’s image by differ­ing from each f(x) in whether it con­tains x.

#2

A nonempty set has func­tions with­out a fixed point iff it has at least two el­e­ments. It suffices to show that there is no sur­jec­tion from S to S → 2, which is analo­gous to #1.

#3

T has only one el­e­ment. Use that one.

source = “main = putStrLn (\”source = \” ++ show source ++ \”\\n\” ++ source)”
main = putStrLn (“source = ” ++ show source ++ “\n” ++ source)

Is #8 sup­posed to read “Write a pro­gram that takes a func­tion f tak­ing a string as in­put as in­put, and pro­duces its out­put by ap­ply­ing f to its source code. For ex­am­ple, if f re­verses the given string, then the pro­gram should out­puts its source code back­wards.”?

If so, here.

source = “onme = putStrLn $f$ \”source = \” ++ show source ++ \”\\n\” ++ source”
onme f = putStrLn $f$ “source = ” ++ show source ++ “\n” ++ source

• Ex 1

Ex­er­cise 1: Let and let . Sup­pose that , then let be an el­e­ment such that . Then by defi­ni­tion, and . So , a con­tra­dic­tion. Hence , so that is not sur­jec­tive.

Ex 2

Ex­er­cise 2: Since is nonempty, it con­tains at least one el­e­ment . Let be a func­tion with­out a fixed point, then , so that and are two differ­ent el­e­ments in (this is the only thing we shall use the func­tion for).

Let for nonempty. Sup­pose by con­tra­dic­tion that is sur­jec­tive. Define a map by the rule . Given any sub­set , let be given by Since is sur­jec­tive, we find a such that . Then . This proves that is sur­jec­tive, which con­tra­dicts the re­sult from (a).

Ex 3

Ex­er­cise 3: By (2) we know that , and so and where . That means for any . and .

• At­tempted solu­tion and some thoughts on #9:

Define a for­mula tak­ing one free vari­able to be .

Now define to be . By the defi­ni­tion of we have .

We have

The first step fol­lows by the defi­ni­tion of , the sec­ond by the defi­ni­tion of , the third by the defi­ni­tion of , and the fourth by the prop­erty of men­tioned above. Since by the type sig­na­ture of , this com­pletes the proof.

It’s a lit­tle un­clear to me what the no­ta­tion means. In par­tic­u­lar, I’ve as­sumed that takes as in­puts Gödel num­bers of for­mu­las rather than the for­mu­las them­selves. If takes as in­puts the for­mu­las them­selves, then I don’t think we can as­sume that the for­mula ex­ists with­out do­ing more ar­ith­me­ti­za­tion work (i.e. the equiv­a­lent of would need to know how to con­vert from the Gödel num­ber of a for­mula to the for­mula it­self).

If the bi­con­di­tional “” is a con­nec­tive in the logic it­self, then I think the same proof works but we would need to as­sume more about than is given in the prob­lem state­ment, namely that the the­ory we have can prove the sub­sti­tu­tion prop­erty of .

The as­sump­tion about the quan­tifier com­plex­ity of and was barely used. It was just given to us in the type sig­na­ture for , and the same proof would have worked with­out this as­sump­tion, so I am con­fused about why the prob­lem in­cludes this as­sump­tion.

• Here’s the proof from the pa­per again:

=s2A < px0,0..p9x0> xx0x0x0x0x0e0..6y0e0x0e0x0e0x0e0e0e0x0e0e0x0e0e0x0.x0e0x0e0e0x0e0e0e0x0e0.x0e0bx<x0e0e0x0e0e0e0e0x0e0.x0e0e0.e0e0.x0e0e0e0e0..2e0e0.x0e0e0e0e0).

So, a proof can’t be “s2A” or “s2B” or “s2A” or “s2B” or “s2B” or “s2C” or “wor­lds” or “pos­si­ble wor­lds” or “no known world”. But it might well be that the proof is cor­rect enough given the premises.

So we as­sume the proof is cor­rect!

• Q7 (Python):

Y = lambda s: eval(s)(s)
Y(‘lambda s: print(“Y = lambda s: eval(s)(s)\\nY({s!r})”)’)

Q8 (Python):

Not sure about the in­ter­pre­ta­tion of this one. Here’s a way to have it work for any fixed (python func­tion) f:

f = ‘lambda s: “\\n”.join(s.splitlines()[::-1])’

go = ‘lambda s: print(eval(f)(eval(s)(s)))’

eval(go)(‘lambda src: f”f = {f!r}\\ngo = {go!r}\\neval(go)({src!r})”’)

• I am con­fused by the in­tro­duc­tory state­ment for #9. Is this an ac­cu­rate rephras­ing?

By rep­re­sent­ing syn­tax us­ing ar­ith­metic, it is pos­si­ble to define a func­tion as fol­lows:

Define with image in , such that:
sub­sti­tutes the Goedel-num­ber of into (cre­at­ing ) and then sub­sti­tutes the Goedel-num­ber of into some fixed for­mula to get a re­sult in .

Given the way is defined, it’s un­clear to me how we en­sure type cor­rect­ness of . In what sense is a set of sen­tences (rather than a set of pairs of sen­tences)? What does an el­e­ment of that set look like?

• Yeah, it is just func­tions that take in two sen­tences and put both their Godel num­bers into a fixed for­mula (with 2 in­puts).

• Ex 1.

Sup­pose there is a sur­jec­tion f : S → P(S). Con­sider the set . Since f is a sur­jec­tion, X = f(y) for some y in S. Does y lie in X? If , then , so by defi­ni­tion of X, . If , then , so y must be­long to X. Con­tra­dic­tion.

Ex 2.

Since there is a func­tion with­out fixed points, T must have at least two el­e­ments. Hence, there is a sur­jec­tion , which in­duces a sur­jec­tion (a func­tion goes to ). So, if there were a sur­jec­tion , there would also be a sur­jec­tion , which can­not be by pre­vi­ous ex­er­cise.

Ex 4.

Sup­pose is a com­putable sur­jec­tive func­tion. Con­sider the func­tion defined by . The func­tion g is com­putable, there­fore there should ex­ist an : .

Then . Con­tra­dic­tion.

Ex 5.

Sup­pose halt(x,y) is a com­putable func­tion. Con­sider the func­tion : ; T if

Sup­pose is a Tur­ing code of f. Since f halts ev­ery­where, halt(s’, s’) = T. But then . Con­tra­dic­tion.

Ex 6.

Sup­pose that is a con­tin­u­ous sur­jec­tion. Con­sider the func­tion (here—f(x, x) is a point di­a­met­ri­cally op­posed to f(x, x)). f is sur­jec­tive, hence g = f(y), but then g(y) = f(y,y) = - f(y,y). Con­tra­dic­tion.

Ex 7. A quine in python3:

code = “”“code = {}{}{}{}{}{}{}
print(code.for­mat(‘”’,‘”’,‘”’,code,‘”’,‘”’,‘”’))”””
print(code.for­mat(‘”’,‘”’,‘”’,code,‘”’,‘”’,‘”’))

Ex 8. In python:

im­port in­spect­
def f(string):
re­turn string[::-1]
def ap­ply­to­self(f):
source = in­spect.get­source(f)
re­turn f(source)
ap­ply­to­self(f)

‘\n]1-::[gnirts nruter \n:)gnirts(f fed’

Ex 9.

The for­mula for is

Ex 11.

Sup­pose is the for­mula . By the di­ag­o­nal lemma, there ex­ists a for­mula A such that .

There­fore,

By prop­erty c,

Again by prop­erty c,

Com­bin­ing pre­vi­ous two im­pli­ca­tions,

Since , we have

Com­bin­ing this with , we get

From this we get , there­fore, and . QED.

• Don’t know if this is still rele­vant, but on Ex9

you definitely can’t define this way. Your defi­ni­tion in­cludes the godel nu­meral for , which makes the defi­ni­tion de­pend on it­self.

• Self-refer­en­tial defi­ni­tions can be con­structed with the di­ag­o­nal lemma. Given that the point of the ex­er­cise is to show some­thing similar, you’re right that this solu­tion is prob­a­bly a bit sus­pect.

• I might be wrong, but I be­lieve this is not cor­rect. The di­ag­o­nal lemma lets you con­struct a sen­tence that is log­i­cally equiv­a­lent to some­thing in­clud­ing its own godel nu­meral. This is differ­ent from hav­ing its own godel nu­meral be part of the syn­tac­tic defi­ni­tion.

In par­tic­u­lar, the former isn’t re­cur­sive. It defines one sen­tence and then, once that sen­tence is defined, proves some­thing about a sec­ond sen­tence which in­cludes the godel nu­meral of the first. But what seed at­tempted (un­less I mi­s­un­der­stood it) was to use the godel nu­meral in the syn­tac­tic defi­ni­tion for , which doesn’t make sense be­cause is not defined un­til is.

• Minor cor­rec­tion for #7: You prob­a­bly want to say “nonempty quine” or “non­triv­ial quine”. The triv­ial quine works in many lan­guages.

• My non­triv­ial an­swer for Q7, in Python:

with open(“foo.py”, “r”) as foo:

And for Q8:

def f(string):
re­turn ″.join([chr(ord(c)+1) for c in string])

with open(“foo.py”, “r”) as foo:

• Ex8

This was rea­son­ably straight-for­ward given the quine.

def apply(f):
l = chr(123) # opening curly bracket
r = chr(125) # closing curly bracket
q = chr(39) # single quotation mark
n = chr(10) # linebreak
z = [n+"    ", l+f"z[i]"+r+q+n+"        + f"+q]
x = [n+"        ", l+f"x[i]"+r]
e = [q, l+"e[i]"+r+q+")"+n+"    print(f(sourcecode))"]
sourcecode = ""
for i in range(0,2):
sourcecode += (f'def apply(f):{z[i]}'
+ f'l = chr(123) # opening curly bracket{z[i]}'
+ f'r = chr(125) # closing curly bracket{z[i]}'
+ f'q = chr(39) # single quotation mark{z[i]}'
+ f'n = chr(10) # linebreak{z[i]}'
+ f'z = [n+"    ", l+f"z[i]"+r+q+n+"        + f"+q]{z[i]}'
+ f'x = [n+"        ", l+f"x[i]"+r]{z[i]}'
+ f'e = [q, l+"e[i]"+r+q+")"+n+"    print(f(sourcecode))"]{z[i]}'
+ f'sourcecode = ""{z[i]}'
+ f'for i in range(0,2):{x[i]}sourcecode += (f{e[i]}')
print(f(sourcecode))

• Last time, I got to Ex7. This time, I de­cided to do them all again be­fore con­tin­u­ing.

Com­ment on Ex1-6

It gets easy if you just write down what prop­erty you want to have in first-or­der logic.

For ex­am­ple, for Ex1 you want a set that does the fol­low­ing:

now if we con­sider a set as a func­tion that takes an el­e­ment and re­turns true or false, this becomes

How do you get such a ? You can just choose , then

and this is done by defin­ing , i.e., which is pre­cisely the solu­tion. This al­most im­me­di­ately an­swers Ex 1,2,4 and it mostly an­swers Ex6.

Another quine for Ex7, this time in python:

l = chr(123) # opening curly bracket
r = chr(125) # closing curly bracket
q = chr(39) # single quotation mark
t = chr(9) # tab
n = chr(10) # linebreak
z = [n, l+f"z[i]"+r+q+n+t+"+ f"+q]
x = [n+t, l+f"x[i]"+r]
e = [q, l+"e[i]"+r+q+", end="+q+q+")"]
for i in range(0,2):
print(f'l = chr(123) # opening curly bracket{z[i]}'
+ f'r = chr(125) # closing curly bracket{z[i]}'
+ f'q = chr(39) # single quotation mark{z[i]}'
+ f't = chr(9) # tab{z[i]}'
+ f'n = chr(10) # linebreak{z[i]}'
+ f'z = [n, l+f"z[i]"+r+q+n+t+"+ f"+q]{z[i]}'
+ f'x = [n+t, l+f"x[i]"+r]{z[i]}'
+ f'e = [q, l+"e[i]"+r+q+", end="+q+q+")"]{z[i]}'
+ f'for i in range(0,2):{x[i]}print(f{e[i]}', end='')