User:IssaRice/Computability and logic/Diagonalization lemma (Yanofsky method)

This page is just a rewritten version of the proof of the diagonalization lemma from Yanofsky's paper. There are some parts I found difficult to understand/gaps that I thought should be filled, so this version will hopefully be much more complete.

Theorem statement and proof

Theorem (Diagonalization lemma). Let $T$ be some nice theory (I don't remember the exact conditions, but Peano Arithmetic or Robinson Arithmetic would work). For any single-place formula $\mathcal{E}(x)$ with $x$ as its only free variable, there exists a sentence (closed formula) $\mathcal{C}$ such that $T⊢\mathcal{C}\leftrightarrow \mathcal{E}(⌜\mathcal{C}⌝)$.

Proof. We will use what's called the wikipedia:Lindenbaum–Tarski algebra in our proof, which the Yanofsky paper just calls Lindenbaum classes. The idea is to define an equivalence an equivalence relation on formulas, so that $A\sim B$ iff our theory $T$ can prove that $A$ and $B$ are logically equivalent. In other words, we define $A\sim B$ iff $T⊢A\leftrightarrow B$. This is easily verified to be an equivalence relation. One twist is that it doesn't make sense to compare two formulas with differing arity. For instance, what does it even mean to say "2+2=5" and "x+5=7" are or are not provably equivalent? For this reason, we make a separate equivalence relation for each arity, and so we end up with separate quotients for each arity. For $i=0,1,2,\dots$, we let ${\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^i$ be the set of Lindenbaum classes of formulas with $i$ free variables.

That means that e.g. each element of ${\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^0$ is not a sentence, but rather a set of sentences that are all provably equivalent. But every sentence is either true or false, so doesn't this mean ${\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^0$ has just two element, $[\mathrm{\top }{]}_{\sim }$ and $[\mathrm{\perp }{]}_{\sim }$ (i.e. the class of true sentences and the class of false sentences)? No! That's because even if two sentences are both true, our theory may be unable to prove that it is so! That's the whole point of Gödel's first incompleteness theorem, which shows us that there can be true sentences (such as the famous "I am not provable" sentence $G$) which are not provable (so that even though $G$ is true, $G\notin [2+2=5{]}_{\sim }$).

In the paper, Yanofsky toggles fluidly between thinking of a formula like $\mathcal{B}(x)$ as a formula vs a set of formulas whose representative is $\mathcal{B}(x)$ (i.e. the class $[\mathcal{B}(x){]}_{\sim }$). To avoid confusion, we will take care to always denote sets of formulas using the equivalence class notation $[-{]}_{\sim }$.

Now following the paper, we define a function $f:{\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^1\times {\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^1\to {\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^0$ as follows:

$f([\mathcal{B}(x){]}_{\sim },[\mathcal{H}(y){]}_{\sim }):=[\mathcal{H}(⌜\mathcal{B}(x)⌝){]}_{\sim }$

This is just the act of substituting the Gödel number of first formula into the second formula. Notice a problem here! Since we have defined the function on the Lindenbaum classes rather than the bare set of formulas themselves, we must check that the result is not dependent on the choice of representatives. For $\mathcal{H}(y)$ we are good, because if we picked some provably equivalent $\mathcal{H}\text{'}(y)$ instead, the results $\mathcal{H}(⌜\mathcal{B}(x)⌝)$ and $\mathcal{H}\text{'}(⌜\mathcal{B}(x)⌝)$ are provably equivalent, so the two classes will be equal. But what about the choice of $\mathcal{B}(x)$? Since $\mathcal{H}(y)$ could be literally any one-place formula at all, and different choices of representatives $\mathcal{B}(x)$ will produce different Gödel numbers, substituting in these different Gödel numbers could produce totally different sentences. Imagine $\mathcal{B}(x)$ has Gödel number 2 and $\mathcal{B}\text{'}(x)$ is provably equivalent to $\mathcal{B}(x)$ and has Gödel number 11. If $\mathcal{H}(y)$ is a sentence like "x+5=7", then this will give two sentences "2+5=7" and "11+5=7", which are not provably equivalent!

So the function $f$ given above is not well-defined. To get around this problem, we can say that whenever we need to make a choice of formula from an equivalence class, we always pick the one with the smallest Gödel number. Now no matter which representative $\mathcal{B}(x)$ we choose, there will be a further step of standardizing on which Gödel number to use, so the function ends up well-defined. Picking the smallest Gödel number is well-defined by the wikipedia:well-ordering principle. So our new definition of $f$ looks like this:

$f([\mathcal{B}(x){]}_{\sim },[\mathcal{H}(y){]}_{\sim }):=[\mathcal{H}(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(x){]}_{\sim }\}){]}_{\sim }$

Now each single-place formula $\mathcal{E}(x)$ induces a mapping ${\mathrm{\Phi }}_{\mathcal{E}}:{\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^0\to {\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^0$ by $\mathcal{[}\mathcal{P}{]}_{\sim }\mapsto \mathcal{[}\mathcal{E}(min\{⌜\phi ⌝:\phi \in [\mathcal{P}{]}_{\sim }\}){]}_{\sim }$. We again have to standardize by taking the smallest Gödel number in the class in order to ensure the mapping is well-defined.

Drawing on Theorem 3 (diagonal theorem) earlier in the paper, we want to perform the familiar construction to get the function $g$.

We define $g([\mathcal{B}(x){]}_{\sim }):={\mathrm{\Phi }}_{\mathcal{E}}(f([\mathcal{B}(x){]}_{\sim },[\mathcal{B}(x){]}_{\sim }))$ as in the paper. Since $f([\mathcal{B}(x){]}_{\sim },[\mathcal{B}(x){]}_{\sim })=[\mathcal{B}(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(x){]}_{\sim }\}){]}_{\sim }$ this means we have ${\mathrm{\Phi }}_{\mathcal{E}}([\mathcal{B}(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(x){]}_{\sim }\}){]}_{\sim })$ by replacing inside ${\mathrm{\Phi }}_{\mathcal{E}}(-)$. And now expanding the definition of ${\mathrm{\Phi }}_{\mathcal{E}}$ we get $\mathcal{[}\mathcal{E}(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(x){]}_{\sim }\}){]}_{\sim }\}){]}_{\sim }$. That is definitely way more complicated-looking than the $\mathcal{E}(⌜\mathcal{B}(⌜\mathcal{B}(x)⌝)⌝)$ that Yanofsky gets at this point in the paper! But it also ensures everything is well-defined.

To get the proof to work, we must show $g$ is representable. Recall that this means we must find some $G(x)\in {\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^1$ such that $g(-)=f(-,G(x))$. How do we figure out which G(x) works? It's a lot easier to work informally by eliding the distinction between formulas and equivalence classes of formulas, so let's be a bit loose and be in "exploration mode" here, then we will come back later and phrase things formally.

well, we want to choose G(x) such that g(B(x)) = f(B(x), G(x)) for every B(x). Let's try to expand both LHS and RHS separately, and see where we get.

g(B(x)) = \Phi_E(f(B(x), B(x))) = E(B(B(x)))

and f(B(x), G(x)) = G(B(x))

so this means we need E(B(B(x))) = G(B(x)). So G just needs to diagonalize B(x) and then wrap it around E: G(x) = E(D(x)).

Formally, we define $G(x)$ to be $E(D(x))$ as well.

Now to really show that g is representable, we must show that $g([B(x){]}_{\sim })=f([B(x){]}_{\sim },[G(x){]}_{\sim })$.

We have $g([B(x){]}_{\sim })=\mathcal{[}\mathcal{E}(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(x){]}_{\sim }\}){]}_{\sim }\}){]}_{\sim }$

and $f([B(x){]}_{\sim },[G(x){]}_{\sim })=[\mathcal{G}(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(x){]}_{\sim }\}){]}_{\sim }$

expanding the definition of G, we get $[\mathcal{E}(D(min\{⌜\phi ⌝:\phi \in [\mathcal{B}(x){]}_{\sim }\})){]}_{\sim }$.

Now by definition of D, we get $[\mathcal{E}(?(⌜min\{⌜\phi ⌝:\phi \in [\mathcal{B}(x){]}_{\sim }\}⌝)){]}_{\sim }$.

[TODO] Here we need to explain what D(x) means and why it's valid.

[TODO] another thing we ought to discuss in the proof: since we are looking for a fixed point for any Lind^0 -> Lind^0, that fixes what the set Y could be. But it doesn't decide what the set T could be. How do we know that T=Lind^1?

Acknowledgments

Thanks to Rupert McCallum for helping me work through the proof.

See also

• User:IssaRice/Computability_and_logic/Diagonalization_lemma