ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда.

Пять аксиом и первое правило ТТЧ.

Таким образом, нам придется отказаться от простого рецепта, предложенного выше, и пойти по более сложному пути: у нас будут аксиомы и правила вывода. Прежде всего, как было обещано, все правила исчисления высказываний будут использованы в ТТЧ. Итак, первой теоремой ТТЧ будет следующая:

<S0 = 0 V ~ S0 = 0>

Она может быть выведена так же, как <P V ~ P >. Прежде чем приводить правила, давайте запишем пять аксиом. ТТЧ:

АКСИОМА 1: Aa:~Sa=0.

АКСИОМА 2: Aa:(a+0)=a.

АКСИОМА 3: Aa:Ab:(a+Sb)=S(a+b).

АКСИОМА 4: Aa:(a*0)=0.

АКСИОМА 5: Aa:Ab:(a*Sb)=((a*b)+a).

(В строгой версии вместо b используйте a'.) Все они очень просты. Аксиома 1 сообщает что-то о числе 0; аксиомы 2 и 3 говорят о свойствах сложения; аксиомы 4 и 5 говорят о свойствах умножения и о его отношении к сложению.