Возникает интересный вопрос: «Каким образом мы можем вывести строчку 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) правило фантазии