Math 557 Nov 14
Gödelization
We can code formulas of the language of \(\mathsf{PA}^-\) as natural numbers, the so-called Gödel numbers. They let us express syntactical properties of arithmetic formulas as number-theoretic properties in the language of arithmetic. This will be important for the self-referential argument at the heart of the first incompleteness theorem. Below, “term” and “formula” always refer to the language \(\mathcal{L} = \{0,1,+,*, <\}\).
Gödel numbers
Using primitive recursion, we assign every term \(t\) a Gödel-Nummer \(\ulcorner t \urcorner\):
\[ \begin{aligned} \ulcorner 0 \urcorner \; \; &= \; \; 1\\ \ulcorner 1 \urcorner \; \; &= \; \; 3\\ \ulcorner v_i \urcorner \; \; &= \; \; 3^2 \cdot 5^i\\ \ulcorner s+t \urcorner \; \; &= \; \; 3^3 \cdot 5^{\ulcorner s \urcorner} \cdot 7^{\ulcorner t \urcorner}\\ \ulcorner s \cdot t \urcorner \; \; &= \; \; 3^4 \cdot 5^{\ulcorner s \urcorner} \cdot 7^{\ulcorner t \urcorner} \end{aligned} \]
Using the Gödel numbers of terms, we can again recursively assign each formula \(\varphi\) a Gödel number \(\ulcorner \varphi \urcorner\):
\[ \begin{aligned} \ulcorner s=t \urcorner \; \; &= \; \; 2 \cdot 5^{\ulcorner s \urcorner} \cdot 7^{\ulcorner t \urcorner}\\ \ulcorner s<t \urcorner \; \; &= \; \; 2 \cdot 3 \cdot 5^{\ulcorner s \urcorner} \cdot 7^{\ulcorner t \urcorner}\\ \ulcorner \neg \varphi \urcorner \; \; &= \; \; 2 \cdot 3^2 \cdot 5^{\ulcorner s \urcorner} \\ \ulcorner (\varphi \land \psi \urcorner) \; \; &= \; \; 2 \cdot 3^3 \cdot 5^{\ulcorner \varphi \urcorner} \cdot 7^{\ulcorner \psi \urcorner}\\ \ulcorner \exists v_i \varphi \urcorner \; \; &= \; \; 2 \cdot 3^4 \cdot 5^i \cdot 7^{\ulcorner \varphi \urcorner}\\ \end{aligned} \]
There are, of course, other coding schemes for formulas that work equally well. The crucial property of any suitable numbering is that we are able to effectively recognize Gödel numbers of basic syntactical objects.
Computability of syntactic properties
Based on the simple recursive definition of \(\ulcorner . \urcorner\), we have
We can appeal to the Church-Turing Thesis to prove this (you should think of informal algorithms to compute these sets). To show the sets are actually primitive recursive, you can use recursion and bounded search - the Gödel numbers of subformulas (subterms) are smaller than the Gödel number of the overall formula (term). Work by induction on height – show that the properties for all formulas (terms) of a fixed height are primitive recursive. Finally, note that the height is always bounded by the length of a formula (term). We leave the details as an exercise.
We can also show that the set of Gödel numbers of logical axioms is primitive recursive. This is relatively straightforward for the equality and quantifier axioms, as these are defined according to a syntactic scheme. The set of tautologies is a little trickier, since this is defined semantically.
Given a finite sequence of Gödel numbers of formulas,
\[ \ulcorner \varphi_1 \urcorner, \dots, \ulcorner \varphi_n \urcorner \]
we can use the usual sequence coding to code this as a single number denoted as
\[ \langle \ulcorner \varphi_1 \urcorner, \dots, \ulcorner \varphi_n \urcorner \rangle. \]
Proof (sketch). Given \((x,y)\), one first checks if \(x\) is the Gödel number of a formula \(\psi\). If yes, it suffices to decode and to test whether all components of \(y\) are Gödel numbers of formulas \(\varphi_i\), the last one being equal to \(\psi\), and whether for every \(i\), either \(\varphi_i\) is a logical axiom (which is primitive recursive by Theorem 1) or whether it can be obtained using deduction rules from previous formulas.
Decidable theories
Recall that given a theory \(T\), its deductive closure is defined as \[ T^\vdash = \{ \sigma : T \vdash \sigma \}. \]
For any set of formulas \(S\), let \[ \ulcorner S \urcorner = \{ \ulcorner \varphi \urcorner : \varphi \in S \}. \]
Similarly to Lemma 1, one can show
Proof. Let \(\widetilde{T}\) be a recursive theory such that \((\widetilde{T})^\vdash = T^\vdash\). We have \(\varphi \in T^\vdash\) if and only if \(\varphi\) is a sentence and there exists a proof of \(\varphi\) in \(\widetilde{T}\). Hence, by Proposition 1 and Lemma 2, \(\varphi \in T^\vdash\) can be expressed via an existential quantifier over a recursive property, which implies it is recursively enumerable.
Proof. Since by Theorem 2, \(\ulcorner T^\vdash \urcorner\) is r.e., it suffices to show that \(\mathbb{N} \setminus \ulcorner T^\vdash \urcorner\) is r.e.
Since \(T\) is complete, \(\mathbb{N} \setminus \ulcorner T^\vdash \urcorner\) is the union of \(A= \{ \ulcorner \varphi \urcorner : \neg \varphi \in T^\vdash\}\) and \(B= \{ x : x \text{ is not the Gödel number of a sentence} \}\). \(B\) is primitive recursive, while \(A\) is r.e.: simply enumerate \(\ulcorner T^\vdash \urcorner\), and whenever a sentence of the form \(\neg \varphi\) is listed, enumerate \(\varphi\) into \(A\).