Обсуждаемое «доказательство» проведено в рамках «наивной теории», а заключение доказательства не согласуется с известными фактами в контексте ZFC. На этом основании автор выдвигает предположение о неформализуемости в ZFC предложенных им рассуждений. Timothy Y. Chow дает понять, что несогласованность можно объяснить гораздо более прозаичным способом, и указывает на пробел (строго говоря, ошибку) в предложенных рассуждениях. Кто при этом ошибается и насколько элементарно — вопрос малоинтересный, ибо вкусовой.
P.S. Если кого-то почему-то интересует мое мнение (в чем я, разумеется, сомневаюсь, ибо далеко не спец), то, на мой взгляд, странновато считать элементарной ошибкой указание на элементарную ошибку.
Но я не собираюсь отстаивать это мнение. Если кому-то приятнее считать то рассуждение примером неформализуемого в ZFC доказательства — нет проблем, пусть так считают. Тем не менее — опять-таки, на мой взгляд, — таким способом можно оправдать почти любую лажу в доказательстве чего угодно, недоказуемого в ZFC: мол, в рамках ZFC это рассуждение не канает, а значит, оно неформализуемо в ZFC.
"Доказательство" Finnur Larusson'а в общем случае, не является доказательством в ZFC. Он же сам об этом говорит: 
) то и теория ZFC+EM то же имеет модель (кто бы в этом сомневался 
и 
следует противоречивость ZFC, а без него -- не могу, так как мне, как и Marcin Mostowski, кажется возможным, что во всех моделях ZFC код доказательства 
является "бесконечно большим" (во всяком случае, до тех пор, пока кто-то это не опровергнет).