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

Возникает интересный вопрос: «Каким образом мы можем вывести строчку 0=0?» Кажется, что очевидным способом было бы сначала вывести строчку Aa:a=a и затем использовать спецификацию. Как вы думаете, где ошибка в нижеследующем «выводе» Aa:a=a... Можете ли вы ее исправить?

(1) Aa:(a+0)=a   аксиома 2

(2) Aa:a=(a+0)   симметрия

(3) Aa:a=a транзитивность (строчки 2,1)

Я привел это маленькое упражнение, чтобы указать на следующий простой факт: при манипуляции хорошо знакомыми символами, такими, как «=», мы не должны торопиться. Мы должны следовать правилам, а не нашему знанию пассивных значений символов. (Тем не менее, это знание весьма ценно, чтобы помочь нам направить вывод по верному пути.)

Почему спецификация и общность ограничены

Давайте выясним, почему и спецификация, и общность нуждаются в ограничениях Взгляните на следующие две деривации; в каждой из них одно из ограничений нарушено. Обратите внимание, к каким печальным последствиям это привело.

(1)  [                    проталкивание

(2)     a=0             посылка

(3)     Aa:a=0        обобщение (ложно!)

(4)     Sa=0           спецификация

(5)  ]                   выталкивание

(6)        правило фантазии