В формальном методе указанное содержательное рассуждение оформляется в виде такого правила: если доказано предложение B и доказано предложение (¬A ⇒ ¬B), то считается доказанным и предложение A.

Подобные правила носят название правил вывода. Они должны быть перечислены исчерпывающим образом. Их соединение с аксиомами приводит к тому, что некоторые предложения объявляются доказуемыми. Сперва доказуемыми объявляются все аксиомы, а затем провозглашается, что применение любого правила вывода к любым доказуемым предложениям даёт доказуемое предложение.

Проиллюстрируем сказанное на примере того, как в формальном методе доказывается утверждение 0'''' ≠ 0'', содержательный вывод которого из аксиом-утверждений был приведён выше.

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

() ⇒ ¬ ∃ = xy 0'.

() ⇒ ¬ ∃ = xy 0'.

Символы алфавита принято называть буквами, а цепочки букв – словами.

Каждое предложение, таким образом, является словом в только что определённом смысле. Придирчивый читатель может спросить, все ли слова являются предложениями, а если нет, то какой процедурой они, предложения, выделяются среди всех слов. Ответим ему так: для наших локальных целей это знать необязательно, и он может спокойно всюду заменить встречающийся ниже термин «предложение» (коль скоро он представляется ему непонятным) на термин «слово». (Как сказал ещё принц Гамлет, «слова, слова, слова».)

Внимательный читатель заметит, что в выписанном алфавите отсутствует буква ≠. Она излишня, потому что вместо а ≠ b можно писать ¬ (a = b).