Временно прервём выписывание списка, чтобы сделать два комментария. Первый комментарий: мы только что установили доказуемость предложения ¬ (0′′ = 0). На содержательном уровне это предложение выражает тот интересный факт, что два не равно нолю. Второй комментарий: уже выписанные две строки позволяют заметить одну важную особенность формального метода, отличающую его от метода неформального. Вспомним, что, излагая неформальный метод, аксиому II мы записали так: Не существует такого x, что х' = 0. Ясно, что смысл аксиомы не изменился бы, выбери мы для неё такую запись: Не существует такого y, что у' = 0. Поэтому доказательство утверждения 0'''' ≠ 0'', предъявленное нами в рамках неформального метода, осталось бы прежним. А вот если бы мы в формальном методе заменили аксиому ¬ ∃ х (х' = 0) на аксиому на ¬ ∃ у (у' = 0), то получить предложение ¬ (0'' = 0) нам бы не удалось, поскольку правило ¬ ∃ разрешает подстановку именно вместо буквы x, а не вместо буквы y. Формальный метод на то и называется формальным, что форма записи имеет здесь первенствующее значение. Продолжим список:

3) (х′ = у′) ⇒ (х = y) [Ax. I];

4) (0′′′ = 0′) ⇒ (0′′ = 0) [3; C: x → 0′′, y → 0];

5) ¬ (0'' = 0) ⇒ ¬ (0''' = 0') [4; ⇒ ¬];

6) (0'''' = 0'') ⇒ (0''' = 0') [3; С: х → 0''', у → 0'];