User:IssaRice/Computability and logic/Diagonalization lemma

The diagonalization lemma, also called the Gödel–Carnap fixed point theorem, is a fixed point theorem in logic.

A verbal version of this result, modified from GEB (p. 449), runs as follows: Take the predicate cannot-be-proved-when-diagonalized(x). This takes a predicate in the x input, and says whether the sentence can be proved when diagonalized (i.e. inserted into itself). For instance, cannot-be-proved-when-diagonalized("has-length-less-than-one-thousand(x)") claims that has-length-less-than-one-thousand("has-length-less-than-one-thousand(x)") cannot be proved. In this case, let's say it's false, since we can see that the string "has-length-less-than-one-thousand(x)" has length less than 1000, and let's assume our proof system is strong enough to prove this. Now, to diagonalize cannot-be-proved-when-diagonalized(x) is to form the sentence cannot-be-proved-when-diagonalized("cannot-be-proved-when-diagonalized(x)"). So can this sentence be proved or not? If it can be proved, then the sentence itself claims that it cannot be proved, a contradiction. So it must not be provable.

Basically, unlike the English language, a sentence can't refer to itself using phrases like "this sentence itself", so there is no straightforward way to make claims like "This sentence cannot be proved". To get around this restriction, we must use diagonalization – substituting a sentence's own encoding (i.e. string representation, aka "Gödel number") into itself. This allows a predicate to talk of its own string representation. So now if that predicate happens to claim unprovability – then we get Gödel's first incompleteness theorem.

The diagonalization lemma generalizes to talk about any predicate P(x), not just not-provable(x). We want to find a sentence G such that G is true if and only if P("G") is (this is a little sloppy -- it's not actually the string "G", but rather if we made whatever G happens to be into a string...). Let G be has-property-P-when-diagonalized("has-property-P-when-diagonalized(x)"). If G is true, then has-property-P-when-diagonalized(x) must have property P when diagonalized, i.e. P("has-property-P-when-diagonalized('has-property-P-when-diagonalized(x)')") which means P("G") is true. If G is false, then has-property-P-when-diagonalized(x) must not have property P when diagonalized, i.e. P("has-property-P-when-diagonalized('has-property-P-when-diagonalized(x)')") is false.

Rogers's fixed point theorem

Let $f$ be a total computable function. Then there exists an index $e$ such that ${\phi }_e\simeq {\phi }_{f(e)}$.

(simplified)

Define $d(x)={\phi }_x(x)$ (this is actually slightly wrong, but it brings out the analogy better).

Consider the function $f\circ d$. This is partial recursive, so $f\circ d\simeq {\phi }_i$ for some index $i$.

Now ${\phi }_{f(d(i))}\simeq {\phi }_{{\phi }_i(i)}$ since $f\circ d\simeq {\phi }_i$. This is equivalent to ${\phi }_{d(i)}$ by definition of $d$. Thus, we may take $e=d(i)$ to complete the proof.

It looks like we have $f(d(i))={\phi }_i(i)=d(i)$, i.e. $f(e)=e$. Is this right?

Repeatedly using the facts that (1) $i$ is an index for $f\circ d$, and (2) $d(i)={\phi }_i(i)$, allows us to create an iteration effect:

${\phi }_i(i)\simeq f(d(i))\simeq f({\phi }_i(i))\simeq f(f(d(i)))\simeq f(f({\phi }_i(i)))\simeq \cdots \simeq f\circ \cdots \circ f\circ d(i)$

(I'm wondering if there's some deeper meaning to this. So far it's just an interesting connection between diagonalization-based fixed points and iteration-based fixed points. I think there might be a connection between this and the fix function in Haskell.)

In the more rigorous/careful version of the proof, we use the s-m-n theorem to get an index of a function, $s$, which is basically like $d$. The difference is that ${\phi }_x(x)$ might not be defined for all $x$ (actually it isn't, since some partial functions are always undefined) so $d$ is not total. On the other hand, $s$ is obtained via the s-m-n theorem so is total. When ${\phi }_x(x)$ is undefined, $s(x)$ gives an index of the always-undefined partial function. So $s$ says "this is undefined" in a defined way. Thanks to this property, the expression ${\phi }_{s(x)}$ always makes sense, whereas ${\phi }_{{\phi }_x(x)}$ sometimes doesn't make sense.

See also https://machinelearning.subwiki.org/wiki/User:IssaRice/Computability_and_logic/Rogers_fixed_point_theorem_using_Sipser%27s_notation

Diagonalization lemma

(semantic version)

Let $A$ be a formula with one free variable. Then there exists a sentence $G$ such that $G$ iff $A(⌜G⌝)$.

Define $\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(x)$ to be $⌜C(⌜C⌝)⌝$ where $x=⌜C⌝$. In other words, given a number $x$, the function $\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}$ finds the formula with that Godel number, then diagonalizes it (i.e. substitutes the Godel number of the formula into the formula itself), then returns the Godel number of the resulting sentence.

Let $B$ be $A(\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(x))$, and let $G$ be $B(⌜B⌝)$.

Then $G$ is $A(\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝))$, by substituting $x=⌜B⌝$ in the definition of $B$.

We also have $\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝)=⌜B(⌜B⌝)⌝$ by definition of $\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}$. By definition of $G$, this is $⌜G⌝$, so we have $\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝)=⌜G⌝$.

To complete the proof, apply $A$ to both sides of the final equality to obtain $A(\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝))$ iff $A(⌜G⌝)$; this simplifies to $G$ iff $A(⌜G⌝)$.

use of extra quantified variable to make a substitution

(see p. 448 of GEB)

outside the formal system, if we have some function f, a constant a, and some one-place relation R, we can substitute f(a) into R like: R(f(a)). but many systems of formal logic don't have a way to directly talk about outputs of functions like f(a). instead, they have a relation like F(a,y) to mean f(a)=y. [why on earth would they do this? i think the basic reason is that if functions are just relations, we have fewer cases to have to prove in those annoying structural induction proofs.] so how do we express an idea like R(f(a))? we can make use of an extra variable to hold the output, e.g. $F(a,y)\wedge R(y)$. but this leaves y free, so actually we want $\mathrm{\exists }y(F(a,y)\wedge R(y))$. alternatively, we can also say $F(a,y)\to R(y)$. in this case we want $\mathrm{\forall }y(F(a,y)\to R(y))$. it's easy to prove that both of these clumsy ways of writing are logically equivalent to R(f(a)).

something similar happens when we want to diagonalize formulas. given a formula $A(x)$ that has just x free, it's easy enough to diagonalize it: $A(⌜A(x)⌝)$. but what about a sentence like $B$? how do we "substitute" in something into something that has no free variable? [why on earth would you want to try that? i think it simplifies the proof a little if we assume diagonalization is defined for any sentence. but i forgot where exactly the simplification occurs.] the idea is again to make use of a separate variable: $\mathrm{\exists }x(x=⌜A(x)⌝\wedge A(x))$. again, i think we could also do $\mathrm{\forall }x(x=⌜A(x)⌝\to A(x))$. we're basically considering a function that finds the godel number of a sentence. except unlike a relation, a single-free-variable formula fixes some specific variable that it leaves free (a relation doesn't know whether it's x or y that's free -- it just expresses some idea), so we need to fix some single variable to use throughout.

Trying to discover the lemma

approach 1

https://mathoverflow.net/a/31374

approach 2

see Owings paper.

In the framework of this paper, we have a matrix where each entry is of a certain type. Then we apply the function $\alpha$ to the diagonal. If the diagonal turns into one of the rows, $\alpha$ has a fixed point.

So now the trick is to figure out what our $\alpha$ should be, and also what our matrix should look like.

Picking the $\alpha$ doesn't seem hard: we want a fixed point for the operation ${\phi }_{f(-)}$, so we can pick $\alpha ({\phi }_e)={\phi }_{f(e)}$. One problem is that this might not be well-defined, but we can just go with this for now (it ends up not mattering, for reasons I don't really understand, but the Owings paper has another workaround, which is to use relations; I find that more confusing).

The matrix that works turns out to have entries ${\phi }_{{\phi }_j(k)}$. I'm not sure how one would have figured this out. One might also think ${\phi }_j(k)$ would work, but notice that then we fail the type checking with $\alpha$ (which takes a function, not a natural number).

So now we take the diagonal, which has entries ${\phi }_{{\phi }_k(k)}$, for $k=0,1,2,\dots$, and apply $\alpha$. We get ${\phi }_{f({\phi }_k(k))}$. But $d$ defined by $d(x)={\phi }_x(x)$ is a recursive function, so the diagonal has turned into ${\phi }_{f(d(k))}={\phi }_{f\circ d(k)}$. Since a composition of recursive functions is itself recursive, $f\circ d$ is recursive. So we have some index $e$ for it, i.e. $f\circ d\simeq {\phi }_e$. So $\alpha$ applied to the diagonal results in ${\phi }_{{\phi }_e(k)}$, which is one of the rows (the $e$th row). This means $\alpha$ has a fixed point, in the $e$th entry, i.e. at ${\phi }_{{\phi }_e(e)}$. So we expect $\alpha ({\phi }_{{\phi }_e(e)})={\phi }_{{\phi }_e(e)}$. Since $\alpha ({\phi }_{{\phi }_e(e)})={\phi }_{f({\phi }_e(e))}$, the "real" fixed point for the operator will be at ${\phi }_e(e)$. Indeed, ${\phi }_{f({\phi }_e(e))}\simeq {\phi }_{f\circ d(e)}\simeq {\phi }_{{\phi }_e(e)}$.

Now we have to verify that $\alpha$ doesn't need to be well-defined.

approach 3

Take Cantor's theorem, generalize it to mention fixed points, then take the contrapositive. See the Yanofsky paper for details.

This version still has some mystery for me, e.g. replacing "the set has at least two elements" with "there is a function from the set to itself without a fixed point". The logical equivalence is easy to see, but getting the idea for rephrasing this condition to mention fixed points is not obvious at all.

The use of the s-m-n theorem also isn't obvious to me. Why use it at all? Why use it on $g$? Why do we care about the index of $s$?

It's also not clear to me why we use $T=\mathbf{N}$ and $Y=\mathcal{F}$. In some sense it does make sense, like the natural numbers are all the algorithms, and the set of computable functions are the "properties" (a.k.a. "the objects being named").

approach 4

http://www.andrew.cmu.edu/user/kk3n/complearn/chapter8.pdf -- see section 8.1

also see Moore and Mertens's section on lambda calculus

in the untyped lambda calculus, there is only one type of entity, namely functions, which can operate on other functions. This makes it easy for functions to operate on themselves, which creates self-reference.

but when working with partial recursive functions, we don't have this. instead, we have numbers and then partial functions that operate on numbers. to get self-reference, we need some kind of encoding. this is why we numbered the partial recursive functions.

but now, one of the familiar facts about the lambda calculus is the existence of the fixed point combinator (aka y combinator). (note: this passes the buck to wondering how one would have come up with the lambda calculus, or how one would come up with the fixed point combinator in that setting; but this seems easier to answer.) since this theorem works in one setting in which we have self-reference, we might wonder if we can "port over" the theorem to the case where we have self-reference in a different setting.

Comparison table

Some things to notice:

• The two theorems are essentially identical, with identical proofs, as seen by the matching rows. The analogy breaks down slightly at the very end, where we apply ${\phi }_{f(\cdot )}$ vs $A(\cdot )$ (the latter corresponds to $f$ until the very end).
• In the partial recursive functions world, it's easy to go from the index (e.g. $e$) to the partial function (${\phi }_e$). In the formulas world it's the reverse, where it's easy to go from a formula (e.g. $A$) to its Godel number $⌜A⌝$). I wonder if there is something essential here, or if it is simply some sort of historical accident in notation.
• For the diagonalization lemma, here we have done the semantic version (? I think...), but usually the manipulations are done inside a formal system with reference to some theory $T$ to derive a syntactic result (i.e. we have some theory that is strong enough to do all these manipulations within the object-level language). For partial recursive functions, as far as I know, there is no analogous distinction between semantics vs syntax.
• The diagonalization part is not completely correct/as strong as possible for both proofs. For the partial recursive functions side, we want to make sure that ${\phi }_{{\phi }_x(x)}$ is actually defined in each case. For the logic side, I think often the diagonalization is defined as $\mathrm{\exists }x(x=⌜A⌝\wedge A)$ so that it is defined for all formulas, not just ones with one free variable. But the essential ideas are all present below, and since this makes the comparison easier, the presentation is simplified.

Step	Rogers's fixed point theorem	Diagonalization lemma
Theorem statement (note: quantifiers are part of the metalanguage)	$(\mathrm{\forall }f\mathrm{\exists }e){\phi }_e\simeq {\phi }_{f(e)}$	$(\mathrm{\forall }A\mathrm{\exists }G)G\leftrightarrow A(⌜G⌝)$
Given mapping	$f$	$A$
Definition of diagonal function	$d(x)={\phi }_x(x)$	$\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜C⌝)=⌜C(⌜C⌝)⌝$
Composition of given mapping with diagonal function ($\mathrm{g}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{n}\circ \mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}\mathrm{o}\mathrm{n}\mathrm{a}\mathrm{l}$)	$f(d(x))$	$A(\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(x))$
Naming the $\mathrm{g}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{n}\circ \mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}\mathrm{o}\mathrm{n}\mathrm{a}\mathrm{l}$ composition	$f\circ d$ (name not given because compositions are easy to express outside a formal language)	$B$
Index of $\mathrm{g}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{n}\circ \mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}\mathrm{o}\mathrm{n}\mathrm{a}\mathrm{l}$ composition	$i$	$⌜B⌝$
Expanding using definition of diagonal	$d(i)={\phi }_i(i)$	$\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝)=⌜B(⌜B⌝)⌝$
The $\mathrm{g}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{n}\circ \mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}\mathrm{o}\mathrm{n}\mathrm{a}\mathrm{l}$ composition applied to own index (i.e. diagonalization of the composition)	$f\circ d(i)$	$B(⌜B⌝)$
G defined	${\phi }_i(i)$ (no equivalent definition)	$G$ is $B(⌜B⌝)$
	$f(d(i))={\phi }_i(i)$	$A(\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝))\leftrightarrow B(⌜B⌝)$
Renaming index	$e=d(i)$	$⌜G⌝=\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝)$
Leibniz law to previous row	Apply ${\phi }_{f(\cdot )}$ to obtain ${\phi }_{f(e)}={\phi }_{f(d(i))}$	Apply $A(\cdot )$ to obtain $A(⌜G⌝)\leftrightarrow A(\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝))$
Use definition of G	${\phi }_{f(e)}={\phi }_{{\phi }_i(i)}={\phi }_e$	$A(⌜G⌝)\leftrightarrow B(⌜B⌝)\leftrightarrow G$
(Definition of G)?	${\phi }_i(i)$ is $f(d(i))$	$G$ is $A(\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(⌜B⌝))$

Quotes

"All of these theorems tend to strain one's intuition; in fact, many people find them almost paradoxical. The most popular proofs of these theorems only serve to aggravate the situation because they are completely unmotivated, seem to depend upon a low combinatorial trick, and are so barbarically short as to be nearly incapable of rational analysis."

"This is just a lovely result, insightful in its concept and far reaching in its consequences. We’d love to say that the proof was also lovely and enlightening, but to be honest, we don’t have an enlightening sort of proof to show you. Sometimes the best way to describe a proof is that the argument sort of picks you up and shakes you until you agree that it does, in fact, establish what it is supposed to establish. That’s what you get here."

"The brevity of the proof does not make for transparency; it has the aura of a magician’s trick. How did Gödel ever come up with the idea? As a matter of fact, Gödel did not come up with that idea."

Questions/things to explain

• In Peter Smith's book, he defines Gdl(m,n) as Prf(m, diag(n)). What is the analogue of Gld for the Rogers fixed point theorem?
• I like the $D(⌜\phi ⌝)⟺\phi (⌜\phi ⌝)$ that begins this answer, but what is the analogue for partial functions? It seems like it is $d(x)={\phi }_x(x)$, which does exist (because we are allowed to have undefined values). So the motivation that works for the logic version doesn't work for the partial functions version, which bugs me.