Конкретно это ν-зеркальное правило не входит в число правил вывода ПМ, хотя и могло бы. Суть в том, что это правило показывает, как можно механически передвигать символы, игнорируя их смысл, но сохраняя при этом истинность. Это правило достаточно тривиально, но есть и более хитрые, которые занимаются настоящим делом. В этом и есть вся суть символической логики, впервые предложенной Аристотелем; затем она в течение долгих веков по кусочкам развивалась мыслителями, среди которых были Блез Паскаль, Готфрид Вильгельм фон Лейбниц, Джордж Буль, Август де Морган, Готлоб Фреге, Джузеппе Пеано, Давид Гильберт и многие другие. Рассел и Уайтхед просто развивали античную мечту о полной механизации рассуждений более целеустремленно, чем их предшественники.
Механизируя Кредо Математика
Если вы примените правила вывода ПМ к ее аксиомам (к семенам, которые составляют «нулевое поколение» теорем), вы получите некоторое «потомство» – теоремы «первого поколения». Затем снова примените правила к теоремам первого поколения (а также к аксиомам) всеми возможными способами; так вы получите новую охапку теорем – второе поколение. Затем из всего этого варева получится третья охапка теорем, и дальше, до бесконечности, они будут разрастаться как снежный ком. Бесконечная масса теорем ПМ полностью определена начальными семенами и типографскими «правилами роста», которые позволяют создавать новые теоремы из старых.
Нужно ли говорить, что мы надеемся на то, что все механически произведенные теоремы ПМ являются истинными утверждениями теории чисел (т. е. никогда не будет произведено ложное утверждение), и в то же время мы надеемся на то, что все истинные утверждения теории чисел будут механически произведены внутри ПМ (т. е. нет такого истинного утверждения, которое никогда не будет произведено). Первая из этих надежд называется
Короче говоря, мы хотим, чтобы вся бесконечная масса теорем ПМ точно совпадала с бесконечной массой истинных утверждений теории чисел – мы хотим идеального, безупречного соответствия. По крайней мере, этого хотели Рассел и Уайтхед, и они верили, что с ПМ у них получится достичь цели (в конце концов, «
Давайте вспомним Кредо Математика, которое в той или иной форме существовало за много веков до появления Рассела и Уайтхеда:
Первая строка выражает вышеописанную первую надежду – на непротиворечивость. Вторая строка выражает вышеописанную вторую надежду – на полноту. Теперь мы видим, что Кредо Математика очень тесно связано с намерениями Рассела и Уайтхеда. Их целью, однако, было установить Кредо на новый жесткий фундамент с ПМ в качестве пьедестала. Другими словами, там, где Кредо Математика говорит лишь «доказательство», не объясняя, что за этим термином стоит, люди должны были понимать, что это «доказательство внутри ПМ» – вот чего хотели Рассел и Уайтхед.
Сам Гёдель весьма уважал мощь ПМ, это можно увидеть во вводной части его статьи 1931 года:
Развитие математики в направлении большей аккуратности привело – как известно – к тому, что значительные ее территории были формализованы, чтобы доказательства можно было получать согласно нескольким механическим правилам. Наиболее всеобъемлющими из созданных формальных систем являются, с одной стороны, «Принципы математики» (ПМ), а с другой, система аксиом для теории множеств Цермело – Френкеля (позже расширенная Дж. фон Нейманом). Эти две системы настолько обширны, что все методики доказательств, ныне используемые, были формализованы в них, т. е. сжаты до нескольких аксиом и правил вывода.
И все же, несмотря то, как великодушно Гёдель снял шляпу перед трудом Рассела и Уайтхеда, он не верил ни в то, что было достигнуто идеальное соответствие между истиной и теоремами ПМ, ни в то, что такая цель была
Удивительная синхронность шагов