## Assumptions On Definability Over The Standard Model Ω, Part 2

So we set out the basic assumptions about definability over $\Omega$ 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 $\textup{F}: \omega \rightarrow \omega$ is definable over $\Omega$.

A function $\textup{F}: \textup{X} \rightarrow \textup{Z}$ is effectively computable if, and only if, there is an effective procedure such that, for any $x \in \textup{X}$ the procedure calculates the value $\textup{F}(x)$.  The claim is that every such function defined on the natural numbers is definable in the standard model.

(ii) Every decidable set $\textup{X} \subseteq \omega$ is definable over $\Omega$.

A subset $\textup{A} \subseteq \textup{X}$ is decidable if, and only if, the property $\mathcal{P}$ defined as $(\mathcal{P}(x): \Longleftrightarrow x \in \textup{A})$ is decidable in $\textup{X}$.  And a property $\mathcal{P}$ defined over a set $\textup{X}$ is decidable in $\textup{X}$ if, and only if, there is an effective (or decision) procedure for deciding, for any $x \in \textup{X}$ whether or not $\mathcal{P}(x)$ holds.  Here the claim is straightforward, every such set of natural numbers is definable in the standard model.

(iii) Every effectively countable set $\textup{X} \subseteq \omega$ is definable over $\Omega$

Finally, a set $\textup{X}$ is effectively countable if, and only if, $\textup{X}$ is empty or there is an effectively computable function $\textup{F}: \omega \rightarrow \textup{X}$ that counts $\textup{X}$ (i.e., $\textup{X}$ is the image of $\textup{F}$, $\textup{X} = \mathsf{Im}(\textup{F}) := \{\textup{F}(n): n \in \omega\}$). 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 $\Omega$ as well as a diagonalization function that will play a role in the proof.