What's the natural metric/topology on infinite derivations?

31 Views Asked by At

In the appendix to the SEP Proof Theory article, Michael Rathjen makes reference to a topology on infinite derivations for which a variant of cut-elimination is a continuous function. The referenced paper by Mints is not very explicit. Another common referenced paper is by Kreisel, Mints, and Simpson (paper) where the following description is given.

The most obvious additional requirement on $\rho$, suggested by this step is continuity of $\rho$, where a neighborhood of a derivation is determined (as is usual for trees) by a finite number of finite initial paths in the given derivation tree.

Is this just the topology on Baire space where basic open sets are infinite paths extending a finite path? It appears so, but I would like some verification that I'm understanding this description correctly. Pointers to introductory material that discusses this in more detail would also be very appreciated.