The experimental bridge to the Gaia project allows now to import some definitions and theorems of the so-called Ketonen-Solovay combinatorial machinery into the Gaia environment (see Chapter 7 of the documentation).
The first topics treated in this version are: canonical sequences, accessibility, and a few rapidly growing hierarchies of arithmetical functions.