An Explicit Ordinal Bound for System T Dialogue Trees

Abstract

Escardó's dialogue interpretation assigns to each closed term $t:(\iota \to \iota )\to \iota$ of Gödel's System~T a well-founded, countably branching tree $D(t)$, where $\iota$ is the natural-number type. We give a direct proof that its classical ordinal height is below ${\epsilon }_0$. More precisely, we compute a natural number $K(t)\ge 2$ from the type levels occurring in the source term and prove $h(D(t))<{\theta }_{K(t)}$, where ${\theta }_0=\omega$ and ${\theta }_{n+1}={\omega }^{{\theta }_n}$. Our proof translates recursors into closed infinitary templates and eliminates $\beta$-redexes by a finite sequence of passes indexed by ordinary type level. The translation and every pass preserve the dialogue denotation exactly. An auxiliary rank $\rho$ satisfies an additive substitution bound; each pass sends rank $\alpha$ to at most $2^{\alpha }$. Combining these estimates with a computable initial bound $\omega +m(t)$ and a dialogue-height bound $2^{\rho (N)}$ for closed ground normal forms $N$ yields the stated tower bound. A semantics-preserving translation transfers the result to Escardó's original combinatory interpretation. We formalise the proof in Agda over classical ordinals under explicit foundational assumptions.

19 pages, 1 figure