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. The duel was later 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 in less 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 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 less.
    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):
    &forall R {
    {for any (coded) formula [ψ] and any variable assignment t
    (R( [ψ],t) ↔
    ( ([ψ] = `x_i ∈ x_j' ∧ t(x_1) ∈ t(x_j)) ∨
    ([ψ] = `x_i = x_j' ∧ t(x_1) = t(x_j)) ∨
    ([ψ] = `(∼θ)' ∧ ∼R([θ],t)) ∨
    ([ψ] = `(θ∧ξ)' ∧ R([θ],t) ∧ R([ξ],t)) ∨
    ([ψ] = `∃x_i (&theta)' and, for some an xi-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 φ(x1) in the language of first-order set-theory (as presented in the definition of `Sat') with less than a googol symbols and x1 as its only free variable such that: (a) there is a variable assignment s assigning m to x1 such that Sat([φ(x1)],s), and (b) for any variable assignment t, if Sat([φ(x1)],t), then t assigns m to x1.


  3. Further Readings