Bop-counting function

The bop-counting function is a function defined by Harvey Friedman, arising in study of binary operations on structures.
==Definition==
Let \(D\) be a set. A ternary relation on \(D\) is a set \(R\subseteq D^3\). We call two ternary relations \(R \subseteq D^3,\, R' \subseteq D'^3\) equivalent or isomorphic iff there is a bijection \(f:D\rightarrow D'\) such that \((a,b,c)\in R\Leftrightarrow (f(a),f(b),f(c))\in R'\).
A ternary relation \(R\) is a binary operator or bop iff every \((a,b)\in D^2\) uniquely determines \(c\in D\) such that \((a,b,c)\in R\) (so that \(R\) is a function \(D^2\rightarrow D\)). For \(k\in\Bbb N\) a \(k\)-restriction of \(R\) is a domain restriction of \(R\) to a set \(E^2\) such that \(|E|=k\). Two bops \(R_1,R_2\) are \(k\)-similar if for every \(k\)-restriction of \(R_1\) we can find \(k\)-restriction of \(R_2\) which is isomorphic to it, and vice versa. \(k\)-similarity is an equivalence relation, and this is easy to show.
Finally, define the bop-counting function \(\theta(k)\) for \(k\in\Bbb N\) to be the number of equivalence classes under \(k\)-similarity.
==Properties==
By counting the number of possible (up to isomorphism) \(k\)-restrictions of a set, it can be show that \(\theta(k)\) is a function which is at most triply exponential in \(k\) (i.e. it is bounded by \(2^{2^{2^{ck}}}\) for some constant \(c\)). Nevertheless, Friedman has shown that this function is not recursive. This presents algorithmic difficulty in finding values of this function.
A more striking result regards the specific value \(\theta(12)\). Friedman has shown that the statement "\(\theta(12)=N\)", for any natural number \(N\), cannot be proven in any of well-known formal theories such as ZFC, and stronger formal theories including ZFC + I1Harvey Friedman, Impossible Counting (2015) (pp. 9-10), and NBG + "there exists a nontrivial elementary embedding \(j:V\rightarrow V\)" (assuming they are consistent).
We can however try to measure how "close" a theory is to providing exact value of the number, by asking for upper bounds which the theory can provide. To be precise, for theory \(T\), let \(\theta(12,T)\) be the least \(N\) such that \(T \vdash \theta(12) \leq N\). If \(T,T'\) are "standard" large cardinal extensions of ZFC (with term "standard" being intentionally left vague; Friedman defers clarification until a later paper), and both are consistent, then if \(T'\) proves the consistency of \(T\) then \(\theta(12,T') < \theta(12,T)\). This, in a way, shows how bad these theories are at estimating \(\theta(12)\), as even a barely stronger system asserting consistency already shows tighter bound.
==References==
Category:Functions