What I'd want to say here is "the largest number nameable using 1000 symbols in second-order logic" (not original, I think someone else won a contest that way). But the fact that someone can ask "Which formulation of second-order logic?" probably defeats this unless you can also, in those fifteen seconds, cite a standard formulation of second-order logic and a standard axiomatization of number in that formulation, otherwise it's an ambiguous specification. HOL is a standard and formal formulation of higher-order logic that I can think of in fifteen seconds, but I wouldn't be able to think of a standard formulation of Peano Arithmetic that was already in HOL.<p>Actually, now that I think of it, "the largest number nameable using 1000 symbols in HOL plus a successor symbol" might work, since you can define addition, multiplication, etc. in higher-order logic using only a successor symbol.<p>Interesting fact: This is a fundamental jump up from first-order logic, which is a fundamental jump up from Busy Beaver, and then once you're there, it's operating at the highest level of abstraction that I know about or have ever heard of. There are things you can do to make that number bigger - picking a different ordinal for the order of logic, recursing over how you get the number of symbols - but they all amount to saying "plus one", and not jumping to a qualitatively different level of abstraction. Once you abstract over second-order logic you are, so far as I know, <i>done</i>.