🙣🙜 Or 🙞🙡
How I Learned to Stop Worrying
and Love this Sentence
2021-11-21
Gödel’s fixed point lemma, also known as the Diagonal lemma, is one of those lemmas. Mathematicians are weird in that we classify results in a very unusual way — and most of this is tacit but here goes: \(\renewcommand\iff\leftrightarrow\)
Lemmas are, thus, the workhorse of the working
mathematician; and the Diagonal lemma is no exception, in fact Gödel’s
first incompleteness theorem is basically a corollary (see above) of
that lemma.
What really is the diagonal lemma about? Funny question to ask before we actually even start talking about it; although we have just started talking about it, so the the argument doesn’t apply.
Mathematics is a formal system, a mathematical formula is a sequence of symbols all of which have some function. Formulas live in what we call languages, which are formal specifications of word formation rules. Much like a sentence might not be an English sentence but be a Portuguese sentence, formulas can belong to different languages.
For instance, there is a language of arithmetic; that language has terms which are thigns like \(x+y\) , etc. and it has atomic formulas \(a < b\) and \(l = r\) ; and it has complex formulas like \[ \forall x:\exists z: x+z = 0 \]
When we interpret a formula in an environment, we assign meaning to each of the symbols and operate with them. Now, sometimes we want to say something that is self referential, such as \[ x \ \text{is an ordinal iff}\ x \ \text{is transitive and}\ \forall y\in x: y \ \text{is an ordinal} \] or “this sentence is false”. But how exactly would you go about writting a sentence that refers to itself? Gödel’s fixed point lemma comes to our rescue through indirection.
A Gödelization, or Gödel numbering is an meta-theoretical algorithm for transforming a given formula into a term of formal arithmetic. An even more technical result (Kleene, S. C. “Introduction to Metamathematics” Theorem §49.27) states that any partial recursive function are representable; that is, for any partial recursive metamathematical \(n\) -ary function \(f\) there is a \((n+1)\) -ary formula \(\phi\) such that for any numerals \(x_1\cdots x_n\) , \[ \vdash f(x_1\cdots x_n) = y \iff \phi(y,x_1\cdots x_n) \] notice those \(x_1\cdots x_n\) aren’t variables, they are numerals we picked from the start, and that “ \(f(...)\) ” is a number we computed. The only real variable here is \(y\) .
The Gödelization of a sentence is, then, the term corresponding to \(1+1+\cdots+1\) that is equal to the number we got from whatever algorithm we chose to transform formulas into numbers. \(\newcommand\quote[1]{\text“#1\text”}\) We write that term as \(\quote\phi\) .
The lemma states that for any formula \(\psi(x)\) with one free variable \(x\) ; there is a sentence \(\phi\) such that \[ \vdash \phi \iff \psi(\quote\phi) \]
But who cares? Think about it: if we can code formulas as numbers, we can code (certain) properties of formulas as numerical sentences like \(x\leq y\) , etc. So really, if \(\phi\) is something insteresting like “the formula \(x\) is not provable from the axioms of arithmetic” then we have found a sentence \(\phi\) which is logically equivalent to “ \(\phi\) provable from the axioms of arithmetic”. In fact given any formulaic property, the lemma assures that there is a formula which hold exactly if it has the property.
If \(k\) is metatheoretical numeral, we can denote by \(\mathbf m\) the term \(1+\cdots+1\) \(m\) times. One may define a partial recursive function \(\sigma(\quote{\phi(x)},m)\) which takes \(\quote{\phi(x)}\) to the number \(\quote{\phi(\mathbf m)}\) . Depending on what is the Gödel numbering we chose this might be straightforward or not, but it’s always painful.
This function is represented by a particular formula \(\Sigma(x,y)\) ; then we let \[\alpha(x) \equiv \exists y:\Sigma(y, x, x) \land \psi(y)\] and then let \[\phi\equiv\alpha(\quote\alpha)\] \[\begin{aligned} \phi &\iff \alpha(\quote{\alpha(x)})\\ &\iff \exists y: \Sigma(y, \quote{\alpha(x)}, \quote{\alpha(x)}) \land \psi(y)\\ &\iff \exists y: y = \sigma(\quote{\alpha(x)},\quote{\alpha(x)}) \land\psi(y)\\ &\iff \exists y: y = \quote{\alpha(\quote{\alpha(x)})}\land \psi(y)\\ &\quad\quad\;\text{ since substitution is defined on those entries, }\\ &\iff y = \quote{\alpha(\quote{\alpha(x)})}\land \psi(y)\\ &\iff \psi(\quote{\alpha(\quote{\alpha(x)})})\\ &\quad\quad\;\text{ now considering that $\quote\phi$ equals $\quote{\alpha(\quote{\alpha(x)})}$ , }\\ &\iff \psi(\quote\phi)\\ \end{aligned}\]And so it’s been proven that \(\phi\iff\psi(\quote\phi)\) as desired.
If one is able to define a formula \(\mathfrak P\) such that \[ (\vdash \mathfrak P(\quote\psi)) \Leftrightarrow (\vdash \psi) \] then applying the lemma on the formula \(\neg\mathfrak P\) yields a sentence \(\phi\) such that \[ \vdash \phi\iff\neg\mathfrak P(\quote\phi) \] So if \(\vdash \phi\) then \(\vdash \neg\mathfrak P(\quote\phi)\) which we know to be equivalent to \(\not\vdash\phi\) , which cannot be. Conversely, if \(\vdash\neg\phi\) then \(\vdash\mathfrak P(\quote\phi)\) ; which we know to be equivalent to \(\vdash\phi\) , leading us to another contradiction.
If the theory is consistent, then we must conclude that \(\not\vdash\phi\) and \(\not\vdash\neg\phi\) .