11,840
pages

The extended function of transcendental integers (Japanese: 超越整数の拡張関数), which is denoted by $$\textrm{TR}$$, is a family of computable large functions coined by a Japanese Googology Wiki user Fish.[1] It extends the computable function which naturally arises from the definition of transcendental integer.

## Definition

Let $$T$$ be a formal theory with a fixed embedding of an arithmetic, and $$n$$ a natural number. Then $$\textrm{TR}(T,n)$$ is defined as the least integer $$N$$ such that for any Turing machine $$M$$, if the termination of $$M$$ is provable in $$T$$ within $$n$$ symbols, then $$M$$ actually halts within $$N$$ steps.

## Common misconceptions

Since the precise definition of the provability is difficult, googologists tend to ignore the actual formulation using Goedel numbers, and intuitively discuss the behaviour. As a result, they tend to state something like "The $$\textrm{TR}(\textrm{ZFC},n)$$ function is ill-defined in $$\textrm{ZFC}$$ set theory because $$\textrm{ZFC}$$ set theory cannot refer to itself due to Berry's paradox" or "the least trancendental integer is ill-defined in $$\textrm{ZFC}$$ set theory because $$\textrm{ZFC}$$ cannot prove its consistency by Goedel's incompleteness theorem". Such statements are not based on actual definitions and proofs, and are in fact wrong. See #Explanation for details.

## Explanation

We are working in a base theory such as $$\textrm{ZFC}$$ set theory, and considering $$T$$ as a formal theory coded in the base theory. For each Turing machine $$M$$ in the base theory, there is a known way to code $$M$$ in an arithmetic, and hence in $$T$$. Therefore the termination of $$M$$ in $$T$$ naturally makes sense. In this way, $$\textrm{TR}$$ function generates a partial function on $$n$$ for each formal theory $$T$$ with a fixed embedding of an arithmetic. If $$T$$ is recursive, then the resulting partial function is computable.

This function $$\textrm{TR}$$ itself is not total, because there are inconsistent formal theories. For example, suppose that the base theory is consistent, $$T$$ is $$\textrm{PA}$$ augmented by the disprovable formula $$0 = S0$$, and $$M$$ is non-terminating. By the principle of explosion, the termination of $$M$$ is provable in $$T$$. If $$n$$ is greater than or equal to the minimum of the symbols of a proof of the termination of $$M$$ in $$T$$, then there is no integer $$N$$ such that $$M$$ halts within $$N$$ steps, because $$M$$ does not halt. Therefore $$\textrm{TR}(T,n)$$ is ill-defined in this case.

Henceforth, we only consider the case where the language of $$T$$ admits at most finitely many constant term symbols, function symbols, and relation symbols, and enumerate the set of variable symbols of $$T$$ as $$x_0, x_1, \ldots$$. For any $$n$$, let $$P_n$$ denote the set of proofs in $$T$$ with at most $$n$$ symbols. Replacement of variables gives an equivalence relation $$\sim_n$$ on $$P_n$$, and every proof belonging to $$P_n$$ is equivalent with respect to $$\sim_n$$ to a proof in the subset $$P'_n \subset P_n$$ of proofs in which no variable with index $$> n$$ occurs. Since $$P'_n$$ is a finite set by the assumption of the finiteness of constant term symbols, function symbols, and relation symbols, there are at most finitely many Turing machines $$M$$ whose terminations are verifiable in $$T$$ within $$n$$ sumbols. Therefore if every Turing machine $$M$$ whose termination is verifiable in $$T$$ within $$n$$ symbols terminates, then the set of halting steps of such Turing machines is a finite set, which admits the supremum $$N$$, and $$\textrm{TR}(T,n)$$ is defined. Here, note that we assumed the condition that every Turing machine $$M$$ whose termination is verifiable in $$T$$ within $$n$$ symbols terminates, and it does not necessarily hold.

Even if $$T$$ is consistent in the sense $$\textrm{Con}(T)$$ holds in the base theory, then $$T$$ might prove the termination of a non-terminating Turing machine. For example, if the base theory is $$\textrm{ZFC}$$ set theory and $$T$$ is $$\textrm{PA} + \neg \textrm{Con}(\textrm{PA})$$, then $$T$$ is consistent but $$\textrm{TR}(T,n)$$ is ill-defined for a sufficiently large $$n \in \mathbb{N}$$, because there is a Turing machine whose termination is equivalent to $$\neg \textrm{Con}(\textrm{PA})$$, which is provable in $$T$$ but is disprovable in the base theory.

In order to ensure "the well-definedness of $$\textrm{TR}(T,n)$$ for any $$n \in \mathbb{N}$$", it suffices to assume a strong assumption called the $$\Sigma_1$$-soundness of $$T$$ in the base theory. Indeed, Japanese Googologist p進大好きbot proved the provability of "the well-definedness of $$\textrm{TR}(T,n)$$ for any $$n \in \mathbb{N}$$" under this assumption.[2] If we just want to define $$\textrm{TR}(T,n)$$ for a specific $$n$$, e.g. $$2^{1000}$$, then we just need a weaker assumption that for any Turing machine $$M$$, if the termination of $$M$$ is provable in $$T$$ within $$n$$ symbols, then $$M$$ actually halts. Using this strategy, p進大好きbot further proved the provability of "the well-definedness of $$\textrm{TR}(T,n)$$" for any $$n$$ given as the formalisation a meta natural number, e.g. $$2^{1000}$$, when $$T$$ is a formalisation of the base theory (without the assumption of the $$\Sigma_1$$-soundness).[2] Furthemore, p進大好きbot extended $$\textrm{TR}$$ function called "巨大数楼閣数" so that the pointwise well-definedness remains to be provable.<ref name="proof"> For koteitan's translation of the proofs and the extension by p進大好きbot into a pdf file, see #External Links.

For example, if $$T$$ is $$\textrm{ZFC}$$ set theory, then the function $$\textrm{TR}(T,n)$$ on $$n \in \mathbb{N}$$ is total under the assumption of the $$\Sigma_1$$-soundness of $$\textrm{ZFC}$$ set theory in the base theory, and the number $$\textrm{TR}(T,n)$$ is well-defined in $$\textrm{ZFC}$$ set theory (withut the assumption of the $$\Sigma_1$$-soundness of $$\textrm{ZFC}$$ set theory) for any $$n$$ given as the formalisation a meta natural number. Since $$\textrm{TR}(T,2^{1000})$$ coincides with the least transcendental integer, $$\textrm{TR}$$ is called the extended function of transcendental integers.

## Specialisation

Fish coined a specific function called $$\textrm{I}0$$ function as $$\textrm{TR}(\textrm{ZFC}+\textrm{I}0,n)$$. Here, $$\textrm{I}0$$ denotes the axiom of the existence of a rank-into-rank cardinal, which is a very strong large cardinal axiom. As Friedman does not coin a specific transcendental integer, Fish does not coin a value of $$\textrm{I}0$$ function.

## Analysis

By the definition, $$\textrm{TR}(T,n)$$ grows faster than any computable function which is provably total in $$T$$. It implies that if a given computable total function is "known to be total", then it is bounded by $$\textrm{TR}(T,n)$$ for a specific choice of $$T$$. For example, almost all known total computable function is bounded by $$\textrm{I}0$$ function.

Although it is arguable whether it is a naive extension of the notion of a transcendental integer, it is significant because it explicitly gives an explanation that a stronger theory directly yields a larger number in a further stronger theory, as Fish pointed out. Therefore it is reasonable to fix and clarify the base theory if we work in a theory stronger than $$\textrm{ZFC}$$ set theory. Otherwise, any total computable function is weaker than $$\textrm{TR}$$ function in the sense above.

A function like $$\textrm{TR}(T,n)$$ with a specific $$T$$ is sometimes "approximated" to $$\textrm{PTO}(T)$$, i.e. the proof-theoretic ordinal of $$T$$, in the fast-growing hierarchy, but the "approximation" does not make sense because the fast-growing hierarchy is well-defined not for an ordinal but for a tuple of an ordinal and a system of fundamental sequences. Unlike smaller ordinals, $$\textrm{PTO}(T)$$ does not possess a fixed system of fundamental sequence, and hence the comparison is meaningless. Since the fast-growing hierarchy heavily depends on the choice of a system of fundamental sequences, the comparison would be quite doubtful even if we could fix a system of fundamental sequences.