greatitself.
Continue
research36 min studyLesson 980 in Mathematics

Arithmetical hierarchy and Tarski undefinability

Classify quantifier alternations and prove why arithmetic cannot define all of its own standard truth.

Before you begin
On this page

The question for today

What you’ll understand

  • Classify concrete computability index sets by computable-matrix quantifier forms.
  • Declare the free-variable and parameter conventions for the unrelativized hierarchy.
  • Derive Tarski’s contradiction for a proposed arithmetic truth predicate in the standard model.

Halting, totality, and truth all concern arithmetic, but their definitions require different kinds of unbounded quantification. The arithmetical hierarchy measures finite alternations between existential and universal searches. Tarski's theorem then shows that the truth set for all arithmetic sentences cannot be captured by any one arithmetic definition. We will classify specific program properties, compare finite tests with quantified guarantees, and finish with the precise standard-model scope of the undefinability argument.

State the convention before counting quantifier blocks

Work with relations on fixed finite tuples of natural numbers in the standard model, with those tuples as the free variables. For positive levels, use alternating unbounded quantifier blocks over a total computable matrix: Sigma begins existentially and Pi universally. Quantifiers of the same kind can share a block through effective tuple coding. Fixed natural-number parameters may be replaced by numerals and do not add arbitrary oracle information. No arbitrary set parameter or nonstandard-model parameter is being allowed.

These positive-level set classes agree with the usual arithmetic normal forms using bounded arithmetic matrices. This does not identify every computable relation with a bounded formula in the bare language of addition and multiplication. Bounded quantifiers do not count as new alternations in the standard syntactic hierarchy. Delta at a positive level means membership in both corresponding Sigma and Pi classes; Delta-one is exactly decidability, while Sigma-one is c.e. and Pi-one is co-c.e. A displayed upper-bound form alone does not prove completeness or exact minimal complexity.

A∈Σ20  ⟺  ∃R∈Comp ∀x [x∈A↔∃u∀v R(x,u,v)],A∈Π20  ⟺  ∃S∈Comp ∀x [x∈A↔∀u∃v S(x,u,v)].\begin{aligned}A\in\Sigma^0_2&\iff\exists R\in\mathrm{Comp}\ \forall x\,[x\in A\leftrightarrow\exists u\forall v\,R(x,u,v)],\\A\in\Pi^0_2&\iff\exists S\in\mathrm{Comp}\ \forall x\,[x\in A\leftrightarrow\forall u\exists v\,S(x,u,v)].\end{aligned}
Comp denotes total computable relations, selected metatheoretically and uniformly for every free number tuple x. The displayed R and S choices are not number-quantifier blocks of the arithmetic formulas.↔ Scroll wide equations horizontally.

Program properties expose different orders of search

Let H(e,x,s) mean that machine e on input x halts within s steps. It is decidable by bounded simulation. A program is total exactly when every input has some sufficient time bound, giving a Pi-two definition. Negating totality yields an existential input that fails to halt at every time bound, a Sigma-two definition. The input witness and time witness play different roles; exchanging their quantifiers would require a single uniform finite time bound and would describe a much stronger property.

Finiteness of a c.e. domain W sub e has a Sigma-two form: some numerical bound b exceeds every domain member. Express this as existence of b followed by universality over input x and stage s, requiring that x at least b never satisfies H(e,x,s). Pairing x and s keeps one universal block. These forms classify the sets from above. Their familiar completeness results require additional reductions, which are not proved merely by writing the quantifiers.

TOT={e:∀x∃s H(e,x,s)}∈Π20;FIN={e:∃b∀x∀s [x≥b⇒¬H(e,x,s)]}∈Σ20.\mathrm{TOT}=\{e:\forall x\exists s\ H(e,x,s)\}\in\Pi^0_2;\quad\mathrm{FIN}=\{e:\exists b\forall x\forall s\,[x\ge b\Rightarrow\neg H(e,x,s)]\}\in\Sigma^0_2.
The bounded-halting matrix is computable; unbounded alternation controls these positive-level upper bounds.↔ Scroll wide equations horizontally.

A single arithmetic truth predicate would contradict diagonalization

Let True be the set of codes of closed first-order arithmetic sentences true in the standard natural numbers, under our fixed effective syntax. Tarski's theorem says no arithmetic formula Tr(z) defines this entire set there. If such a formula existed, the diagonal lemma would give a sentence L whose truth is equivalent to not-Tr applied to its own code. Since the standard natural numbers satisfy Q, the formal fixed-point equivalence holds in that standard model and contradicts the proposed definition of truth.

The theorem does not ban external semantic definitions in a stronger metalanguage, nor partial truth predicates for fixed bounded levels of formulas. It also does not say that every arithmetic set is undefinable: halting and many more complicated sets are arithmetically definable. Fixed natural parameters do not evade the argument, because they can first be replaced by their numerals before diagonalization. The crucial scope is one formula defining truth for all arithmetic sentences in the standard model, not every conceivable use of the word truth.

N⊨L↔¬Tr⁡(⌜L⌝),Tr⁡ defining full truth would give N⊨L↔¬L.\mathbb N\models L\leftrightarrow\neg\operatorname{Tr}(\ulcorner L\urcorner),\qquad\operatorname{Tr}\text{ defining full truth would give }\mathbb N\models L\leftrightarrow\neg L.
The contradiction uses standard-model truth and the diagonal lemma, not an assumption that an arbitrary arithmetic theory is complete.↔ Scroll wide equations horizontally.

Work it through

Finite agreement does not settle a totality quantifier

Compare programs P and Q on natural input x: P waits x+2 stages and returns zero; Q does the same for x≤4 and loops for x≥5. Here a stage is a declared unit of the chosen program model, not a claim about a particular compiled Turing instruction count. Classify their totality and explain the limit of testing inputs zero through four for six stages.

  1. For each input x, P has a finite completion stage x+2. Thus every x has an s with H(P,x,s), proving P belongs to TOT. There is no one fixed stage bound for all inputs because x+2 grows without bound.

  2. Q agrees with P on all tested inputs zero through four, completing them at stages two through six. Yet input five never halts, so for that input every stage fails the bounded-halting test. Q therefore lies outside TOT.

  3. The finite experiment gives identical results for P and Q but verifies only finitely many instances. Totality requires the universal input quantifier, while non-totality of Q is certified here by inspecting its explicit looping branch. The quantifier formulas provide Π₂ and Σ₂ upper bounds without needing to run either program on every input.

∀x∃s H(P,x,s),∃x∀s¬H(Q,x,s)with witness x=5.\forall x\exists s\ H(P,x,s),\qquad\exists x\forall s\neg H(Q,x,s)\quad\text{with witness }x=5.
The time witness for P depends on x; the nonhalting input for Q is fixed before quantifying over all stages.↔ Scroll wide equations horizontally.
The result

P is total and Q is not, despite agreement throughout the specified finite test. Proof of an all-input statement requires information beyond that finite table.

The living notebook

Explore the model

Interactive lab

Interactive lab · optimization

Compare eventual approximation with exact arrival

Pause and Reset, set step size η to 0.5 and initial position x₀ to 2. Take eight Steps, giving iteration eight, x=1/128 and objective 1/32768. In exact arithmetic no finite iterate equals zero, but every positive tolerance is eventually met. For a fresh run Reset and set both η to 1 and x₀ to 2; one Step reaches zero exactly. This quadratic model illustrates different quantifier claims, not a totality decider or truth predicate. Each Step advances one iteration; control edits retain time.

Compare eventual approximation with exact arrivalGradient descent on f(x) = x²/2: xₙ = (1 − η)ⁿx₀. Playback advances two discrete iterations per second. Values outside |x| ≤ 4 are explicitly reported. Current readings: Position x0: 2; Objective x²/2: 2; Iteration behavior: Stable step. All parameters are adjustable with the labeled controls below.−4−202402.174.356.528.7Parameter xf(x) = x²/2n = 0
ObjectiveDiscrete iterate
Position x0
2
Objective x²/2
2
Iteration behavior
Stable step
n = 0 · t = 0 s

Gradient descent on f(x) = x²/2: xₙ = (1 − η)ⁿx₀. Playback advances two discrete iterations per second. Values outside |x| ≤ 4 are explicitly reported. Parameter changes pause playback and recompute the model at the current elapsed time. Reset restores both parameters and returns time to zero. Playback starts paused. Adjust either parameter, then choose Play or Step.

Look forFor every tolerance there is a time is weaker than there is a time of exact equality.

Pause & reason

Check your understanding

Which statement correctly specifies the Tarski theorem used in this lesson?

Your turn

Try it yourself

Assume an arithmetic formula Tr(z), possibly with fixed natural parameters, defines standard truth for every arithmetic sentence code. Give the diagonal contradiction and explain why replacing Tr with the standard proof predicate avoids that particular contradiction without making the proof predicate a truth definition.

Take a moment to make a prediction or work it out on paper. Open a hint when you need one.

Give me a hint

Replace fixed parameters by numerals first. Apply the diagonal lemma to the negation of the resulting one-variable formula, then evaluate its equivalence in the standard model.

Compare with the solution

After substituting numerals for the fixed parameters, the diagonal lemma yields L with Q⊢L↔¬Tr⁡(⌜L⌝)Q\vdash L\leftrightarrow\neg\operatorname{Tr}(\ulcorner L\urcorner). Since Q is true in the standard model, that equivalence holds there. The alleged definition gives Tr of L exactly when L is true, so L is true exactly when it is false, a contradiction. Replacing Tr by provability supplies no all-truth biconditional: a consistent effective theory can leave L unproved. The resulting Gödel sentence expresses a limit of that proof system instead of producing a semantic contradiction.

Keep the idea

Take it with you

  • Positive arithmetical levels track alternating number-quantifier blocks with explicit parameter conventions.
  • Finite program tests cannot replace an all-input or all-time quantifier.
  • Tarski excludes one arithmetic definition of full standard truth while allowing restricted predicates and external semantics.

Read further

Original sources and deeper explanations to follow at your own pace.

Optional progress, saved in this browser when available. Revisit any lesson at any time.

Lesson not marked complete.