Today we’re going to follow Hinman’s proof of Tarski’s theorem. The proof is by contradiction, and employs diagonalization. First, assuming clauses (i)-(iii) on definability, a universal -section for the class of -definable sets is established and it’s diagonal is shown to not be definable over .
A -section is a set defined for any set and any relation such that for each , . is universal for a class if, and only if, every member of the class is a -section. The diagonal set of is .
Second, assuming the definability of , there is a formula such that for all , . But since the function is effectively computable, it is definable and so, , for some . But this means that,
which means that is definable. This is a contradiction. So, is not definable and not effectively countable. Nor is effectively countable.
In the next update (probably on a plane!) I’ll discuss this theorem and get into Hellman’s example.