System T and the Dialectica Interpretation

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

An intuitionistic proof of $\mathrm{\forall }n\mathrm{\exists }mA(n,m)$ establishes that a witness exists for every input. Its conclusion need not display the finite-type functional that computes the witness. Gödel’s Dialectica interpretation makes that hidden data explicit: positive quantifiers become witnesses, negative quantifiers become challenges, and implication transforms both.

The target of this chapter is Gödel’s System $T$. The source is first-order Heyting arithmetic $\mathsf{HA}$, exactly as in the direct soundness theorem of Avigad and Feferman’s reconstruction [AF98]. This choice is important. The same source explains direct higher-type variants, but not full extensional $E\text{-}{\mathsf{HA}}^{\omega }$; the latter first needs a separate formal interpretation into a suitable weaker higher-type arithmetic. Nothing below silently crosses that boundary.

Primitive recursion at finite types

Finite types are generated by $$\sigma ,\tau ::=\mathbb{N}\mid \sigma \to \tau .$$ Products are convenient for tuples but eliminable by currying, so they are metanotation here. Terms are the simply typed lambda terms with $$0:\mathbb{N},\mathsf{S}:\mathbb{N}\to \mathbb{N},{\mathsf{R}}_{\sigma }:\sigma \to (\mathbb{N}\to \sigma \to \sigma )\to \mathbb{N}\to \sigma .$$ The computation rules are $$(\lambda x.t)u⟶t[u/x],{\mathsf{R}}_{\sigma }ag0⟶a,$$ $${\mathsf{R}}_{\sigma }ag(\mathsf{S}n)⟶gn({\mathsf{R}}_{\sigma }agn).$$ We take their compatible closure. This lambda presentation is definitionally intertranslatable with the typed $K,S,R$ presentation used in the primary source [AF98].

Addition, multiplication, and triangular summation are System $T$ terms: For example, Recursion occurs on a natural number, although the accumulated result may have any finite type. Thus ${\mathsf{R}}_{\mathbb{N}\to \mathbb{N}}$, for example, builds a sequence of functions.

Reducibility and normalization

Let $\mathsf{SN}$ be the terms admitting no infinite reduction sequence. Define reducibility by type: $${\mathcal{R}}_{\mathbb{N}}=\mathsf{SN},{\mathcal{R}}_{\sigma \to \tau }=\{t\mid \mathrm{\forall }u\in {\mathcal{R}}_{\sigma }.tu\in {\mathcal{R}}_{\tau }\}.$$ A term is neutral if it is a variable, a neutral application, or a recursor whose natural argument is neutral. The candidate facts needed below are:

1. $t\in {\mathcal{R}}_{\sigma }$ implies $t\in \mathsf{SN}$;

2. $t\in {\mathcal{R}}_{\sigma }$ and $t⟶t^{\prime }$ imply $t^{\prime }\in {\mathcal{R}}_{\sigma }$;

3. a neutral $t:\sigma$ is in ${\mathcal{R}}_{\sigma }$ if every immediate reduct of $t$ is;

4. every variable is reducible.

All four are proved together by induction on $\sigma$. At arrow type, apply the term to an arbitrary reducible argument. For neutral expansion, the reducts of $tu$ either reduce $t$, reduce $u$, or expose a head redex; nested induction on the finite reduction height of $u$ closes the case.

Proof of Lemma 66.1 — Reducibility of primitive recursion

Proof. Compatible one-step reduction is finitely branching on a finite term. Hence strong normalization of $n$ gives a maximum reduction length. Induct on that length, with a subordinate induction on the reduction heights of $a$ and $g$. Candidate closure handles reductions inside the three arguments. If the head argument is $0$, the head reduct is $a$. If it is $\mathsf{S}k$, the head reduct is $gk({\mathsf{R}}_{\sigma }agk)$. The outer induction makes the recursive call reducible, and reducibility of $g$ handles its two arguments. If the head argument is neutral, candidate neutral expansion applies. These are all immediate reducts. ◻

For a substitution $\rho$, write $\rho \in {\mathcal{R}}_{\mathrm{\Gamma }}$ when $x:\sigma \in \mathrm{\Gamma }$ implies $\rho (x)\in {\mathcal{R}}_{\sigma }$.

Proof of Theorem 66.2 — Fundamental theorem

Proof. Induct on the typing derivation. Variables use $\rho$. Application uses the arrow clause. For abstraction, extend $\rho$ by an arbitrary reducible argument; beta expansion and the induction hypothesis give a reducible result. Zero has no reduct and therefore lies in $\mathsf{SN}$. If $u\in {\mathcal{R}}_{\mathbb{N}}$, then $u\in \mathsf{SN}$, and every reduction of $\mathsf{S}u$ reduces $u$; hence $\mathsf{S}u\in \mathsf{SN}$. Thus successor satisfies the arrow clause. The recursor case is lemma 66.1. ◻

Proof of Corollary 66.3 — Normalization and numerical canonicity

Proof. Use the identity substitution in theorem 66.2 and candidate fact 1. For canonicity, inspect a closed normal natural term. It is neither a variable nor a lambda. An application or recursor at its head would either contain a redex or have a closed neutral natural head, which does not exist. Thus it is $0$ or $\mathsf{S}n$; iterate the argument. ◻

The normalization claim has the same System $T$ signature and reduction boundary as Avigad and Feferman’s Theorem 4.3.3 [AF98].

This proof supplies normalization, not a feasible cost bound. System $T$ functionals can have very large normalization behavior as their finite type level rises.

The Dialectica matrix

For every arithmetic formula $A$, its interpretation has the form $$A^{\mathsf{D}}\equiv \mathrm{\exists }\overrightarrow{x}\mathrm{\forall }\overrightarrow{y}.A_{\mathsf{D}}(\overrightarrow{x},\overrightarrow{y}),$$ where the matrix $A_{\mathsf{D}}$ is quantifier-free in the language of System $T$. Witness variables $\overrightarrow{x}$ and challenge variables $\overrightarrow{y}$ may be empty. If $A^{\mathsf{D}}=\mathrm{\exists }\overrightarrow{x}\mathrm{\forall }\overrightarrow{y}.A_{\mathsf{D}}$ and $B^{\mathsf{D}}=\mathrm{\exists }\overrightarrow{u}\mathrm{\forall }\overrightarrow{v}.B_{\mathsf{D}}$, define: Negation is implication to false, hence $$(\mathrm{\neg }A{)}^{\mathsf{D}}\equiv \mathrm{\exists }Y\mathrm{\forall }\overrightarrow{x}.\mathrm{\neg }{A}_{\mathsf{D}}(\overrightarrow{x},Y\overrightarrow{x}).$$ The functional $U$ sends a witness for the premise to a witness for the conclusion. The functional $Y$ sends a premise witness and a challenged conclusion to a challenge against that premise. Forgetting $Y$ destroys the contravariant information in implication.

Soundness for Heyting arithmetic

Let $\mathsf{HA}$ be first-order intuitionistic arithmetic with equality, zero, successor, primitive-recursive function symbols, and induction for all formulas. Let equational System $T$ include quantifier-free propositional reasoning and induction for quantifier-free formulas. This is the exact first-order source/finite-type target pair used in the direct theorem below.

Proof of Lemma 66.4 — Deciding a matrix

Proof. Induct on the quantifier-free matrix. Equality of natural-number terms is decidable by primitive recursion. Boolean combinations compose their characteristic terms. Define $\mathsf{Cond}$ by recursion on its numerical test. No decision procedure for quantified formulas is asserted. ◻

Proof of Theorem 66.5 — Dialectica soundness for HA

Proof. Induct on the $\mathsf{HA}$ derivation. Atomic equality axioms need no witness. Conjunction introduction pairs the two witness tuples; its eliminations project one tuple. Disjunction introduction supplies tag $0$ or $1$; elimination combines the branch witnesses with $\mathsf{Cond}$. Universal introduction abstracts the source variable into the witness functional, and elimination applies it. Existential introduction pairs the arithmetic witness with the matrix witness; elimination substitutes both into the continuation.

For implication introduction, the induction hypothesis under an assumed witness $\overrightarrow{x}$ computes a result witness $U\overrightarrow{x}$ and identifies which premise challenge $Y\overrightarrow{x}\overrightarrow{v}$ suffices for each result challenge $\overrightarrow{v}$. These are exactly the two functionals in the implication clause. For modus ponens, suppose $\overrightarrow{a}$ realizes $A$, while $U,Y$ realize $A\to B$. Instantiate the first matrix at $Y\overrightarrow{a}\overrightarrow{v}$, and the second at $\overrightarrow{x}=\overrightarrow{a}$; then $U\overrightarrow{a}$ realizes $B$. Thus the extracted witness is functional application.

Contraction $A\to A\wedge A$ duplicates the positive witness. For a pair of challenges, lemma 66.4 and $\mathsf{Cond}$ select a challenge on which the required premise matrix would otherwise fail. Weakening ignores an unused witness. Exchange and associativity only rearrange tuples.

For arithmetic induction, assume extracted $a$ realizes the base case and extracted step functionals transform a witness at $n$ into one at $\mathsf{S}n$, while translating a challenge backwards. Define the positive witness at $n$ by $\mathsf{R}agn$. A subordinate primitive recursion threads the final challenge backwards through the preceding stages. Target induction on $n$ proves the resulting matrix. The defining equations for the primitive-recursive arithmetic symbols are handled by their System $T$ representatives. These cases cover the axiom and rule schemes of the selected presentation of $\mathsf{HA}$. ◻

The proof is syntax directed and local: cut or modus ponens composes extracted terms rather than globally normalizing the source proof. Avigad and Feferman state this theorem as their Theorem 2.4.1 and spell out modus ponens, contraction, matrix decision, and induction [AF98].

A witness calculated

Let $\mathsf{Tri}(n,m)$ be the primitive-recursive graph of triangular summation. Its defining equations prove $$\mathsf{Tri}(0,0),\mathsf{Tri}(n,m)⟹\mathsf{Tri}(\mathsf{S}n,\mathsf{S}n+m).$$ Heyting arithmetic proves $$\mathrm{\forall }n\mathrm{\exists }m.\mathsf{Tri}(n,m)$$ by induction: choose $0$ at the base, and from witness $m$ choose $\mathsf{S}n+m$ at the step. Because $\mathsf{Tri}$ is atomic, the Dialectica translation is simply $$\mathrm{\exists }{F}^{\mathbb{N}\to \mathbb{N}}\mathrm{\forall }n.\mathsf{Tri}(n,Fn).$$ Following the soundness induction gives $$F=\mathsf{tri}=\lambda n.{\mathsf{R}}_{\mathbb{N}}0(\lambda k.\lambda r.\mathsf{add}(\mathsf{S}k)r)n.$$ The earlier reduction calculates $F(3)=6$. The target proof also verifies $\mathsf{Tri}(3,6)$; computation alone would not establish the matrix.

The higher-type and classical boundary

The direct argument extends to the intensional, weakly extensional, and type-zero-equality higher-type arithmetics paired with their corresponding targets. It does not directly interpret full $E\text{-}{\mathsf{HA}}^{\omega }$. Avigad and Feferman instead describe a formal interpretation of the extensional theory into ${\mathsf{HA}}_0^{\omega }$, preserving formulas whose variables have low types, before applying Dialectica [AF98].

Likewise, classical arithmetic first uses a negative translation. Countable choice and the principles needed for classical analysis require stronger functionals, notably bar recursion. That extension is developed separately; it is not a consequence of theorem 66.5.

Seminar and practical

Suggested first pass.

Begin with exercise 66.5; then run exercise 66.7.

Exercise 66.5¶

★★☆ Explain the variance of $U$ and $Y$ in the implication clause by staging a game between a witness and a challenger. Then give a concrete formula for which deleting $Y$ loses information. (Half a page.)

Referenced from 4 locations

• System T and the Dialectica Interpretation
• Solutions for Chapters 64–66

Exercise 66.6¶

★★☆ Prepare a boundary ledger with rows for $\mathsf{HA}$, ${\mathsf{HA}}_0^{\omega }$, $E\text{-}{\mathsf{HA}}^{\omega }$, classical arithmetic, countable choice, and classical analysis. For each, state whether this chapter gives a direct interpretation, a composed interpretation, or no theorem. Cite the exact construction required in the latter two cases. (One page.)

Referenced from 3 locations

• System T and the Dialectica Interpretation
• Solutions for Chapters 64–66

Exercise 66.7¶

★★★ Practical project.system-t-witness-evaluator The companion artifact system-t-witness-evaluator implements the natural-number fragment of System $T$. Add multiplication, run $\mathsf{tri}3$, and add a mutation that uses the predecessor index where its successor is required. Record the Kappa commands and explain which recursor equation the mutation violates. (One page plus code.)

Referenced from 5 locations

• System T and the Dialectica Interpretation
• Object calculus checker and evaluator
• ch:system-t-dialectica: a finite-type witness

Sources and theorem boundary

The finite-type syntax, exact Dialectica clauses, and soundness induction are from Avigad and Feferman [AF98]. The reducibility development is a Tait argument specialized to System $T$; Tait’s intensional interpretation is a historical primary source for finite-type proof interpretations [Tai67]. The companion course supplies evaluation and metatheory exercises [Hof24]. Bar-recursive extensions are sourced and proved separately. The extracted witness theorem here is exactly for the selected $\mathsf{HA}$-to-System-$T$ translation.