11,055 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.

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

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.

Fish numbers: Fish number 1 · Fish number 2 · Fish number 3 · Fish number 4 · Fish number 5 · Fish number 6 · Fish number 7
Mapping functions: S map · SS map · S(n) map · M(n) map · M(m,n) map
By Aeton: Okojo numbers · N-growing hierarchy
By BashicuHyudora: Primitive sequence number · Pair sequence number · Bashicu matrix system
By Kanrokoti: KumaKuma ψ function
By 巨大数大好きbot: Flan numbers
By Jason: Irrational arrow notation · δOCF · δφ · ε function
By mrna: 段階配列表記 · 降下段階配列表記 · 多変数段階配列表記 · SSAN · S-σ
By Nayuta Ito: N primitive
By p進大好きbot: Large Number Garden Number
By Yukito: Hyper primitive sequence system · Y sequence · YY sequence · Y function
Indian counting system: Lakh · Crore · Tallakshana · Uppala · Dvajagravati · Paduma · Mahakathana · Asankhyeya · Dvajagranisamani · Vahanaprajnapti · Inga · Kuruta · Sarvanikshepa · Agrasara · Uttaraparamanurajahpravesa · Avatamsaka Sutra · Nirabhilapya nirabhilapya parivarta
Chinese, Japanese and Korean counting system: Wan · Yi · Zhao · Jing · Gai · Zi · Rang · Gou · Jian · Zheng · Zai · Ji · Gougasha · Asougi · Nayuta · Fukashigi · Muryoutaisuu
Other: Taro's multivariable Ackermann function · TR function · Arai's $$\psi$$ · Sushi Kokuu Hen

Community content is available under CC-BY-SA unless otherwise noted.