Topics in Nonstandard Arithmetic 4: Truth (Part 1)

Prev TOC Next

In post 15 of the Conversation, I observed:

• Gödel’s two most famous results are the completeness theorem and the incompleteness theorem.
• Tarski’s two most famous results are the undefinability of truth and the definition of truth.

The second bullet has occupied its share of pixels in the Conversation. Time for a summing up.

Here’s a precise statement of the Tarski Undefinability Theorem for PA. (As usual, ⌜φ⌝  stands for the Gödel number of φ.)

There is no formula True(x) in L(PA) such that for all sentences φ in L(PA),
ℕ ⊧ φ iff ℕ ⊧ True(⌜φ⌝).  (The symbol ⊧ is defined below.)

A similar theorem holds for ZF. Note that these results don’t involve the theories, just the structures: they are semantic, not proof-theoretic.

The title of this blog means I am honor bound to sketch the proof of this theorem. However, it turns out that Tarski’s definition of truth matters more for us, so I will relegate the proof to an addendum.

As an induction, the truth definition looks rather innocuous. Trying to formalize it leads us to several “workarounds” or “loopholes” in the Undefinability Theorem. I’ll discuss four in this and future posts:

• True_d, truth for formulas of parse-tree depth at most d. This is an infinite sequence of formulas.
• True for set-based structures, a single formula of ZF. (Models of PA qualify as set-based structures.)
• Sat_Σn, satisfaction for Σ_n formulas. A refinement of True_d, and likewise an infinite sequence of formulas.
• The Arithmetized Completeness Theorem (ACT), a different approach.

Let’s start with Tarski’s inductive definition of truth for a structure N in a language L. So for every relation symbol of L, we have a corresponding relation on N with the same arity, and ditto for constants and function symbols. First step: expand the language by adding new constants for all the elements of N. We call these names, and L_N denotes the expanded language. In the special case of ℕ, we could skip this step since we have numerals: 0, 1, 1+1, (1+1)+1, … In any case, we need a way to refer to any element of N.

Next, we define the value of closed terms. This is inductive, but I think it’s obvious enough to skip the description. After that, we define truth for closed atomic sentences: formulas of the form R(t₁,…,t_n) where all the t_i’s are closed terms. Again pretty clear. I’ll write true₀(φ) for this predicate, so true₀(φ) holds iff φ is a true closed atomic formula. Just two observations: these steps depend on the interpretation of the relation symbols, function symbols, and constants of L_N in the structure N. Also, I’ll usually assume that the special relation symbol ‘=’ is interpreted by actual equality. (Convenient, but not essential.)

After all this throat-clearing, the inductive definition is simple.

true(φ ∧ ψ)	iff	true(φ) and true(ψ)
true(¬φ)	iff	not true(φ)
true(∃x φ(x))	iff	there exists a name c such that true(φ(c))

I’m assuming that ∨ and ∀ are abbreviations (‘vernacular’), so for example ∀x φ(x) is rewritten as ¬∃x¬φ(x). But it’s easy enough to add clauses if we want these symbols to be primitive:

true(φ ∨ ψ)	iff	true(φ) or true(ψ)
true(∀x φ(x))	iff	for all names c, true(φ(c))

The induction here is on the parse-tree depth of the closed formulas. The sooner you start thinking of formulas as parse-trees, the better! But some authors prefer to induct on the length of the formulas, which does work.

You can see why we had to add all those names: the definition of truth for quantifiers wouldn’t work otherwise. Some authors take a slightly different tack, defining true(φ(x₁,…,x_n), (a₁,…,a_n)), where the x_i’s are the free variables occurring in φ, and the a_i’s are any elements of the structure. They also don’t expand L to L_N.

Time to introduce some standard notation. N ⊧ φ means that the closed formula (aka sentence) φ is true in N. Usually read, N satisfies φ.

OK. How do we interpret the right hand sides of the induction? Informally! You’re expected to know the meaning of the English words ‘and’, ‘not’, and ‘there exists’. People also say that the meta-theory is naive set theory. I’ll look at how this can be formalized in ZF set theory in the next post.

But first, let’s look at True_d. This comes in two flavors: True_d( ⌜φ⌝ ), and the parametrized version True_d( ⌜φ(x₁,…,x_n)⌝ , [a₁,…,a_n]). We’ll start with the simpler True_d( ⌜φ⌝ ).

True_d(⌜φ⌝) is a sequence of ever-longer formulas in L(PA), True₀(⌜φ⌝), True₁(⌜φ⌝), True₂(⌜φ⌝), … They all take the Gödel number of a closed formula φ as the argument. They enjoy this property, for any model N of PA:

For all φ of depth at most d,      N ⊧ φ  iff  N ⊧ True_d(⌜φ⌝).

And also this property:

For all φ of depth at most d,      PA ⊢ φ↔True_d(⌜φ⌝).

(In fact these are equivalent, by the completeness theorem.) Note that the proof in PA of “φ↔True_d(⌜φ⌝)” is different for each φ! We don’t have a single uniform proof.

As always with Gödel numbers, it takes a bit of low-level futzing to justify things fully. However, the motto “PA can handle syntax” works quite well for handwaving. For example, PA has a formula for “is a Gödel number”, or for “x is a Gödel-number of a formula of the form φ∧ψ, and y=⌜φ⌝ and z=⌜ψ⌝ are the Gödel numbers of the two conjuncts”. (See post 8 in the Conversation for a bit more, or consult a textbook such as Kaye.)

Assume inductively that True_d(x) has been constructed. Then True_d+1(x) is this formula (in ‘vernacular’, i.e., a masochist could use this to formalize it completely):

            x= ⌜¬φ⌝           →     ¬True_d(⌜φ⌝)
∧          x= ⌜φ∧ψ⌝       →     True_d(⌜φ⌝) ∧ True_d(⌜ψ⌝)
∧          x= ⌜∃y φ(y)⌝  →      ∃u True_d(⌜φ(u)⌝)

The occurrences of True_d are copied into True_d+1, with suitable modifications. (Actually, it’s a touch messier: True_d+1(⌜φ⌝) should check that φ has depth at most d+1, and if φ’s depth is at most d, it should return True_d(⌜φ⌝).)

The clause for ∃y φ(y) deserves comment. The quantifier ∃y is “buried inside the Gödel number”; PA does some parsing to “see that it’s there”. The quantifier ∃u however is a true, explicit quantifier of L(PA). I said in the Conversation that quantifiers “bleed through”. In other words, the formulas True_d(x) occur higher and higher in the Arithmetical Hierarchy as d increases. This explains, in part, why it is not possible to combine all the True_d’s into a single formula True(x). See post 13 and posts 15 through 17 for a much more extensive discussion of the matter.

The parametrized version of True_d looks like this, employing the notation as short for x₁,…,x_n:

,

where is the list coded as a single element.

PA has several methods of coding finite lists as single numbers. You can iteratively use a recursive pairing function, but that only provides codes for lists of a given fixed length. In his 1931 paper on the incompleteness theorem, Gödel used the Chinese Remainder Theorem to provide a coding for lists of any finite length.

The parametrized version of True_d enjoys this property, for any model N of PA:

For all of depth at most d and all ,

iff

and also this property:

For all of depth at most d,

Next post: defining ‘true’ in ZF.

---

Addendum: Tarski’s Undefinability Theorem

I stated this as:

There is no formula True(x) in L(PA) such that for all sentences φ in L(PA),
ℕ ⊧ φ iff ℕ ⊧ True(⌜φ⌝).

This holds for any model N of PA, not just ℕ. A fortiori there is no formula True(x) for which, for all sentences φ in L(PA), PA ⊢ φ↔True(⌜φ⌝). For if we had such a formula, then we would have N ⊧ φ iff N ⊧ True(⌜φ⌝) for all models N of PA.

Let N be a model of PA. Suppose there is a formula True(x) with one free variable such that for all sentences φ in L(PA),  N ⊧ φ iff N ⊧ True(⌜φ⌝). (Here, by “formula” and “sentence”, I mean standard length formulas and sentences. Although I think the argument still works if we allow things that “N thinks” are formulas and sentences.)

Let {φ_n(x):n∈ω} be an effective enumeration of all formulas of L(PA) with one free variable. Consider

ψ(x) = ¬True(⌜φ_x(x)⌝)

Then ψ(x) can be expressed as a formula of L(PA), since ⌜φ_x(x)⌝ depends recursively on x. So it occurs in the enumeration, say as φ_n(x). Then

N ⊧ φ_n(n) ⇔ N ⊧ ¬True(⌜φ_n(n)⌝) ⇔ N ⊧ ¬φ_n(n).

Contradiction, QED.

Prev TOC Next