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 \mathsf{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 \mathsf{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 \mathsf{ACA_0} one can define the classes of consistent, closed under deduction, and complete theories.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: