Naming Large Integers is Naming Strong Logics

Scott Aaronson's Who Can Name the Bigger Number? was recently discussed on the programming subreddit. One of the comments noted the Big Number Duel, which was inspired by Aaronson's article. The winning entry in the duel was

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

I think we can do a little bit better without increasing from 10¹⁰⁰ the number of symbols allowed:

The smallest number bigger than any finite number named by an expression in the language of set theory plus an axiom stating the existence of a proper class of inaccessible cardinals with a googol symbols or less.

Since this theory (ZFC+class of inaccessibles) is stronger than ZFC by itself, I suspect it will define larger integers in the same number of symbols. We could continue along this track by listing larger cardinals and stronger axioms of set theory. This game now becomes essentially Bram Cohen's MineField, in which we are not naming just numbers, but logics.

Besides the Big Number Duel, another test of the "name large integers" game was the C Bignum Bakeoff, which asked contestants to wite a C program that returned a large number. Ralph Loader won by to shoehorning a logic called the Calculus of Constructions into his entry, then simply saying something like "the largest integer definable in the Calculus of Constructions using less than a googol symbols".

The idea of naming finite numbers by extending the strength of not only the working notation but also the working logic is not new; see 0^# and 0^†.