Diagonalization Fixed Point Exercises

post by Scott Garrabrant, SamEisenstat · 2018-11-18T00:31:19.683Z · LW · GW · 24 comments

Contents

24 comments

This is the second of three sets of fixed point exercises. The first post in this sequence is here [LW · GW], giving context.

  1. Recall Cantor’s diagonal argument for the uncountability of the real numbers. Apply the same technique to convince yourself than for any set , the cardinality of is less than the cardinality of the power set (i.e. there is no surjection from to ).

  2. Suppose that a nonempty set has a function from to which lacks fixed points (i.e. for all ). Convince yourself that there is no surjection from S to , for any nonempty . (We will write the set of functions from to either as or ; these are the same.)

  3. For nonempty and , suppose you are given a surjective function from the set to the set of functions from to , and let be a function from to itself. The previous result implies that there exists an in such that . Can you use your proof to describe in terms of and ?

  4. Given sets and , let denote the space of total computable functions from to . We say that a function from to is computable if and only if the corresponding function (given by is computable. Show that there is no surjective computable function from the set of all strings to .

  5. Show that the previous result implies that there is no computable function from which outputs if and only if the first input is a code for a Turing machine that halts when given the second input.

  6. Given topological spaces and , let be the space with the set of continuous functions from to as its underlying set, and with topology such that is continuous if and only if the corresponding function (given by ) is continuous, assuming such a space exists. Convince yourself that there is no space which continuously surjects onto , where is the circle.

  7. In your preferred programming language, write a quine, that is, a program whose output is a string equal to its own source code.

  8. Write a program that defines a function taking a string as input, and produces its output by applying to its source code. For example, if reverses the given string, then the program should outputs its source code backwards.

  9. Given two sets and of sentences, let be the set of all functions from to defined by substituting the Gödel number of a sentence in into a fixed formula. Let be the set of all sentences in the language of arithmetic with one unbounded universal quantifier and arbitrarily many bounded quantifiers, and let be the set of all formulas with one free variables of that same quantifier complexity. By representing syntax using arithmetic, it is possible to give a function that substitutes its second argument into its first argument. Pick some coding of formulas as natural numbers, where we denote the number coding for a formula as . Using this, show that for any formula , there is a formula such that .

  10. (Gödel's second incompleteness theorem) In the set , there is a formula such that holds iff the sentence is not provable in Peano arithmetic. Using this, show that Peano arithmetic cannot prove its own consistency.

  11. (Löb's theorem) More generally, the diagonal lemma states that for any formula with a single free variable, there is a formula such that, provably, . Now, suppose that Peano arithmetic proves that for some formula . Show that Peano arithmetic also proves itself. Some facts that you may need are that (a) when a sentence is provable, the sentence is itself provable, (b) Peano arithmetic proves this fact, that is, Peano arithmetic proves , for any sentence and (c) Peano arithmetic proves the fact that if and are provable, then is provable.

  12. (Tarski's theorem) Show that there does not exist a formula with one free variable such that for each sentence , the statement holds.

  13. Looking back at all these exercises, think about the relationship between them.


Please use the spoilers feature - the symbol '>' followed by '!' followed by space -in your comments to hide all solutions, partial solutions, and other discussions of the math. The comments will be moderated strictly to hide spoilers!

I recommend putting all the object level points in spoilers and including metadata outside of the spoilers, like so: "I think I've solved problem #5, here's my solution <spoilers>" or "I'd like help with problem #3, here's what I understand <spoilers>" so that people can choose what to read.

24 comments

Comments sorted by top scores.

comment by Adele Lopez (adele-lopez-1) · 2018-11-22T02:21:26.675Z · LW(p) · GW(p)

Ex 8: (in Python, using a reversal function)

def f(s):
return s[::-1]

dlmt = '"""'
code = """def f(s):
return s[::-1]

dlmt = '{}'
code = {}{}{}
code = code.format(dlmt, dlmt, code, dlmt)
print(f(code))"""
code = code.format(dlmt, dlmt, code, dlmt)
print(f(code))

comment by Rafael Harth (sil-ver) · 2018-11-18T23:11:24.616Z · LW(p) · GW(p)

Ex 4

Given a computable function , define a function by the rule . Then is computable, however, because for , we have that and .

Ex 5:

We show the contrapositive: given a function halt, we construct a surjective function from to as follows: enumerate all turing machines, such that each corresponds to a string. Given a , if does not decode to a turing machine, set . If it does, let denote that turning machine. Let with input first run halt; if halt returns , put out , otherwise will halt on input ; run on and put out the result.

Given a computable function , there is a string such that implements (if the turing thesis is true). Then , so that is surjective.

Ex 6:

Let be a parametrization of the circle given by . Given and , write to denote the point , where . First, note that, regardless of the topology on , it holds true that if is continuous, then so is for any , because given a basis element of the circle, we have which is open because is continuous.

Let be a continuous function from to . Then is continuous, and so is the diagonal function . Fix any , then given by is also continuous, but given any , one has and thus . It follows that is not surjective.

Ex 7:

I did it in java. There's probably easier ways to do this, especially in other languages, but it still works. It was incredibly fun to do. My basic idea was to have a loop iterate 2 times, the first time printing the program, the second time printing the printing command. Escaping the " characters is the biggest problem, the main idea here was to have a string q that equals " in the first iteration and " + q + " in the second. That second string (as part of the code in an expression where a string is printed) will print itself in the console output. Code:

package maths;public class Quine{public 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);}}}":"System.out.print(o+";System.out.print(o+"package maths;public class Quine{public 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+"System.out.print(o+"+q+";"+e);}}}

comment by Czynski (JacobKopczynski) · 2018-11-24T01:14:33.979Z · LW(p) · GW(p)

For #6, I have what looks to me like a counterexample. Possibly I am using the wrong definition of continuous function? I am taking this one as my source.

Take as the topological space the real line under the Euclidean topology. Let be the point in at radians rotation. This is surjective; all points in are mapped to infinitely many times. It is also continuous; For every and neighborhood there is a neighborhood such that ,

The partial functions f(x) from are also continuous by the same argument.

Replies from: adele-lopez-1
comment by Adele Lopez (adele-lopez-1) · 2018-11-24T06:25:26.990Z · LW(p) · GW(p)

Currying doesn't preserve surjectivity. As a simple example, you can easily find a surjective function , but there are no surjective functions .

Replies from: JacobKopczynski
comment by Czynski (JacobKopczynski) · 2018-11-24T17:31:23.196Z · LW(p) · GW(p)

Ah, yes, that makes sense. I got distracted by the definition of 's topology

and applied it to surjectivity as well as continuity.

comment by riceissa · 2019-04-14T19:57:38.709Z · LW(p) · GW(p)

Thoughts on #10:

I am confused about this exercise. The standard/modern proof of Gödel's second incompleteness theorem uses the Hilbert–Bernays–Löb derivability conditions, which are stated as (a), (b), (c) in exercise #11. If the exercises are meant to be solved in sequence, this seems to imply that #10 is solvable without using the derivability conditions. I tried doing this for a while without getting anywhere.

Maybe another way to state my confusion is that I'm pretty sure that up to exercise #10, nothing that distinguishes Peano arithmetic from Robinson arithmetic has been introduced (it is only with the introduction of the derivability conditions in #11 that this difference becomes apparent). It looks like there is a version of the second incompleteness theorem for Robinson arithmetic, but the paper says "The proof is by the construction of a nonstandard model in which this formula [i.e. formula expressing consistency] is false", so I'm guessing this proof won't work for Peano arithmetic.

comment by riceissa · 2019-04-14T19:41:46.836Z · LW(p) · GW(p)

My solution for #12:

Suppose for the sake of contradiction that such a formula exists. By the diagonal lemma applied to , there is some sentence such that, provably, . By the soundness of our theory, in fact . But by the property for we also have , which means , a contradiction.

This seems to be the "semantic" version of the theorem, where the property for is stated outside the system. There is also a "syntactic" version where the property for is stated within the system.

comment by Gurkenglas · 2018-11-18T23:36:16.738Z · LW(p) · GW(p)

#1

Let f be such a surjection. Construct a member of P(S) outside f's image by differing from each f(x) in whether it contains x.

#2

A nonempty set has functions without a fixed point iff it has at least two elements. It suffices to show that there is no surjection from S to S -> 2, which is analogous to #1.

#3

T has only one element. Use that one.

#7 Haskell

source = "main = putStrLn (\"source = \" ++ show source ++ \"\\n\" ++ source)"
main = putStrLn ("source = " ++ show source ++ "\n" ++ source)

Is #8 supposed to read "Write a program that takes a function f taking a string as input as input, and produces its output by applying f to its source code. For example, if f reverses the given string, then the program should outputs its source code backwards."?

If so, here.

source = "onme = putStrLn $ f $ \"source = \" ++ show source ++ \"\\n\" ++ source"
onme f = putStrLn $ f $ "source = " ++ show source ++ "\n" ++ source

comment by Rafael Harth (sil-ver) · 2018-11-18T20:57:20.965Z · LW(p) · GW(p)

Ex 1

Exercise 1: Let and let . Suppose that , then let be an element such that . Then by definition, and . So , a contradiction. Hence , so that is not surjective.

Ex 2

Exercise 2: Since is nonempty, it contains at least one element . Let be a function without a fixed point, then , so that and are two different elements in (this is the only thing we shall use the function for).

Let for nonempty. Suppose by contradiction that is surjective. Define a map by the rule . Given any subset , let be given by Since is surjective, we find a such that . Then . This proves that is surjective, which contradicts the result from (a).

Ex 3

Exercise 3: By (2) we know that , and so and where . That means for any . and .

comment by riceissa · 2019-04-01T18:56:07.202Z · LW(p) · GW(p)

Attempted solution and some thoughts on #9:

Define a formula taking one free variable to be .

Now define to be . By the definition of we have .

We have

The first step follows by the definition of , the second by the definition of , the third by the definition of , and the fourth by the property of mentioned above. Since by the type signature of , this completes the proof.

Things I'm not sure about:

It's a little unclear to me what the notation means. In particular, I've assumed that takes as inputs Gödel numbers of formulas rather than the formulas themselves. If takes as inputs the formulas themselves, then I don't think we can assume that the formula exists without doing more arithmetization work (i.e. the equivalent of would need to know how to convert from the Gödel number of a formula to the formula itself).

If the biconditional "" is a connective in the logic itself, then I think the same proof works but we would need to assume more about than is given in the problem statement, namely that the theory we have can prove the substitution property of .

The assumption about the quantifier complexity of and was barely used. It was just given to us in the type signature for , and the same proof would have worked without this assumption, so I am confused about why the problem includes this assumption.

Replies from: GPT2
comment by GPT2 · 2019-04-01T18:56:19.321Z · LW(p) · GW(p)

Here's the proof from the paper 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 "worlds" or "possible worlds" or "no known world". But it might well be that the proof is correct enough given the premises.

So we assume the proof is correct!

comment by James Payor (JamesPayor) · 2018-12-07T10:05:05.603Z · LW(p) · GW(p)

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 interpretation of this one. Here's a way to have it work for any fixed (python function) 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})"')

comment by Czynski (JacobKopczynski) · 2018-11-23T04:47:45.634Z · LW(p) · GW(p)

I am confused by the introductory statement for #9. Is this an accurate rephrasing?

By representing syntax using arithmetic, it is possible to define a function as follows:

Define with image in , such that:
substitutes the Goedel-number of into (creating ) and then substitutes the Goedel-number of into some fixed formula to get a result in .

comment by Vladimir Mikulik (vladimir-mikulik) · 2018-11-21T12:46:05.386Z · LW(p) · GW(p)

I’m confused about Q9.

Given the way is defined, it’s unclear to me how we ensure type correctness of . In what sense is a set of sentences (rather than a set of pairs of sentences)? What does an element of that set look like?

Replies from: Scott Garrabrant
comment by Scott Garrabrant · 2018-11-22T16:06:42.235Z · LW(p) · GW(p)

Yeah, it is just functions that take in two sentences and put both their Godel numbers into a fixed formula (with 2 inputs).

comment by seed · 2019-12-29T16:01:32.747Z · LW(p) · GW(p)

Ex 1.

Suppose there is a surjection f : S -> P(S). Consider the set . Since f is a surjection, X = f(y) for some y in S. Does y lie in X? If , then , so by definition of X, . If , then , so y must belong to X. Contradiction.

Ex 2.

Since there is a function without fixed points, T must have at least two elements. Hence, there is a surjection , which induces a surjection (a function goes to ). So, if there were a surjection , there would also be a surjection , which cannot be by previous exercise.

Ex 4.

Suppose is a computable surjective function. Consider the function defined by . The function g is computable, therefore there should exist an : .

Then . Contradiction.

Ex 5.

Suppose halt(x,y) is a computable function. Consider the function : ; T if

Suppose is a Turing code of f. Since f halts everywhere, halt(s', s') = T. But then . Contradiction.

Ex 6.

Suppose that is a continuous surjection. Consider the function (here - f(x, x) is a point diametrically opposed to f(x, x)). f is surjective, hence g = f(y), but then g(y) = f(y,y) = - f(y,y). Contradiction.

Ex 7. A quine in python3:

code = """code = {}{}{}{}{}{}{}
print(code.format('"','"','"',code,'"','"','"'))"""
print(code.format('"','"','"',code,'"','"','"'))

Ex 8. In python:

import inspect
def f(string):
return string[::-1]
def applytoself(f):
source = inspect.getsource(f)
return f(source)
applytoself(f)

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

Ex 9.

The formula for is

Ex 11.

Suppose is the formula . By the diagonal lemma, there exists a formula A such that .

Therefore,

By property c,

Again by property c,

Combining previous two implications,

Since , we have

Combining this with , we get

From this we get , therefore, and . QED.


Replies from: sil-ver
comment by Rafael Harth (sil-ver) · 2020-10-17T16:25:55.733Z · LW(p) · GW(p)

Don't know if this is still relevant, but on Ex9

you definitely can't define this way. Your definition includes the godel numeral for , which makes the definition depend on itself.

Replies from: mark-xu
comment by Mark Xu (mark-xu) · 2020-10-17T16:56:42.451Z · LW(p) · GW(p)

Self-referential definitions can be constructed with the diagonal lemma. Given that the point of the exercise is to show something similar, you're right that this solution is probably a bit suspect.

Replies from: sil-ver
comment by Rafael Harth (sil-ver) · 2020-10-17T18:24:33.116Z · LW(p) · GW(p)

I might be wrong, but I believe this is not correct. The diagonal lemma lets you construct a sentence that is logically equivalent to something including its own godel numeral. This is different from having its own godel numeral be part of the syntactic definition.

In particular, the former isn't recursive. It defines one sentence and then, once that sentence is defined, proves something about a second sentence which includes the godel numeral of the first. But what seed attempted (unless I misunderstood it) was to use the godel numeral in the syntactic definition for , which doesn't make sense because is not defined until is.

comment by Czynski (JacobKopczynski) · 2018-11-22T22:17:51.248Z · LW(p) · GW(p)

Minor correction for #7: You probably want to say "nonempty quine" or "nontrivial quine". The trivial quine works in many languages.

Replies from: JacobKopczynski
comment by Czynski (JacobKopczynski) · 2018-11-24T18:07:03.841Z · LW(p) · GW(p)

My nontrivial answer for Q7, in Python:

with open("foo.py", "r") as foo:
print foo.read()

And for Q8:

def f(string):
return ''.join([chr(ord(c)+1) for c in string])

with open("foo.py", "r") as foo:
print f(foo.read())

comment by Rafael Harth (sil-ver) · 2020-10-16T16:59:43.733Z · LW(p) · GW(p)

Ex8

This was reasonably straight-forward 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))
comment by Rafael Harth (sil-ver) · 2020-10-16T09:31:02.277Z · LW(p) · GW(p)

Last time, I got to Ex7. This time, I decided to do them all again before continuing.

Comment on Ex1-6

It gets easy if you just write down what property you want to have in first-order logic.

For example, for Ex1 you want a set that does the following:

now if we consider a set as a function that takes an element and returns true or false, this becomes

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

and this is done by defining , i.e., which is precisely the solution. This almost immediately answers Ex 1,2,4 and it mostly answers 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='')
comment by Pi Rogers (pi-rogers) · 2024-01-02T07:06:29.148Z · LW(p) · GW(p)

Solution to 8 implemented in python using zero self-reference, where you can replace f with code for any arbitrary function on string x (escaping characters as necessary):

 f="x+'\\n'+x"
def ff(x):
return eval(f)
(lambda s : print(ff('f='+chr(34)+f+chr(34)+chr(10)+'def ff(x):'+chr(10)+chr(9)+'return eval(f)'+chr(10)+s+'('+chr(34)+s+chr(34)+')')))("(lambda s : print(ff('f='+chr(34)+f+chr(34)+chr(10)+'def ff(x):'+chr(10)+chr(9)+'return eval(f)'+chr(10)+s+'('+chr(34)+s+chr(34)+')')))")

edit: fixed spoiler tags