Welp, other people have gotten into trying to beat FOOT, so I figured I might as well try my hand at it.

With a decided lack of originality, I've decided to name my system FOFT (First Order Functional Theory). As the name suggests, the fundamental new objects are functionals on ordinals. Functionals are defined as follows:

Let \(F_\alpha\) denote the set of \(\alpha\)-functionals.

A 0-functional is just an ordinal.

A \(n+1\)-functional is a function from \(F_n\) to \(F_n\). Equivalently, it is a function from \(\prod_{i=1}^n F_i\) to \(F_0\). (You can see this by repeatedly applying the definition of \(F_i\) in the range - for example, \(f: F_3 \mapsto F_3 \implies f: F_3 \mapsto (F_2 \mapsto F_2) \implies f: F_3 \mapsto (F_2 \mapsto (F_1 \mapsto F_1)) \implies f: F_3 \mapsto (F_2 \mapsto (F_1 \mapsto (F_0 \mapsto F_0)))\). )

We can use the latter definition to extend the notion of functionals into the transfinite: An \(\alpha\)-functional is a function from \(\prod_{\beta < \alpha} F_\beta\) to \(F_0\).

Now that we have the background, here is the definition of FOFT:

Define \(FOFT\) to be the language FOST augmented by the symbol \(Func\). \(Func\) takes two variables; the expression \(Func(\gamma,\delta)\) evaluates to the \(\delta\)-functional \(Func_\gamma^\delta\) to be defined later.

We define a restricted version of \(FOFT\), denoted \(FOFT_\alpha^\beta\) for ordinals \(\alpha, \beta\). \(FOFT_\alpha^\beta\) is again the language FOST augmented by the symbol \(Func\), except this time the expression \(Func(\gamma,\delta)\) only evaluates to the \(\delta\)-functional \(Func_\gamma^\delta\) when either \(\delta < \beta\) or \(\delta = \beta \wedge \gamma < \alpha\); otherwise, \(Func(\gamma,\delta)\) is set to the 0 \(\delta\)-functional.

Given ordinals \(\alpha, \beta\) and a function \(f\) such that for \(\gamma < \beta\), \(f(\gamma)\) is a \(\gamma\)-functional, define the language \(FOFT_\alpha^\beta (f)\) to be \(FOFT_\alpha^\beta\) augmented by the symbol \(f\); the expression \(f(\gamma)\) is used to denote precise the \(\gamma\)-functional \(f(\gamma)\).

Given ordinals \(\alpha, \beta\), define a \(\beta\)-functional \(Func_\alpha^\beta\) by defining \(Func_\alpha^\beta (f) \) (with \(\alpha, \beta, f\) defined as in the previous paragraph) to be the smallest ordinal \(\lambda\) such that \(V\) and \(V_\lambda\) satisfy precisely the same sentences in \(FOFT_\alpha^\beta(f)\).

FOFT(n) can then be defined as the largest number such that there is an FOFT sentence of n symbols or less that uniquely defines the number. Finally, define Superfoft to be FOFTgoogol(googol) (that is, FOFT(FOFT(...(FOFT(googol)...)) with a googol applications of FOFT).

Now that we have defined our extended languages, let's see how they compare to other extensions of FOST like FOOT and Emlightened's language for Little Biggedon (let's call the latter L).

Now, \(Func^0_0\) is just the smallest \(\lambda\) such that \(V\) and \(V_\lambda\) satisfy the same sentences of FOST, so \(Func^0_0\) is just Wojowu's Ord. \(Func^0_1\) is the smallest \(\lambda\) such that \(V\) and \(V_\lambda\) satisfy the same sentences of FOST augmented by \(Func^0_0\) (or Ord), so it is equal to Ord2. So in general, \(Func^0_\alpha\) is equal to \(\text{Ord}_{1+\alpha}\). \(FOFT^1_0\), then, can specify \(Func^0_\alpha\) for any ordinal \(\alpha\) it can specify; equvalently, it can specify \(\text{Ord}_\alpha\). So \(FOFT^1_0\) is equivalent to FOOT.

That's it for now. Corrections and suggestions for improvement are welcome!