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:

  • Trued, 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 Trued, 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 LN 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(t1,…,tn) where all the ti’s are closed terms. Again pretty clear. I’ll write true0(φ) for this predicate, so true0(φ) 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 LN 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(φ(x1,…,xn), (a1,…,an)), where the xi’s are the free variables occurring in φ, and the ai’s are any elements of the structure. They also don’t expand L to LN.

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 Trued. This comes in two flavors: Trued( ⌜φ⌝ ), and the parametrized version Trued( ⌜φ(x1,…,xn)⌝ , [a1,…,an]). We’ll start with the simpler Trued( ⌜φ⌝ ).

Trued(⌜φ⌝) is a sequence of ever-longer formulas in L(PA), True0(⌜φ⌝), True1(⌜φ⌝), True2(⌜φ⌝), … 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 ⊧ Trued(⌜φ⌝).

And also this property:

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

(In fact these are equivalent, by the completeness theorem.) Note that the proof in PA of “φ↔Trued(⌜φ⌝)” 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 Trued(x) has been constructed. Then Trued+1(x) is this formula (in ‘vernacular’, i.e., a masochist could use this to formalize it completely):

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

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

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 Trued(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 Trued’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 Trued looks like this, employing the notation \vec{x} as short for x1,…,xn:

\text{True}_d(\ulcorner\varphi(\vec{x})\urcorner,[\vec{a}]),

where [\vec{a}] is the list \vec{a} 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 Trued enjoys this property, for any model N of PA:

For all \varphi(\vec{x}) of depth at most d and all [\vec{a}],

N\models\varphi(\vec{a}) iff N\models\text{True}_d(\ulcorner\varphi(\vec{x})\urcorner, [\vec{a}])

and also this property:

For all \varphi(\vec{x}) of depth at most d,

\text{PA}\vdash \forall\vec{u}\left(\varphi(\vec{u})\leftrightarrow\text{True}_d(\ulcorner\varphi(\vec{x})\urcorner, [\vec{u}])\right)

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

3 Comments

Filed under Peano arithmetic

3 responses to “Topics in Nonstandard Arithmetic 4: Truth (Part 1)

  1. Nice! I’m wondering about an asymmetry between the negative result:

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

    which seems to be talking about a specific model ℕ of PA, the standard model in ZF perhaps, or maybe more vaguely “the standard natural numbers” in “informal set theory”, and the positive results:

    For all \varphi(\vec{x}) of depth at most d and all [\vec{a}],

    N\models\varphi(\vec{a}) iff N\models\text{True}_d(\ulcorner\varphi(\vec{x})\urcorner, [\vec{a}])

    which seems to be talking about a specific arbitrary model N of PA in ZF, and also

    For all \varphi(\vec{x}) of depth at most d,

    \text{PA}\vdash \forall\vec{u}\left(\varphi(\vec{u})\leftrightarrow\text{True}_d(\ulcorner\varphi(\vec{x})\urcorner, [\vec{u}])\right)

    which is about provability (or equivalently, validity in all models).

    Can people prove this?

    For any model N of PA, there is no formula True(x) in L(PA) such that for all sentences φ in L(PA),
    N ⊧ φ iff N ⊧ True(⌜φ⌝).

    How about this?

    There is no formula True(x) in L(PA) such that for all sentences φ in L(PA),

    \text{PA}\vdash \varphi \leftrightarrow\text{True}\left(\ulcorner\varphi \urcorner\right)

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.