Well, I know how I would solve this problem if I was sufficiently good at packing really complicated damn programs into 512 characters of C, or if I were allowed, say, 10 kilobytes of code. Start with a large number X, a larger number Y, and a powerful proof system. For all programs of size X, search through all proofs of length Y to see if they prove that X terminates. Multiply the runtimes of all the Xs together, or pick the largest one, it won't make any difference.
In this case it doesn't matter much whether you use second-order logic or first-order logic, because what you can prove syntactically in second-order logic is no different from what you can prove in a many-sorted first-order logic. But you do want to pick a powerful proof system like ZFC that can prove the consistency of whole ordinal hierarchies of weaker systems, rather than something weak like Peano Arithmetic; that will make a rather large difference, because it means you'll be able to prove the termination of large recursive structures of programs that do their own searches through all possible proofs etc.
If anyone can come up with a method of producing substantially larger numbers than this using bounded finite runtimes and programs guaranteed to terminate, I'd be quite interesting in hearing it.
It takes programs from a restricted language in which all programs provably terminate. It doesn't take arbitrary programs and search for termination proofs relative to a powerful proof system. There's, um... a really really really LARGE difference.
Based on the way that sort of termination proof usually works, I'd guess there are some simple tree ordinals which grow faster than that language, and that a program based on them would defeat the winner, but I haven't looked into it in detail so it's only a guess.
In this case it doesn't matter much whether you use second-order logic or first-order logic, because what you can prove syntactically in second-order logic is no different from what you can prove in a many-sorted first-order logic. But you do want to pick a powerful proof system like ZFC that can prove the consistency of whole ordinal hierarchies of weaker systems, rather than something weak like Peano Arithmetic; that will make a rather large difference, because it means you'll be able to prove the termination of large recursive structures of programs that do their own searches through all possible proofs etc.
If anyone can come up with a method of producing substantially larger numbers than this using bounded finite runtimes and programs guaranteed to terminate, I'd be quite interesting in hearing it.