116b- Lecture 9

(Covered by Todor Tsankov)

We proved the $\Sigma_1$-uniformization theorem. This allowed us to introduce the standard notation $\varphi^k_n$ for the $n$-th partial recursive function in $k$ variables (with respect to an enumeration induced by a $\Sigma_1$-uniformization of a universal $(k+1)$-ary $\Sigma_1$ relation), and proved that the halting problem is unsolvable and that there are partial recursive functions without (total) recursive extensions. A corollary of this (that separation of r.e. sets by recursive sets fails) is part of this week’s homework.

We then reviewed the axioms of ${\sf ACA}_0$ and began to work towards proving that this theory is powerful enough to prove the basic theorems of logic.  Specifically, we showed that given a set coding a countable language, in ${\sf ACA_0}$ one can prove that the set of formulas of the language exists, and the same holds for the sets of sentences or logical axioms. Using this, one can define a provability predicate that states of a set $X$ and a number $n$ that $X$ is a (not necessarily r.e.) set of sentences in the given language, and $n$ codes the Gödel number of a sentence provable from $X$. Hence, in ${\sf ACA_0}$ one can define the classes of consistent, closed under deduction, and complete theories.