BIG FOOT is supposedly a finite number which is defined using first-order oodle theory (an extension of set-theory) like defined here. It has been shown here that BIG FOOT is not well-defined. The reasoning goes as the following:
Suppose that the transfinite ordinal $\alpha_0$ in the original definition is formalised in $T$ by a defining formula $\varphi(\alpha)$ with a free occurence of a variable term $\alpha$. Then the existence of $\alpha_0$ satisfying $\varphi(\alpha_0)$ ensures that the existence of $\beta < \alpha_0$ satisfying $\varphi(\beta)$ by the definition of $\alpha_0$. By the minimality of $\alpha_0$, it implies $\alpha_0 = \beta < \alpha_0$, which contradicts the well-foundedness of $\alpha_0$.
I have a question: is $\varphi$ unary and why it is? I've thought that the language of first-order oodle theory uses n variables as an input.