Внимательное рассмотрение логики построения доказательства «Теоремы о неполноте», выявляет ряд нестыковок и противоречий, делающих процедуру доказательства невыполнимой. Самой главной «нестыковкой», наверное, следует считать то, что запись ∀ x ~ Dem(x, sub(y, 13, y)) в символах базового алфавита не представима, а, следовательно, вычислимого по предложенной процедуре номера не имеет. И, таким образом, все действия, связанные с использованием этого номера, осуществлены быть не могут. Это, если кратко. А подробнее можно посмотреть здесь:
https://doi.org/10.24108/preprints-3112874