При помощи букв нашего алфавита запишем аксиомы в виде предложений:

I. (х' = у') ⇒ (x = y);

II. ¬ ∃ х (х' = 0).

Далее сформулируем правила вывода. Каждое правило договоримся записывать в виде дроби, где в числителе – то предложение или те предложения, к которым это правило применяется, в знаменателе – результат применения. В скобках после названия правила пишем его условное обозначение. Правил будет четыре:

Покажем, что предложение ¬ (0'''' = 0'') доказуемо. Для этого предъявим список из девяти доказуемых предложений, справа от каждого из них указав в квадратных скобках причину, по которой оно признаётся доказуемым. Если предложение является аксиомой, указываем номер аксиомы; если оно получается из предыдущих предложений списка по одному из правил, указываем номера этих предложений в списке и это правило. Вот этот список:

1) ¬ ∃ x (x′ = 0) [Ax. II];

2) ¬ (0′′ = 0) [1; ¬ ∃: x → 0′].