An Explicit Ordinal Bound for System T Dialogue Trees

Abstract

Escardó's dialogue interpretation assigns to each closed term $t:(ι\toι)\toι$ of Gödel's System~T a well-founded, countably branching tree $D(t)$, where $ι$ is the natural-number type. We give a direct proof that its classical ordinal height is below $ε_0$. More precisely, we compute a natural number $K(t)\ge2$ from the type levels occurring in the source term and prove $h(D(t))<θ_{K(t)}$, where $θ_0=ω$ and $θ_{n+1}=ω^{θ_n}$. Our proof translates recursors into closed infinitary templates and eliminates $β$-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 $ρ$ satisfies an additive substitution bound; each pass sends rank $α$ to at most $2^α$. Combining these estimates with a computable initial bound $ω+m(t)$ and a dialogue-height bound $2^{ρ(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.