An Explicit Ordinal Bound for System T Dialogue Trees

RESUMO

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)\ge2$ 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.