TR function

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.Fish, 超越整数の拡張関数TR, 巨大数論 p.230, 2013. 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.p進大好きbot, 超越整数観察日記, Japanese Googology Wiki user blog. 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). Furthemore, p進大好きbot extended \(\textrm{TR}\) function called "巨大数楼閣数" so that the pointwise well-definedness remains to be provable. 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.
== External Links ==
* koteitan, a pdf translation of p進大好きbot's proofs of the totality of \(\textrm{TR}(T,n)\) function under the assumption of \(\Sigma_1\)-soundness of \(T\) in the base theory and the pointwise well-definedness for the case \(T\) is the formalisation of the base theory (without the assumption of \(\Sigma_1\)-soundness) and also p進大好きbot's extension "巨大数楼閣数", dropbox.
== Source ==
== See also ==
ja:TR関数
Category:Higher computable level
Category:Functions
Category:Googology in Asia
Category:Numbers by Fish