Googology Wiki
Advertisement
Googology Wiki

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.

See also

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
See also: Template:Googology in Asia

Advertisement