The -ish is because I've never seen something like this presented, except for some type theories, which are much less useful.

Anyway.

Primitive recursion is a simple method for creating total recursive functions. We can formalise it in such a way that (almost) any sufficiently slow-growing (sub \(\omega\) on the FGH) googological function can be encoded, and hence offers a way of proving that it is recursive and total.

This can even be represented in a way that is easily understandable: zero, successor, projection and composition can be paid no heed when showing a function is PR, and only the recursion step needs to be stated explicitly - and even this can be represented in a simpler manner.

Similarly, a simple extension of primitive recursion, n-fold recursion, can be used to show that more recursive functions (sub \(\omega^\omega\) on the FGH) are in fact total.

These, I propose, are mere examples of a more general concept, that of a Googological System.

A Googological System, unlike a type theory, is a formal system geared specifically towards allowing googological notations to be encoded into the system, and then proven to be total.

The basic concept of most notations is to always have something that's decreasing. In primitive recursion, it's the first argument of the function (and first n in n-fold), in the FGH (and HH) it's the ordinal index of the function, and in the Buchloz Hydra it's the ordinal that the tree corresponds to; this is the same with most notations we make. (Although I am *interested* in seeing a notation made with the concept of Bar Recursion, as this is something hitherto uninvestigated in and dissimilar to most googology; it doesn't come under this umbrella.)

It shouldn't be hard to make a system which allows recursion on trees (and then encode structure as the trees), and it should be possible to thereby make a way to formalise a notation capable of doing recursion up to SVO, although, admittedly, some parts of the notation would probably be extrenuous in order to support encodings, as many notations are built up in layers, and therefore needlessly complicated.

This has the potential to found some of googology, and prove notations to be halting in a *much more* formal way than the common intuition-based 'analysis' which is popular. However, it also has the potential, depending on the systems presented (i.e. if there's a remotely intuitive way to [look at the notation, and derive a sequence of expressible functions which dominates any given expressible function], we can just diagonalise like over a normal notation), to simply offer a shortcut to which anyone

I hope you reply in the comments. Like, you specifically. The previous paragraph is a potential topic for debate, and you're probably interested regardless. Probably.

PS: I am working on two of these so-called Googological Systems. Current lower bound estimates are \(SVO\) (slim chance of up to \(\psi(\Omega_\omega)\)) for the simple one, and \(>\psi_{\omega_1}(\chi(\varepsilon_{M+1}))\) (end of part 5 of Deedlit's ordinal notations) for a next step up.