Hi!
I would like to know what a computabile large number means for googologists.
I know that it is a large number defined as the output of a computable function, i.e. a Turing machine. However, the ambiguity occurs in the meaning of "defined".
I note that every natural number \(n\) is given as a constant function, which is obviously computable, but I guess that googologists do not agree with the computability of \(n\), unless the constant function is "defined" without using \(n\).
Here, the term "defined" appears again. It is not a definability in the formal logical sense, because every constant function is definable. So the term "defined" is refering to the way googologists declare the definition of a Turing machine.
So I would like to know in what range googologists regard a large number as a computable one. For example, if one defines large numbers in the following ways, then do you think that they are computable one?
(1) One writes sentences describing the explicit behaviour of a Turing machine \(M\), and define a large number as the output \(M(0)\) proving that it actually halts with input \(0\) under ZFC axiom.
(2) One writes sentences describing the explicit behaviour of a Turing machine \(M\), and define a large number as the output \(M(0)\) without proving that it actually halts with input \(0\).
(3) One writes sentences describing the explicit behaviour of a Turing machine \(M\), and define a large number as the output \(M(0)\) proving that it actually halts with input \(0\) under an axiom stronger than ZFC axiom.
(4) One writes sentences characterising a Turing machine \(M\), and define a large number as the output \(M(0)\) proving that the sentence actually defines a Turing machine which actually halts under ZFC axiom.
(5) One writes source codes of a programming languge describing the explicit behaviour of a Turing machine \(M\), and define a large number as the output \(M(0)\) proving that it actually halts with input \(0\) under ZFC axiom.
(6) One writes source codes of a programming languge describing the explicit behaviour of a Turing machine \(M\), and define a large number as the output \(\mathbb{M}(M(0),0)\) of the universal Turing machine \(M\) proving that \(M\) actually halts with input \(0\) and \(\mathbb{M}(M(0),-)\) actually halts with input \(0\) under ZFC axiom.
I believe that (1) and (5) are accepted by almost all googologists, and (2) is not by all googologists.
I add examples of (3),(4), and (6).
(3) The \(FPLCIP(10^{100})\) is of this type. A large function defined in a way using finite promice game is not provably total under ZFC, but is provably total under SMAH+.
(4) The existence of \(10^{100}\)-state \(2\)-colour halting Turing machine \(M\) with the greatest output is provable. So one can define a large number as the output \(M(0)\) with input \(0\).
(6) The transcendental integer and other variants are of this type. For example, the existence of \(n + 10^{100}\)-state \(2\)-colour Turing machine \(M_n\) with a proof that it actually halts under ZFC with \(n + 10^{100}\) or less with the greatest output with input \(0\) is provable, and it is easy to write a source code of a function \(M\) sending \(n\) to the natural number \(M(n)\) corresponding to \(M_n\) through the universal Turing machine \(\mathbb{M}\), So one can define a large number as \(\mathbb{M}(M(0),0)\).
What do you think about them? And why do you think so?