Непейвода Н.Н. Прикладная логика

Подождите немного. Документ загружается.

13.5. ВОКРУГ ТЕОРЕМЫ ГЁДЕЛЯ

371

∃y A(n, y) ⇔ n ∈ X. Наличие такой формулы следует из аксиомы пере-

числимости. Аналогично, пусть B(n, m) обладает таким же свойством

для Y . Построим теперь по образу Россера формулу

DR(k, n, m, dC(x)e)

(A(n, m) ⇒ Proof(k, dC(n)e, dC(n)e) ⇒

∃i(i < k & Proof(i, d

C(n)e, dC(n)e))) &

(B(n, m) ⇒ Proof(k, d

C(n)e, d

C(n)e) ⇒

∃i(i < k & Proof(i, dC(n)e, dC(n)e))).

(13.15)

Содержательно данная формула означает отсутствие доказатель-

ства

C(n) при n ∈ X и

C(n)

при n ∈ Y . Рассуждениями, анало-

гичными теореме Россера, получаем, что в любом непротиворечивом

расширении арифметики невыводимо

∀x, y DR(x, n, y) при n ∈ X и его

отрицание при n ∈ Y .

Из усиленной формы конструкции Россера следует, что не

существует алгоритмической расширяющейся последовательности те-

орий

, таких, что ∀x, y DR(x, n, y) для каждого n разрешимо хотя бы

в своей Th

f(n)

. В самом деле, тогда мы могли бы любую вычислимую

функцию доопределить до всюду определенной, чего не может быть.

Из сильной непополнимости вытекает ряд результатов, на которые

впервые обратил внимание Подниекс. Есть формулы, для которых не-

разрешимо утверждение об их неразрешимости и т. д., и даже беско-

нечное число утверждений, каждое из которых утверждает неразреши-

мость предыдущего. Не помогают здесь ни переход к более сильным

теориям для проверки неразрешимости, ни даже построение целой по-

следовательности таких теорий.

Обобщая ту же конструкцию Россера, можно получить существова-

ние для любого

n множества n формул, которые не только независимы,

но и взаимно независимы:их булева комбинация доказуема тогда и толь-

ко тогда, когда она является тавтологией. Более того, такие системы мо-

гут порождаться значениями одной и той же формулы. Эти построения

вынесены в задачи для сильных студентов

Все эти рассуждения являются частным случаем того, что незнание гораздо более

разнообразно по своим формам, чем знание. Умножая свое знание, мы еще сильнее

умножаем незнание, поскольку начинаем видеть то, чего не видели раньше, и избавля-

емся от иллюзий, что ответы на многие вопросы, в обыденной жизни считающиеся

однозначными, на самом деле известны. А вообще нужно всегда помнить, что знание

372

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Все приведенные выше общие конструкции являются эффективны-

ми и достаточно простыми построениями. Таким образом, любая тео-

рия преобразуется в пример неразрешимого в ней утверждения, любая

эффективная последовательность теорий — в пример утверждения, не-

разрешимого всеми этими теориями.

Теперь рассмотрим идеи следующей группы результатов. Посколь-

ку сами теории поставляют нам примеры неразрешимых утверждений,

они же должны поставлять и способы своего собственного пополнения,

так, чтобы эти неразрешимые утверждения были решены. Первый из

таких способов пополнения нашел сам Гёдель. Он заметил, что его рас-

суждения в доказательстве теорем неполноты могут быть проведены в

самой теории

, если к ней добавить формулу, выражающую непроти-

воречивость этой теории. Следовательно,

Теорема 13.7. (Теорема Гёделя о непротиворечивости) Непротиво-

речивость достаточно сильной теории не может быть доказана вну-

три нее самой.

Но тогда утверждение о непротиворечивости

является способом

пополнения

, причем таким, который использует лишь неявно имев-

шиеся в виду при построении

предположения (кто же намеренно ис-

пользует противоречивую теорию в математике?)

Появилось предположение, что в некоем принципе можно достичь

доказательства любого истинного предложения арифметики, построив

последовательность расширяющихся теорий, каждая следующая из ко-

торых утверждает непротиворечивость предыдущей. Конечно же, было

как любого отдельного человека, так и всего рода человеческого конечно, зато неве-

жество его бесконечно (хотя бы потенциально). Поэтому люди, рассуждая совместно,

складывают не только свои знания, но и (в первую очередь) свое незнание, и решение,

принятое комитетом,как правило, глупее того, которое произнес бы самый тупой из его

членов.

На самом деле ситуация намного тоньше. Если взять другое кодирование утвержде-

ния о непротиворечивости, идеей которого является повторять конъюнктивно

A и дизъ-

юнктивно ее отрицания столько раз, какова длина рассматриваемого доказательства

то непротиворечивость арифметики можно доказать в самой арифметике. Другое дело,

что это кодирование неявно включает в себя непротиворечивость арифметики. Словом,

нигде в окрестностях теоремы Гёделя не надейтесь на простые и однозначные реце-

пты и истолкования. Поэтому практически все популярные философские комментарии

к этой теореме неверны. Все вышеизложенное можно суммировать следующим обра-

зом: не верьте никаким философским комментариям к теореме Гёделя, кроме изложен-

ных в книге [14] (но и этим тоже не верьте!).

13.5. ВОКРУГ ТЕОРЕМЫ ГЁДЕЛЯ

373

понятно, что простой вычислимой последовательности здесь недоста-

точно, поскольку результаты Подниекса интуитивно предвосхищались

многими крупными логиками с момента осознания теоремы Гёделя. Но

почему не продолжать построение по ординалам?

Оказалось, что непротиворечивость — слишком слабый принцип,

если даже вести расширение по всем ординалам. Она годится лишь для

доказательства утверждений вида

∀x(ϕ(x) = 0),

где ϕ — вычислимая функция. Однако практически одновременно с ре-

зультатами Гёделя появился еще один, гораздо более мощный, чем не-

противоречивость, способ расширения теорий. Конечно же, он интуи-

тивно базируется на гораздо более мощных предпосылках.

Австрийский логик Р. Карнап предложил применять для того, что-

бы гарантировать доказуемость любой истинной формулы, следующее

правило:

A(0), . . . , A(n), . . .

∀x A(x)

Это правило имеет бесконечное число посылок — для всех стандартных

натуральных чисел. Естественно, если рассматривать другую теорию со

стандартной моделью, то посылки правила должны пробегать по всему

универсу данной модели. Карнап считал очевидным, что такого прави-

ла достаточно для полноты теории, но эта очевидность оказалась столь

глубокой теоремой, что была в чуть более слабом виде доказана лишь в

50-х гг., а последние штрихи поставил в начале 70-х гг. А. Г. Драгалин.

Конечно же, понятие доказательства с применением правила Кар-

напа сразу же перестает быть конечным объектом и становится индук-

тивным определением общего вида. Конечно же, эффективно постро-

ить бесконечно много доказательств посылок тоже нельзя, необходимо

иметь общий алгоритм такого доказательства. И поэтому в кон-

це 50-х — начале 60-х гг. стало интенсивно исследоваться формальное

правило Карнапа:

FCR

T h

∀x ∃y Proof

T h

(x, y, dA(x)e)

∀x A(x)

Итак, формальное правило Карнапа заменяет бесконечное число выво-

дов на доказательство выводимости при произвольном x. Непротиворе-

чивость самой Th легко выводится однократным применением правила

374

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Карнапа для доказательств внутри Th. Доказано, что добавление фор-

мального правила Карнапа позволяет вывести многие формулы, не вы-

водимые из непротиворечивости

. Доказано, что для любой истинной

формулы арифметики имеется некоторое кодирование ординалов до ω

такое, что в трансфинитной последовательности теорий, начинающейся

= PA и определяемой правилами



α+1

= Th

∪ FCR

T h

lim

n∈N

где β

— возрастающая последовательность ординалов, определяющая

при данном кодировании предельный ординал α, найдется теория, в ко-

торой выводима данная формула. Но, конечно же, при любом фикси-

рованном кодировании ординалов можно доходить и до ε

, и до более

страшных ординалов, применяемых лишь специалистами по теории до-

казательств, а полноты все равно не будет.

И наконец, рассмотрим вопрос о фрагментах арифметики. Очевид-

но, что уже они неполны. Но есть еще один любопытный эффект непол-

ноты,связанный с тем, что каждый фрагмент арифметики, где индукция

ограничена формулами вида

. . . K

R(~x),

где R — разрешимое отношение, K

— кванторы, существенно слабее

всей арифметики, а именно, непротиворечивость такого фрагмента до-

казывается в следующем. Поэтому в 50-е гг. была доказана теорема, на-

званная парадоксом изобретателя.

Теорема 13.8. (Ван Хао, 1955) Для каждого

n найдется формула вида

∀x R(x) с разрешимым предикатом R, для доказательства которой в

арифметике понадобится индукция по формулам с не менее чем n кван-

торами.

Итак, в арифметике ситуация качественно меняется по сравнению с

исчислением предикатов: теперь использование промежуточных слож-

ных лемм не просто сокращает вывод, а делает его вообще возмож-

ным

Заметим, что принцип рефлексии (13.3) является частным случаем правила Карнапа.

Хотя он не изменяет отношения выводимости, но может значительно укоротить многие

выводы.

Еще одна иллюстрация к необходимости идеальных объектов и сложных формализ-

мов при открытии ‘простых’ теорем.

13.6. ФОРМАЛИЗАЦИЯ НЕФОРМАЛИЗУЕМЫХ ПОНЯТИЙ

375

Упражнения к § 13.5

13.5.1. Докажите, что если система

n формул A

, . . . , A

такова, что

ни одна из конъюнкций

& ∙∙∙ & μ

где каждое из μ

есть пустое слово либо знак отрицания, нераз-

решима, то булева комбинация этих формул выводима ттт, когда

она является тавтологией (такую систему назовем независимой,

аналогично независимой системе множеств).

13.5.2. Постройте независимую систему формул.

13.5.3. Постройте формулу A(x), такую,что при любом n система A(0),

..., A(n) независима.

§ 13.6. ФОРМАЛИЗАЦИЯ НЕФОРМАЛИЗУЕМЫХ

ПОНЯТИЙ

Те, кто верует слепо, — пути не найдут.

Тех, кто мыслит, — сомнения вечно гнетут.

Опасаюсь, что голос раздастся однажды:

«О невежды! Дорога не там и не тут!»

( О. Хайям. [23, стр. 42])

Итак, даже в математике достаточно сложные понятия невозможно

формализовать. Тем не менее мы вовсю пользуемся их формализация-

ми. Более того, компьютеризация всех сфер человеческой деятельности

приводит к (слишком часто неосознанной) формализации и тех поня-

тий, которые всегда трактовались как неформальные. Эта сторона была

впервые ярко подчеркнута Дж. Вейценбаумом

в его книге [9]. Ведь

Дж. Вейценбаум — один из ярчайших (но отнюдь не самых преуспевших) представи-

телей направления, известного под названием ‘искусственный интеллект’. В середине

60-х годов он создал программу ELIZA (названную по имени героини пьесы Б. Шоу

«Пигмалион»), которая имитировала диалог между психоаналитиком и пациентом. Она

не пыталась понять человеческий язык (что было в принципе невозможно на том уров-

не развития компьютеров и информатики), а просто на основе формальных знаний о

синтаксисе фраз возвращала человеку его собственные утверждения в виде вопросов

376

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

любая компьютерная программа заодно является формализацией поня-

тий, с которыми она работает.

И, наконец, компьютеры заставили людей работать со сложными

формализациями, причем они, как идеальные бюрократы, строго следу-

ют букве этих формализаций. И тут выявилось, что даже сложные фор-

мальные понятия человек склонен понимать как неформальные. Более

того, такую особенность человека нельзя высокомерно игнорировать

как недоразвитость. Только на этой основе можно дать понятие ошибки

в языке программирования

Поэтому дальше нельзя игнорировать вопрос о том, что же такое

формализация неформализуемого, как с ней работать и как не попасться

в ловушки, явно имеющиеся в понятии, с самого начала содержащем

внутреннее противоречие.

Пожалуй, первым открыто заговорил о формализации неформализу-

емых понятий новосибирский логик Н. В. Белякин. Он воспользовался

ситуацией, возникшей вокруг теоремы Гёделя о неполноте, для пред-

ставления гуманитарных понятий.

либо замечаний. Некоторые из правил переформулировки были весьма остроумны, на-

пример, на утверждения типа «Никто меня не любит» мог последовать вопрос: «Кого

конкретно Вы имеете в виду?».

Эта программа послужила эффектным экспериментальным опровержением теста

Тьюринга (см. примечание на стр. 356): люди воспринимали программу как вполне ра-

зумного и доброжелательного собеседника.

Столь творческая и критически мыслящая личность, как Вейценбаум, не могла быть

не шокирована тем, что вокруг его программы, которая была наполовину шуткой, на-

половину опровержением почтенной и глубокой гипотезы (Тьюринг, пожалуй, просто

переоценил интеллект среднего человека), поднялся невероятный шум как вокруг вели-

кого достижения искусственного интеллекта. Это навело его на мысль проанализиро-

вать другие “достижения”, знаменитые к началу 70-х гг., и выявившаяся картина была

просто ужасной: воинствующее полузнание, игнорирующее все достижения мировой

гуманитарной и математической мысли,примитивные модели,рекламируемые как уни-

версальный решатель задач, разгул агрессивной саморекламы и профанации. Поэтому

он написал горькую книгу, говорящую о том, что на самом деле происходит не компью-

терная революция, а компьютерная контрреволюция и в науке, и в обществе.

Критерии ошибки в математической формализации достаточно ясны: либо прямое

противоречие, либо расхождение с истинностью в стандартной модели. А вот в описа-

нии алгоритмических языков очень трудно сделать такую ошибку, которая привела бы

к явной невычислимости некоторых конструкций. Поэтому, как ни парадоксально, есть

понятие ошибки в программе, но до сих пор практически нет понятия ошибки в том, на

чем базируются программы: в определении алгоритмических языков.

13.6. ФОРМАЛИЗАЦИЯ НЕФОРМАЛИЗУЕМЫХ ПОНЯТИЙ

377

Основная идея Белякина следующая. Гуманитарное понятие (напри-

мер, любовь, дружба, честь) разъясняется на прецедентах и получает

неявное алгоритмическое определение. Но деятели культуры специали-

зируются на том, что каждый раз, когда такое определение становится

почти фиксированным и общепринятым (когда возникает формализа-

ция), придумывают прецеденты, не подходящие под данное определе-

ние

.С алгоритмической точки зрения это можно уточнить следующим

образом. В каждый данный момент формализация представляет из себя

разрешимое подмножество некоторого идеального образа понятия, не

являющегося даже перечислимым множеством. Каждая формализация

алгоритмически порождает прецедент, входящий в идеальное множе-

ство, но не подходящий под нее саму. Более того, таким свойством обла-

дает и каждая вычислимая последовательность формализаций. Значит,

хотя в некотором смысле формализации неформализуемого понятия по

Белякину и стремятся к идеальному пределу, но любой реальный пре-

дел сам себя помогает опровергнуть (точно так же, как любая непро-

тиворечивая теория сама помогает построить пример неразрешимого в

ней истинного утверждения).

Строго определить систему формализаций неформализуемых поня-

тий можно, базируясь на теореме Гёделя о неполноте и результатах те-

ории алгоритмов и теории доказательств. В самом деле, поскольку по-

нятия неформализуемы, они должны иметь не просто расходящиеся, а

прямо противоречащие друг другу формализации. Далее, поскольку со-

держательные понятия тесно взаимосвязаны друг с другом, есть смысл

рассматривать их совместную формализацию. И наконец, подмеченный

Н. В. Белякиным эффект диагонализации должен, конечно же,иметь ме-

сто. Таким образом, приходим к следующим принципам, которые есте-

ственно принять как постулаты теории неформализуемых понятий.

Принцип 1. Понятия могут описываться лишь в их взаимо-

связи. Совокупность взаимосвязанных понятий может быть

описана как сигнатура

σ (называемой в гуманитарных ис-

следованиях тезаурус)

В частности, отношения Ромео и Джульетты были прецедентом, не подходившим

под почти формализованное в тот момент понятие любви.

Данный постулат не принимался Белякиным, но давно уже использовался (часто

неявно) в работах Тарского, Карнапа, Витгенштейна и др.

378

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Скажем, понятия любви и ревности тесно взаимосвязаны и принадле-

жат одному и тому же тезаурусу.

Принцип 2. Объем понятия является производным от его

содержания и взаимосвязей с другими понятиями

Принцип 3. Для гуманитарных понятий и их объемы, и их

взаимосвязи все время меняются, их нельзя однозначно за-

фиксировать

Принцип 4. Имеется оператор диагонализации, выдающий

по любой эффективно заданной последовательности уточ-

нений рассматриваемых понятий новое уточнение, не со-

впадающее ни с одним из членов последовательности

Принцип 5. Имеется оператор альтернативы, выдающий по

каждой паре уточнений

(Φ

, Φ

), где Φ

расширяет Φ

, но-

вое уточнение Φ

, расширяющее Φ

, но несовместимое с

Принцип 6. Имеются абсолютно общепризнанные соотно-

шения между понятиями (трюизмы), но они — самые бес-

полезные из всех соотношений.

В самом деле, трюизмом является, скажем, описание ревности как от-

рицательного чувства к объекту действительного или предполагаемого

увлечения любимого (любимой). Из этого определения, вполне почтен-

ного для какого-либо научного трактата, никаких позитивных выводов

не сделаешь. Зато принципы (принадлежащие противоположным куль-

турам любовных отношений):

Если ты —джигит,зарежь подонка,посягающего на твою

любимую!

Пожалуй, впервые этот принцип явно сформулировал Карнап.

А это часто утверждали многие гуманитарии, отрицая возможность применения ма-

тематики для анализа их понятий. Ну что же, в данном пункте мы с ними согласны.

Н. В. Белякин.

А этого у него не было, поскольку он первоначально не рассматривал даже отрица-

ние.

13.6. ФОРМАЛИЗАЦИЯ НЕФОРМАЛИЗУЕМЫХ ПОНЯТИЙ

379

Если ты — светский человек, не дай чувству ревности

проявиться наружу!

позитивны, дают конкретную стратегию поведения в соответствующей

ситуации, но полностью несовместимы друг с другом.

Теперь надо строить математическую модель. Следующие принци-

пы говорят уже о формализации только что перечисленных содержа-

тельных положений на базе теоремы Гёделя о неполноте и ее обобще-

ний.

Принцип 7. В каждый данный момент для данной конкрет-

ной цели взаимоотношения понятий описываются как клас-

сическая теория

T h

. Эта теория называется ипостасью

системы неформализуемых понятий.

Заметим, что здесь сделано сильное предположение о том, что каждая

ипостась описывается теорией,применяющей классическую логику.Это

предположение нуждается в проверке, и проверка была произведена в

первой же работе,описывавшей теорию неформализуемых понятий [22].

В ней было показано, что при естественных предположениях (а именно,

принцип 10) уже для неклассической арифметики не удается постро-

ить нетривиальной системы расширений, описывающей арифметиче-

ские понятия как неформализуемые. Таким образом, теория неформа-

лизуемых понятий еще ярче подчеркивает исключительную роль клас-

сической логики в системе известных логик.

Принцип 8. Среди этих теорий есть теория

T h

, являюща-

яся подтеорией любой T h

Принцип 9. Имеется вычислимая функция

ϕ, строящая по

каждой паре теорий T h

⊂ T h

, теорию T h

ϕ(α,β)

, расши-

ряющую T h

, но несовместимую с T h

Таким образом, каждое расширение теории имеет альтернативу.

Следующий принцип также является сильным предположением, по-

казавшим свою эффективность при описании систем неформализуемых

Ипостась — в христианском богословии одно из конкретных проявлений непости-

жимой и бесконечной сущности единого Бога в нашем мире. Ипостасями являются Бог-

Отец, Бог-Сын и Бог-Дух Святой. Аналогичное понятие имеется и в иудаизме.

380

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

понятий. Он говорит о том, что никакой из новых результатов, получен-

ных в расширениях данной ипостаси, не может считаться даже относи-

тельно бесспорным (неопровержимым в других расширениях).

Принцип 10. Пересечением множества теорем всех теорий,

расширяющих

T h

, являются теоремы самой T h

Этот принцип сразу же отметает в качестве основы для систем нефор-

мализуемых понятий теории, базирующиеся на многих известных не-

классических логиках.

Теория неформализуемых понятий позволила дать подходы к реше-

нию некоторых задач, связанных с несоответствием понятий в языках

программирования. Появились и логические следствия. Одно из них мы

приведем здесь.

Определение 13.6.1.

Высказывание

называется

псевдопроблемой

от-

носительно ипостаси

T h

,входящей в систему формализаций неформа-

лизуемых понятий, если ни в какой ипостаси, являющейся расширением

T h

, ни

не являются теоремами.

Предложение 13.6.1. Метод критики оснований. Если A — псевдо-

проблема, B не является псевдопроблемой, B неразрешимо в T h

и в

теории T h

доказано A ⇒ B, то можно подобрать формулу D, не

являющуюся псевдопроблемой, такую, что D ⇒ A и A ⇒ D — не тео-

ремы T h

, а D ⇒ B — ее теорема.

Доказательство. Пусть для определенности

B доказывается в некото-

рых формализациях. Тогда имеется теория T h

, расширяющая T h

, в

которой доказывается B. Но тогда есть конечный список D

аксиом

T h

, из которого выводится B в T h

. Значит, D

⇒ B является тео-

ремой T h

. Поскольку T h

имеет альтернативу T h

ϕ(α,β)

, усилим D

до списка аксиом D, опровергаемого в данной альтернативе. Посколь-

ку A — псевдопроблема, то ни она, ни ее отрицание не выводимы ни в

T h

, ни в T h

ϕ(α,β)

. Отсюда получаем, что четыре импликации

D ⇒ A D ⇒

D ⇒ A

D ⇒

невыводимы в T h

и, соответственно, D — искомое независимое от A

основание.