(This question is motivated by the reading of the article *Large numbers and unprovable theorems* by Joel Spencer, which can be found at <http://mathdl.maa.org/images/upload_library/22/Ford/Spencer669-675.pdf> and that I recommend).


We all know of the game where a card of a predefined size, say 3x5 cm, is given to every contender, and whoever writes the biggest (positive) integer on his, wins. Naive answers are easily defeated by iteration of fast-growing functions; those are defeated by induction, and these by transfinite induction. However, if a system of axioms is prefixed, then we cannot pursue this strategy forever: for example, if we are only willing to accept Peano's Axioms (PA), then $f\_{\alpha}(n)$ (where $\alpha$ is an ordinal number and $f$ is defined à la Ackermann) is computable (in the sense that the axioms ensure that a program to compute it exists and will terminate in finite time) when $\alpha < \epsilon\_0$, but not if $\alpha = \epsilon\_0$.


This problem suggests two related questions to me:


* It is known that the Ackermann function is well-defined inside AP, and that other functions which grow much faster, like the one in the strong version of the finite Ramsey Theorem of Paris-Harrington, or Goodstein's function whenever it grows fast (I think), or $f\_{\epsilon\_0}(9)$, cannot be defined everywhere just by application of AP, because they "grow too fast for AP". Is there a rigorous definition of what it means for a function to grow too fast for AP (or any other arithmetical axiom system)? Can we establish in any sense a "limit" for this process? For example, can we find a "threshold function" F, depending on the axioms, such that if f dominates F then f is not computable and if F dominates f then it will be? (I'm thinking about something among the lines of the convergence of the p-series for p>0 whenever p>1 and its divergence whenever p<=1).
* Building in the exposition above Spencer observes that, between experts, this game is not funny and reduces to claims of legitimacy (over the validity of the axioms they are supposed to use), since if we allow just a fixed amount of characters for describing our number, and our axioms system is prefixed also, then THERE in fact IS a largest number computable on that system (and thus competitors would come to a draw). However, what happens if we consider the following metagame? Instead of fixing the axiom system beforehand, we allow every contender to (secretly) choose his own system of axioms for arithmetic, in the hope that his will allow faster-growing computable functions than those of the others. Doing this, the contender takes the risk, while trying to get more and more power from the axioms, of actually getting an inconsistent system! Whoever gets the biggest (computable) number in a consistent axiom system wins.
Is this game interesting, or is it "flawed" too? In adittion, inconsistency may be proved within the axiom system, but its consistency would have to be proven in a more powerful framework. Which one would you select and why? What about the metametagame of letting those frameworks to the election of the players? Is that still interesting?



Finding the largest integer describable with a string of symbols of predefined length
My first remark is that if you allow players to pick their own theories, but only allow consistent theories to win, then you will not be able to compute the winner of the contest. The reason is that the consistency of a theory is not in general a computable question. 


To see this, suppose that we had an algorithm that could compute consistency of any given finite theory. Using it, I claim that we can solve the halting problem. Given any Turing machine program $p$ and input $n$, form the theory $T$ asserting the basic facts of arithmetic (a small fragment of PA suffices), plus the assertion that $p$ never halts on input $n$. If $p$ does halt on input $n$, then this theory is inconsistent. And if it doesn't, then the theory is consistent, being true in the standard model. So if we could check consistency, we could solve the halting problem. Since that is impossible, we cannot check consistency in a computable manner. 


My second remark is that if all players work in a fixed consistent theory $T$, but play decriptions of numbers that succeed to define unique numbers provably in the theory $T$, then you still won't be able to compute the winner. For example, perhaps one player plays the definition: *the smallest size proof of a contradiction in some theory $S$, if $S$ is inconsistent, otherwise $10$*, which $T$ can prove uniquely describes a number, without setttling the question of Con(S). But if another player plays $12$, then you will seem to need to decide Con(S) in order to determine the winner, which is impossible by my previous remarks.


