So we set out the basic assumptions about definability over that factor into the proof of Tarski’s theorem. Let’s go over each one to get clear on all the definitions.
(i) Every effectively computable function is definable over .
A function is effectively computable if, and only if, there is an effective procedure such that, for any the procedure calculates the value . The claim is that every such function defined on the natural numbers is definable in the standard model.
(ii) Every decidable set is definable over .
A subset is decidable if, and only if, the property defined as is decidable in . And a property defined over a set is decidable in if, and only if, there is an effective (or decision) procedure for deciding, for any whether or not holds. Here the claim is straightforward, every such set of natural numbers is definable in the standard model.
(iii) Every effectively countable set is definable over
Finally, a set is effectively countable if, and only if, is empty or there is an effectively computable function that counts (i.e., is the image of , ). So, what’s being assumed here is that the effectively countable subsets of the natural numbers are definable in the standard model.
Just a few more definitions and we can get into Tarski’s theorem. In the next update I’ll define the set of indices for the theorems of as well as a diagonalization function that will play a role in the proof.