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. 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.

## 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$$, 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 under the assumption. 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.

For example, if $$T$$ is $$\textrm{ZFC}$$ set theory, then $$\textrm{TR}(T,n)$$ is total under the assumption of the $$\Sigma_1$$-soundness of $$\textrm{ZFC}$$ set theory in the base theory, and $$\textrm{TR}(T,2^{1000})$$ coincides with the least transcendental integer. That is why $$\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.

## Source

1. Fish, 超越整数の拡張関数TR, 巨大数論 p.230, 2013.
2. p進大好きbot, 超越整数観察日記, Japanese Googology Wiki user blog.

By Aeton: Okojo numbers · N-growing hierarchy
By 新井 (Arai): Arai's $$\psi$$
By バシク (BashicuHyudora): Primitive sequence number · Pair sequence number · Bashicu matrix system 1/2/3/4
By ふぃっしゅ (Fish): Fish numbers (Fish number 1 · Fish number 2 · Fish number 3 · Fish number 4 · Fish number 5 · Fish number 6 · Fish number 7 · S map · SS map · s(n) map · m(n) map · m(m,n) map) · Bashicu matrix system 1/2/3/4 computation programmes · TR function (I0 function)
By じぇいそん (Jason): Irrational arrow notation · δOCF · δφ · ε function
By 甘露東風 (Kanrokoti): KumaKuma ψ function
By 小林銅蟲 (Kobayashi Doom): Sushi Kokuu Hen
By koteitan: Bashicu matrix system 2.3
By mrna: 段階配列表記 · 降下段階配列表記 · 多変数段階配列表記 · SSAN · S-σ
By Naruyoko Naruyo: Y sequence computation programme · ω-Y sequence computation programme
By Nayuta Ito: N primitive · Flan numbers · Large Number Lying on the Boundary of the Rule of Touhou Large Number 4
By p進大好きbot: Large Number Garden Number
By たろう (Taro): Taro's multivariable Ackermann function
By ゆきと (Yukito): Hyper primitive sequence system · Y sequence · YY sequence · Y function · ω-Y sequence