Big Number Duel

On January 26th 2007, Adam Elga and I got together to see who could come up with a bigger finite number. The event was part of MIT's Independent Activity Period, and was intended as a way to get undergraduates interested in computability theory, infinite ordinals, higher-order languages, the expressive limitations of representational systems and other areas of contact between mathematics and philosophy.

Adam designed an excellent poster for the event, which you can find here.

Here is a brief description of the duel, which is drawn from my book, On the Brink of Paradox.

The duel was reported in The Tech and an interview was broadcast in The Math Factor.

We got the idea for the competition from this article, by Scott Aaronson.

1. The rules of the game
   Contestants take turns writing down expressions denoting natural numbers. Whoever names the biggest number wins.
   The following restrictions apply:
   1. Any unusual notation must be explained to the audience.
      
      
   2. Primitive semantic vocabulary is not allowed.
      (This means that entries like "the smallest number bigger than any number named by a human so far" or "the smallest number that cannot be named using fewer than fourteen English words" are invalid).
      
      
   In addition, there is to be a "gentleman's agreement", to the effect that each new entry must name a number big enough so as to not be reachable in practice using only methods introduced earlier in the game. (This means, for example, that it would be considered unsporting to win by adding one to your opponent's last entry.)
   
   
2. The winning entry
   The winning entry used a philosopher's trick. It is a version of

   The smallest number bigger than any finite number named by an expression in the language of set theory with a googol symbols or fewer.

   in which the primitive semantic term "named" has been replaced by a formula of second-order set-theory containing no primitive semantic vocabulary, so as to to avoid violating restriction (b) above.
   Here's how to write it formally. For [φ] a (Gödel-coded) formula and s a variable assignment, let "Sat([φ],s)" abbreviate the following second-order formula (where the second-order quantifier is understood plurally):

   For all R {
   {for any (coded) formula [ψ] and any variable assignment t
   (R( [ψ],t) ↔
   ( ([ψ] = "x_i ∈ x_j" ∧ t(x_i) ∈ t(x_j)) ∨
   ([ψ] = "x_i = x_j" ∧ t(x_i) = t(x_j)) ∨
   ([ψ] = "(∼θ)" ∧ ∼R([θ],t)) ∨
   ([ψ] = "(θ∧ξ)" ∧ R([θ],t) ∧ R([ξ],t)) ∨
   ([ψ] = "∃x_i (θ)" and, for some an x_i-variant t' of t, R([θ],t'))
   )}   →
   R([φ],s)}
   

   The winning entry is then this:

   The smallest number bigger than every finite number m with the following property: there is a formula φ(x₁) in the language of first-order set-theory (as presented in the definition of "Sat") with less than a googol symbols and x₁ as its only free variable such that: (a) there is a variable assignment s assigning m to x₁ such that Sat([φ(x₁)],s), and (b) for any variable assignment t, if Sat([φ(x₁)],t), then t assigns m to x₁.

   
   
   Note: Philosophers sometimes assume a realist interpretation of set-theory. On this interpretation, set-theoretic expressions have "standard" meanings, which determine a definite truth-value for each sentence of the language, regardless of whether it is in principle possible to know what those truth-values are. (See, for instance, this article by Vann McGee.) During the competition, Adam and I took for granted that the langauge of (second-order) set-theory was interpreted standardly, which guarantees that the final entry corresponds to a definite number. If the langauge had instead been interpreted on the basis of an axiom system, the final entry would have been invalid. This is because every (consistent) axiomatization of the language has non-isomorphic models and there is no guarantee that the final entry will correspond to the same number with respect to different models.