Skip to main content

My first remark is that if you allow players to pick their own theories, but only allow consistent theories to win, then you will not be able to compute the winner of the contest. The reason is that the consistency of a theory is not in general a computable question.

To see this, suppose that we had an algorithm that could compute consistency of any given finite theory. Using it, I claim that we can solve the halting problem. Given any Turing machine program $p$ and input $n$, form the theory $T$ asserting the basic facts of arithmetic (a small fragment of PA suffices), plus the assertion that $p$ never halts on input $n$. If $p$ does halt on input $n$, then this theory is inconsistent. And if it doesn't, then the theory is consistent, being true in the standard model. So if we could check consistency, we could solve the halting problem. Since that is impossible, we cannot check consistency in a computable manner.

My second remark is that if all players work in a fixed consistent theory $T$, but play descriptions of numbers that succeed to define unique numbers provably in the theory $T$, then you still won't be able to compute the winner. For example, perhaps one player plays the definition: the smallest size proof of a contradiction in some theory $S$, if $S$ is inconsistent, otherwise $10$, which $T$ can prove uniquely describes a number, without setttling the question of Con(S). But if another player plays $12$, then you will seem to need to decide Con(S) in order to determine the winner, which is impossible by my previous remarks. 

Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k