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.[2] 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[2] 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 "巨大数楼閣数"[2], dropbox.
Source[]
See also[]
By Aeton: Okojo numbers · N-growing hierarchy
By 新井 (Arai): Arai's psi function
By aster: White-aster notation · White-aster
By バシク (BashicuHyudora): Primitive sequence number · Pair sequence number · Bashicu matrix system 1/2/3/4 original idea
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 formalisation · TR function (I0 function)
By Gaoji: Weak Buchholz's function
By じぇいそん (Jason): Irrational arrow notation · δOCF · δφ · ε function
By 甘露東風 (Kanrokoti): KumaKuma ψ function
By koteitan: Bashicu matrix system 2.3
By mrna: 段階配列表記 · 降下段階配列表記 · 多変数段階配列表記 · SSAN · S-σ
By Naruyoko Naruyo: Y sequence formalisation · ω-Y sequence formalisation
By Nayuta Ito: N primitive · Flan numbers (Flan number 1 · Flan number 2 · Flan number 3 · Flan number 4 version 3 · Flan number 5 version 3) · Large Number Lying on the Boundary of the Rule of Touhou Large Number 4 · Googology Wiki can have an article with any gibberish if it's assigned to a number
By Okkuu: Extended Weak Buchholz's function
By p進大好きbot: Ordinal notation associated to Extended Weak Buchholz's function · Ordinal notation associated to Extended Buchholz's function · Naruyoko is the great · Large Number Garden Number
By たろう (Taro): Taro's multivariable Ackermann function
By ゆきと (Yukito): Hyper primitive sequence system · Y sequence original idea · YY sequence · Y function · ω-Y sequence original idea
By バシク (BashicuHyudora): Bashicu matrix system as a notation template
By じぇいそん (Jason): Shifting definition
By mrna: Side nesting
By Nayuta Ito and ゆきと (Yukito): Difference sequence system
By ふぃっしゅ (Fish): Ackermann function
By koteitan: Ackermann function · Beklemishev's worms · KumaKuma ψ function
By Mitsuki1729: Ackermann function · Graham's number · Conway's Tetratri · Fish number 1 · Fish number 2 · Laver table
By みずどら: White-aster notation
By Naruyoko Naruyo: p進大好きbot's Translation map for pair sequence system and Buchholz's ordinal notation · KumaKuma ψ function · Naruyoko is the great
By 猫山にゃん太 (Nekoyama Nyanta): Flan number 4 version 3 · Fish number 5 · Laver table
By Okkuu: Fish number 1 · Fish number 2 · Fish number 3 · Fish number 5 · Fish number 6
By rpakr: p進大好きbot's ordinal notation associated to Extended Weak Buchholz's function · Standardness decision algorithm for Taranovsky's ordinal notation
By ふぃっしゅ (Fish): Computing last 100000 digits of mega · Approximation method for FGH using Arrow notation · Translation map for primitive sequence system and Cantor normal form
By Kihara: Proof of an estimation of TREE sequence · Proof of the incomparability of Busy Beaver function and FGH associated to Kleene's \(\mathcal{O}\)
By koteitan: Translation map for primitive sequence system and Cantor normal form
By Naruyoko Naruyo: Translation map for Extended Weak Buchholz's function and Extended Buchholz's function
By Nayuta Ito: Comparison of Steinhaus-Moser Notation and Ampersand Notation
By Okkuu: Verification of みずどら's computation program of White-aster notation
By p進大好きbot: Proof of the termination of Hyper primitive sequence system · Proof of the termination of Pair sequence number · Proof of the termination of segements of TR function in the base theory under the assumption of the \(\Sigma_1\)-soundness and the pointwise well-definedness of \(\textrm{TR}(T,n)\) for the case where \(T\) is the formalisation of the base theory
By 小林銅蟲 (Kobayashi Doom): Sushi Kokuu Hen
By koteitan: Dancing video of a Gijinka of Fukashigi · Dancing video of a Gijinka of 久界 · Storyteller's theotre video reading Large Number Garden Number aloud
See also: Template:Googology in Asia