Чтобы выразить это правило, нам необходимо ввести кое-какую нотацию.

Давайте запишем правильно сформированную формулу, в которой переменная а свободна:

X{a}

(Там могут встречаться и другие свободные переменные, но нам это неважно.) Тогда запись X{Sa/a} будет обозначать то же самое, с той разницей, что все а будут заменены на Sa. Таким же образом, X{0/а} будет обозначать ту же строку, в которой все а заменены на 0.

Приведем конкретный пример. Пусть X{a} обозначает строчку (0+а)=а. Тогда X{Sa/a} представляет строчку (0+Sa)=Sa, a X{0/a} — строчку (0+0)=0.

(Внимание: эта нотация не является частью ТТЧ; она служит нам лишь для того, чтобы говорить о ТТЧ.)

С помощью этой новой нотации мы можем выразить последнее правило ТТЧ весьма точно:

ПРАВИЛО ИНДУКЦИИ. Предположим, что u — переменная и X{u} — правильно сформированная формула, в которой и свободно. Если и Au