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
, truth for formulas of parse-tree depth at most_{d}*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, and likewise an infinite sequence of formulas._{d} - 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*_{1},…,*t _{n}*) where all the

*t*’s are closed terms. Again pretty clear. I’ll write true

_{i}_{0}(φ) for this predicate, so true

_{0}(φ) 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*in the structure

_{N}*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*_{1},…,*x _{n}*), (

*a*

_{1},…,

*a*)), where the

_{n}*x*’s are the free variables occurring in φ, and the

_{i}*a*’s are any elements of the structure. They also don’t expand

_{i}*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

*( ⌜φ⌝ ), and the parametrized version True*

_{d}*( ⌜φ(*

_{d}*x*

_{1},…,

*x*)⌝ , [

_{n}*a*

_{1},…,

*a*]). We’ll start with the simpler True

_{n}*( ⌜φ⌝ ).*

_{d}True* _{d}*(⌜φ⌝) is a sequence of ever-longer formulas in L(PA), True

_{0}(⌜φ⌝), True

_{1}(⌜φ⌝), True

_{2}(⌜φ⌝), … 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(⌜φ⌝) ∧ True_{d}(⌜ψ⌝)_{d}

∧x=⌜∃yφ(y)⌝ → ∃uTrue(⌜φ(_{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

*’s into a single formula True(*

_{d}*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*

_{1},…,

*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.

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

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:

which seems to be talking about a

specific arbitrarymodel N of PA in ZF, and alsowhich is about provability (or equivalently, validity in

allmodels).Can people prove this?

How about this?

Good questions. I didn’t originally give the proof of the Undefinability Theorem, but the title of this blog means I am honor bound to. I decided to put the proof at the end of the post, where I also answer your question. Briefly, yes it holds for all models N of PA, and yes for the provability version.

Thanks very much.