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.

About these ads

This entry was posted on September 11, 2010 at 5:31 AM and is filed under Metatheory of First Order Logic, Models of Arithmetic, Undefinability of Truth. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

Logicians do it with Models

Assumptions On Definability Over The Standard Model Ω, Part 2

Like this:

Leave a Reply Cancel reply

Follow “Logicians do it with Models”