Archive for the ‘Undefinability of Truth’ Category

Fun With Robinson Arithmetic

September 17, 2010

in yesterday’s notes I mentioned Robinson Arithmetic (\mathsf{Q}) as a subsystem of the axiom system \textup{T} in Hellman’s example. Just because it’s so much fun, let’s talk about \mathsf{Q}.  The axioms are listed below.  The dot notation distinguishes between the symbol used and the relation it represents (this notation was used earlier without explanation here and here). \dot{\mathsf{S}}x indicates the successor function that returns the successor of x.

Robinson Arithmetic

(\textup{S1}) \ \forall x (\neg \dot{0} \ \dot{=} \ \dot{\mathsf{S}}x)
(\textup{S2}) \ \forall x \forall y (\dot{\mathsf{S}}x \ \dot{=} \ \dot{\mathsf{S}} y \rightarrow x \dot{=} y)
(\textup{L1}) \ \forall x (\neg x \dot{<} \dot{0})
(\textup{L2}) \ \forall x \forall y [x \dot{<} \dot{\mathsf{S}}y \leftrightarrow (x \dot{<} y \vee x \dot{=} y)]
(\textup{L3}) \ \forall x \forall y [(x \dot{<} y) \vee (x \dot{=} y) \vee (y \dot{<} x])
(\textup{A1}) \ \forall x (x \dot{+} \dot{0} \dot{=} x)
(\textup{A2}) \ \forall x \forall y [x \dot{+} \dot{\mathsf{S}}y \dot{=} \dot{\mathsf{S}}(x \dot{+} y)]
(\textup{M1}) \ \forall x (x \dot{\times} \dot{0} \dot{=} \dot {0})
(\textup{M2}) \ \forall x \forall y [(x \dot{\times} \dot{\mathsf{S}}y) \dot{=} (x \dot{\times} y) \dot{+} x]

These axioms are from Hinman and correspond to what Boolos, Burgess and Jeffrey (in chapter 16 of Computability and Logic) call “minimal arithmetic”. Since the Boolos et al book is so widely studied, here is a map linking both axiomatizations.

(\textup{S1}) \mapsto 1
(\textup{S2}) \mapsto 2
(\textup{L1}) \mapsto 7
(\textup{L2}) \mapsto 8
(\textup{L3}) \mapsto 9
(\textup{A1}) \mapsto 3
(\textup{A2}) \mapsto 4
(\textup{M1}) \mapsto 5
(\textup{M2}) \mapsto 6

This is going to be as confusing as keeping track of names in One Hundred Years of Solitude. Boolos et al compare \mathsf{Q}/minimal arithmetic to the system \mathsf{R}, which has historically been called “Robinson Arithmetic”.  \mathsf{R} differs from \mathsf{Q} in that it contains,

(\textup{Q0}) \ \forall x [x \dot{=} \dot{0} \vee (\exists y) (y \dot{=} \dot{\mathsf{S}}y)]

And it replaces \textup{L1}-\textup{L3} with,

(\textup{Q10}) \ \forall x \forall y [x \dot{<} y \leftrightarrow \exists z (\dot{\mathsf{S}}z \dot{+} x \dot{=} y)

In their comparison Boolos et al conclude that \mathsf{Q} and \mathsf{R} have a lot in common (e.g., some of the same theorems are provable), but in some cases \mathsf{R} is stronger than \mathsf{Q} –e.g., in the non-standard ordinal model of \mathsf{Q} some simple laws (like \dot{1} \dot{+} x \dot{=} x \dot{+} \dot{1}) fail to hold, in addition to (\textup{Q0}) and (\textup{Q10}).  At the same time, howerver, \mathsf{Q} is in some cases stronger than \mathsf{R}.  For example, there is a model (with domain \omega and non standard elements a and b and natural interpretations of \dot{0}, \dot{+}, \dot{\times}, \dot{\mathsf{S}}x of \mathsf{R} where basic laws like x \dot{<} \dot{\mathsf{S}}x fail to hold.

While it’s easier to represent all recursive functions in \mathsf{Q} is than it is to do so in \mathsf{Q} than in \mathsf{R}, any one of these will do for Hellman’s example.  What’s interesting is that in theories like \mathsf{Q} and \mathsf{R} which lack an induction schema (and thus fall just short of Peano Arithmetic) the truth predicate is undefinable.

Hopefully in the next update I’ll be able to get to Hellman’s second definability example.

Posted in Robinson Arithmetic, Undefinability of Truth | Leave a Comment »

Hellman’s First Definability Example

September 15, 2010

What Tarski’s Theorem shows is that interpreted formal languages that are interesting (i.e., with enough expressive machinery to represent arithmetic or fragments thereof) cannot contain a predicate whose extension is the set of code numbers (e.g., \mathsf{Th}(\Omega)^\#) of sentences true in the interpretation.  The extension of any proposed truth predicate in such a system escapes the definitional machinery of the system.  Of course, the truth predicate for first-order arithmetic can be defined with appeal to  a stronger system, like second-order arithmetic, in the case of the Peano Axioms, etc.

Hellman’s first example is the following.  It is a corollary of Tarski’s theorem that a theory in the language, \textup{L}, of arithmetic (e.g., an axiom system \textup{T} containing Robinson Arithmetic (\mathsf{Q})) with symbols for zero, successor, addition, and multiplication, when extended with a one place predicate, \mathsf{Tr}(x) (read “true in arithmetic” such that for each closed sentence \textup{S} in \textup{L} a new axiom of the form \ulcorner \mathsf{Tr}(n) \leftrightarrow \textup{S}\urcorner (where n is the numeral for a code number for the sentence \textup{S}), the resulting theory \textup{T}^{*} contains no explicit definition of  \mathsf{Tr}(x) in \textup{L}.

Connecting this to our ongoing discussion of determination of truth and reference in special collections of models, suppose that \alpha is the class of standard \omega-models of \textup{T}^{*}.  Then we have:

  • In \alpha-structures \textup{L}-truth determines \mathsf{Tr}-truth.
  • In \alpha-structures \textup{L}-reference determines \mathsf{Tr}-reference

Which means that once you have the arithmetical truths in the class \alpha, then so are the ‘true-in-arithmetic’ truths and the same goes for the reference of the vocabularies.  To avoid collapsing to reductionism via Beth’s theorem, note that there is no first-order theory (like those under discussion) in a language with finitely many non-logical symbols has as it’s models just the models in in \alpha.

If you extend \alpha to \alpha^{*} containing all models of \textup{T}^{*}, then you do get reductionism, since determination of reference in \alpha^{*} amounts to implicit definability in \textup{T}^{*} -thus showing that there exist non-standard models of arithmetic.

This is a good example because it is clear, based on popular, well established results and firmly shows how determination of truth and reference in one core theory carry over to it’s extension, without thereby reducing the extension to the core.

In the next update I’ll discuss Hellman’s second definability example.

Posted in Robinson Arithmetic, Supervenience and Determination, Tarski's Theorem, Undefinability of Truth | Leave a Comment »

Tarski’s Theorem

September 14, 2010

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 \textup{U}-section for the class of \Omega-definable sets is established and it’s diagonal is shown to not be definable over \Omega.

A \textup{U}-section is a set defined for any set \textup{A} and any relation \textup{U} \subseteq \textup{A} \times \textup{A} such that for each a \in \textup{A}, \textup{A}_{a} := \{b : \textup{U}(a, b)\}.  \textup{U} is universal for a class \mathcal{C} \subseteq \wp (\textup{A}) if, and only if, every member of the class \mathcal{C} is a \textup{U}-section.  The diagonal set of \textup{U} is \textup{D}_{\textup{U}} := \{a : \textup{U}(a, a)\}.

Second, assuming the definability of \mathsf{Th}(\Omega)^{\#}, there is a formula \phi (y) such that for all p, p \in \mathsf{Th}(\Omega)^{\#} \Longleftrightarrow \phi (\dot{p}) \in \mathsf{Th}(\Omega).  But since the function \mathsf{Sb} is effectively computable, it is definable  and so, \mathsf{Sb}(m) = p \Longleftrightarrow \psi (\dot{m}, \dot{p}) \in \mathsf{Th}(\Omega), for some \psi (x, y).  But this means that,

m \in \textup{D}_{\textup{U}} \Longleftrightarrow \exists p [\phi(\dot{p}) \in \mathsf{Th}(\Omega) and \psi(\dot{m}, \dot{p}) \in \mathsf{Th}(\Omega)]

m \in \textup{D}_{\textup{U}} \Longleftrightarrow \exists y [\phi(y) \wedge \psi(\dot{m}, y)] \in \mathsf{Th}(\Omega),

which means that \textup{D}_{\textup{U}} is definable.  This is a contradiction.  So, \mathsf{Th}(\Omega)^{\#} is not definable and not effectively countable.  Nor is \mathsf{Th}(\Omega) effectively countable.

In the next update (probably on a plane!) I’ll discuss this theorem and get into Hellman’s example.

Posted in Tarski's Theorem, Undefinability of Truth | Leave a Comment »

Statement of Tarski’s Theorem

September 13, 2010

The theorem showing that the theory determined by the standard model of arithmetic, \mathsf{Th} (\Omega), is undecidable and consequently not decidably axiomatizable (this means that \mathsf{Th} (\Omega) \not= \mathsf{Th} (\Gamma), for some \Gamma consisting of axioms of arithmetic, like those of Peano Arithmetic or one of it’s extensions) can be made stronger by showing that \mathsf{Th}(\Omega)^{\#} := \{p: \chi_{p} \in \mathsf{Th}(\Omega)\},  the set of indices of sentences that are true in \mathsf{Th} (\Omega), is not definable over \Omega, which means that \mathsf{Th}(\Omega) is not effectively enumerable.  This is known as Tarski’s Theorem on the undefinability of truth.

Now set up the (provably effectively computable) function \mathsf{Sb}(m):= \#(\chi_{m}(\dot{m})), which returns the least number m such that \chi_{m} is a formula of \textup{L}_{\Omega}.

In the next update I’ll discuss the proof of Tarski’s Theorem and move into the corollary that Hellman uses to give an example of determination without reduction.

Posted in Tarski's Theorem, Undefinability of Truth | Leave a Comment »

Assumptions On Definability Over The Standard Model Ω, Part 2

September 11, 2010

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.

Posted in Metatheory of First Order Logic, Models of Arithmetic, Undefinability of Truth | Leave a Comment »

Assumptions On Definability Over The Standard Model Ω, Part 1

September 10, 2010

In the late 30′s Tarski proved that arithmetical truth cannot be defined in arithmetic.  In the next few updates I’m going to be discussing Tarski’s Undefinability theorem and will follows chapter 4 of Hinman’s Fundamentals.  Check this earlier note if you want to get clear on the definability we’re talking about.

Below are some of the basic assumptions about definability and the standard model of arithmetic that will factor into the proof of Tarski’s theorem.

(i) Every effectively computable function \textup{F}: \omega \rightarrow \omega is definable over \Omega.

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

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

In the next update I’ll break down each of these assumptions and hopefully move into the theorem itself.  The point of all this is just to be able to get through Hellman’s example of determination without reduction using a corollary of the undefinability theorem.

Posted in Metatheory of First Order Logic, Models of Arithmetic, Undefinability of Truth | Leave a Comment »

Follow

Get every new post delivered to your Inbox.