An Explicit Ordinal Bound for System T Dialogue Trees

MingKun Xiao, YiXuan Sun

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 t…