теорема Гёделя о полноте -- 2
ПРОДОЛЖЕНИЕ поста, начатого здесь. Обсуждение проводится по прежнему "адресу".
В данной части поста, я считаю наиболее важными и принципиальными пункты 10 -- 11, где описывается процесс построения модели. Полезно также перечитать пункт 7 -- для тех, кто не знаком с правилами логического рассуждения, которые мы здесь выделяем в качестве основных. В пунктах 8 -- 9 у меня собраны в основном иллюстративные примеры, а в заключительном пункте 12, который мне пришлось разместить в третьей части, идёт серия формальных проверок того, что перед этим было построено. Я вообще-то планировал уложиться в две части, но пришлось сделать три из-за ограничений на длину записей, которая существует в ЖЖ. Так или иначе, я считаю, что на пункт 10 следует обратить особое внимание всем тем, кто в первую очередь интересуется вопросом "из чего же, из чего же, из чего же сделаны наши модели?" :)
7. Прежде всего, я хочу напомнить те основные правила логического рассуждения, которые я выделял в качестве "базовых" в серии предыдущих постов на эту тему. Для того, чтобы сократить число этих правил, мы прежде всего хотим сократить число используемых нами логических связок до отрицания и импликации. Этим мы ничего не теряем, так как все остальные связки через них выражаются. Так, (p or q) есть не что иное как (not(p) -> q), а под (p and q) теперь можно понимать not(not(p) or not(q)). Конечно, сами формулы становятся более громоздкими, если отказаться от связок "или", "и", но нам никто не запрещает их использовать в качестве сокращённых обозначений, что мы далее и будем делать. Но при этом получается, что для исчисления высказываний нам достаточно всего трёх правил логического рассуждения. Напомним их здесь.
(1) Правило Отсечения, или "модус поненс": если доказано A, а также доказано A->B, то разрешается считать доказанным B.
(2) Правило Условного Рассуждения: для доказательства утверждения вида A->B, разрешается принять A в качестве дополнительного предположения (условия), и доказать B при этом условии.
(3) Правило Рассуждения От Противного: для доказательства утверждения B достаточно привести к противоречию утверждение not(B), то есть вывести из него как некоторое утверждение A, так и его отрицание not(A).
Помимо этих правил, мы часто применяем и другие -- например "правило разбора случаев". Но все эти правила можно вывести из правил (1), (2), (3), и в таком качестве далее их использовать. Особенность выписанных правил в том, что они позволяют доказать любой "закон логики" на уровне исчисления высказываний. (То есть без использования логических кванторов.) Под "законом логики" здесь понимается такая формула, которая истинна всегда, независимо от истинностных значений входящих в неё высказывательных переменных.
Однако исчисление высказываний представляет собой довольно узкий фрагмент логики, и для получения "полноценной" картины (способной вобрать в себя "всю математику"), нужно привлекать исчисление предикатов, "устройство" которого я коротко напомнил в предыдущем посте. Для формулировки недостающих правил логического рассуждения (а их будет ещё два), мы минимизируем число используемых нами логических кванторов, оставляя лишь квантор всеобщности. Дело в том, что квантор существования через него выражается следующим образом: если нам надо сказать, что существует некий объект x, удовлетворяющий какому-то условию Ф (оно обычно зависит от x, но мы это здесь не выделяем), то вместо этого можно сказать логически эквивалентную по смыслу вещь. А именно, если мы утверждаем, что Ф выполнено для некоторого x, то мы этим отрицаем? Если бы всё обстояло иначе, то Ф не выполнялось бы никогда. То есть при любом x имело бы место не-Ф. Осталось выписать отрицание этого факта. Таким образом, под (Ex)Ф мы в дальнейшем будем понимать не что иное как not((Ax)(not(Ф))) -- отрицание того, что всегда имеет место не-Ф.
Теперь осталось сформулировать ещё два правила, а также добавить одну небольшую оговорку.
(4) Правило Обобщения: если доказана формула вида Ф(x) для произвольного x, то разрешается считать доказанной формулу (Ax)Ф(x).
(5) Правило Перехода К Частному Случаю: Если доказана формула (Ax)Ф(x), то разрешается считать доказанной формулу Ф(t) для любого выражения t.
Чуть позже мы уточним, что мы далее будем понимать под "выражением". Пока ограничимся тем, что в нашей версии изложения в качестве t можно брать либо переменную, либо константу, но о константах мы поговорим в следующем пункте.
Уточнение, которое требуется сделать, касается правила (2). В отличие от исчисления высказываний, условие A из формулировки правила (2), теперь может зависеть от каких-то переменных, то есть иметь вид A=A(x,y,...,z). И в этом случае, когда мы принимаем A в качестве предположения, то мы его принимаем как бы для фиксированных значений переменных x, y, ..., z. И тогда, по смыслу самого этого предположения, мы не можем в процессе доказательства утверждения B применять правило (4) по отношению ни к одной из переменных x, y, ..., z. Эту оговорку мы сейчас вынесем в качестве "дополнения" к правилу (2).
(*) В процессе условного рассуждения, то есть вывода утверждения B из условия A, не разрешается применять Правило Обобщения к переменным, от которых зависит A.
Может так оказаться, что A не зависит ни от каких переменных -- такие формулы мы далее называем замкнутыми. В этом случае никаких ограничений на условное рассуждение оговорка (*) не накладывает.
8. Сделаем некоторое добавление к описанию языка исчисления предикатов. Нам будет нужно, помимо переменных, использовать также константы, то есть специальные символы, вводимые для обозначения фиксированных объектов. О них вообще-то можно было сказать чуть раньше, но мы решили упомянуть о них именно сейчас. Чем отличаются константы от переменных при их использовании? По сути дела, только тем, что по ним нельзя производить обобщение, то есть "навешивать" квантор всеобщности по этим константам. Если x -- переменная, то формула (Ax)Ф, записываемая также иногда в виде (Ax)Ф(x), всегда имет смысл и разрешена к использованию. Но если c есть символ некой константы, то ни (Ac)Ф, ни (Ac)Ф(c) смысла не имеет и формулой не считается.
Нужно иметь в виду, что константы здесь используются "буквенные", а не "численные". Если нам где-то надо будет использовать какую-то константу типа 13, то для неё следует завести отдельный символ. Про каждую букву, которую мы используем, должно быть указано, используем ли мы её в качестве переменной, или в качестве константы. Обычно "по умолчанию" буква считается переменной, если отстутствует специальная оговорка, что некий символ был выбран нами в качестве константы.
В некоторых других версиях изложения, могут использоваться ещё и так называемые "функциональные символы" для обозначения разного рода математических операций, и с их помощью из переменных и констант можно образовывать всё более и более сложные "выражения" или "термы". Но я уже отмечал, что привлечения символов для обозначения операций можно избежать. Например, вместо двуместного функционального символа f, призванного обозначать сложение чисел, то есть f(x,y) обозначает выражение x+y, можно ввести трёхместный предикатный символ S, где S(x,y,z) означает x+y=z. Та версия, которую я излагаю здесь, оказывается проще, то есть от функциональных символов мы просто отказываемся, и тогда нашими "выражениями" будет всего-навсего переменные и константы. Это, в частности, упрощает применение правила (5).
Ещё здесь надо упомянуть, что иногда вместо "чистого" исчисления предикатов, с котором мы здесь имеем дело, рассматривается так называемое "исчисление предикатов с равенством", где символ = для обозначения равенства входит в "комплект", а все свойства отношения равенства предполагаются выполненными "по умолчанию". Для такой версии изложения также верна теорема Гёделя о полноте, и доказывается она, по сути дела, так же точно. Поэтому мы об этой версии исчисления далее говорить не будем. В учебниках этому вопросу обычно посвящены отдельные параграфы.
Сейчас нам надо сказать кое-что о формулах, которые оказываются истинными всегда -- как бы мы их ни интерпретировали. Чтобы не увеличивать "техническую" часть изложения, ограничимся каким-то простым примером. Пусть у нас имеется "теория", в список обозначений которой входит одна "предметная константа" c, один одноместный предикатный символ P и один двуместный предикатный символ Q. Список "аксиом" теории мы выберем следующим (здесь я делаю это более или менее "наобум"; с таким же успехом можно было написать в качестве примера и что-то другое). Итак:
(Ax)(P(x)->(Ey)Q(x,y))
not((Ex)Q(x,c))
В выписанных нами формулах, буквы c, P и Q не значат пока ничего. Вообще не известно, для каких "нужд" тут они введены. Поэтому сами формулы суть не что иное как чисто синтаксические выражения, не имеющие никакого "смысла". Но им можно придавать разные "смыслы", как-то пытаясь их содержательно интерпретировать. Когда мы строим интерпретацию формул, то прежде всего задаём "предметную область", обозначаемую далее буквой D. Она может состоять из чего угодно, она может быть конечной или бесконечной по нашему усмотрению. Но требуется, чтобы эта совокупность не была "пустой", то есть она включала в себя хотя бы один "объект". Роль "объектов", как уже говорилось, может играть что угодно.
Допустим, мы решили, что D будет множеством целых чисел. Теперь нам надо указать, как мы интерпретируем константу c. Мы должны выбрать для неё значение, равное какому-то фиксированному целому числу. Положим, например, c=0. Далее нужно как-то проинтерпретировать свойство P(x). Произвол в выборе здесь невероятно велик. Мы можем потребовать, чтобы P(x) означало положительность числа x. Можем потребовать вместо этого, чтобы x не превышало 100. А можем потребовать, чтобы P(x) означало, что x было равно либо 3, либо 7, либо 11. То есть абсолютно любое свойство чисел можно взять -- ограничений нет никаких. Остановимся на самой первой из версий, то есть P(x) будет далее означать, что x больше нуля.
Теперь настал черёд проинтерпретировать содержательно, что такое Q(x,y). Вот несколько примеров, что под этим можно было бы понимать: a) x=y; b) x>y; c) x+2y<100; d) x=13; e) x и y совершенно произвольны. Среди всех этих интерпретаций, а также каких угодно остальных, в данном случае мы не ищем что бы то ни было "разумное". Напротив, сейчас важно осознать, что интерпретация может быть какой угодно, в том числе совершенно "дикой".
После того, как интерпретация задана, каждая формула становится высказыванием, то есть она становится истинной или ложной в заданной интерпретации. Когда мы меняем интерпретацию, то может меняться и истинностное значение высказывания. Мы сейчас для c и для P(x) "закрепим" то, что про них было сказано, что есть c полагаем равным нулю, а P(x) у нас означает, что x>0. А вот для Q(x,y) мы будем по отдельности рассматривать каждую из интерпретаций a) - e).
При этом оказывается, что формула (Ax)(P(x)->(Ey)Q(x,y)) окажется истинной во всех этих интерпретациях кроме d). Рекомендуем всем желающим это проверить. Что касается формулы not((Ex)Q(x,c)), то она во всех пяти случаях a) - e) оказывается ложной! Например, в случае a) эта формула утвеждает, что не существует такого целого числа x, которое было бы равно нулю, но это неправда. Таким образом, ни одна из интепретаций для Q, которые нами были рассмотрены, не даёт нам модель нашей "теории". Примеры мы приводили, не заботясь о будущей истинности наших формул. Если бы мы поставили себе целью сделать обе формулы истинными в данной интерпретации, то в качестве Q(x,y) нам можно было бы взять, например, такое условие как 2x+y=1. Тогда вторая из наших формул становится истинной, потому что на самом деле не существует такого целого x, для которого выполнено равенство 2x+c=1, поскольку c=0. И первая формула у нас остаётся истинной, потому что для любого целого x, в том числе и для положительного, найдётся такое целое y, при котором будет верно Q(x,y) -- достаточно положить y=1-2x. Таким образом, рассмотренная нами "теория" имеет "модель". Конечно, это не есть пример какой-то "интересной" теории, для которой существование модели трудно установить -- это не более чем иллюстрация вводимых понятий.
9. Выше мы сказали о том, что такое интерпретация формул, и что такое модель теории. А сейчас следует особо выделить такой класс формул, которые истинны всегда, при любой возможной интерпретации. Про такие формулы можно сказать, что они представляют собой "законы логики" -- при самом широком понимании последних. Их также принято называть "тождественно истинными" формулами, или тавтологиями. Есть также синоним -- "логически общезначимые" формулы.
Приведём несколько примеров тавтологий. Скажем, таковой будет формула (Ax)(P(x)->P(x)): она будет истинна всегда -- как бы мы ни интерпретировали P(x). Это действительно "тавтология" даже в "обыденном" понимании слова -- здесь фактически сказано, что из какого-то высказывания следует оно само. Но не все тавтологии таковы -- среди них бывают очень и очень сложные. Более того, я в самом начале одного из старых своих постов показывал, что любое содержательное утверждение можно сформулировать в виде некоторой тавтологии. Этот аргумент я считаю важным, поэтому не лишне его напомнить.
Допустим, мы доказали какое-то содержательное математическое утверждение T, то есть вывели его из аксиом A, B, ..., C. Если теперь мы составим формулу (A and B and ... and C -> T), то она будет истинна всегда, то есть будет тавтологией. Его надо отличать от самого утверждения T, которое тавтологией, вообще говоря, не будет, и доказательство его "истинности" проведено в предположении "истинности" исходных посылок A, B, ..., C. Однако из этих посылок T выводится уже при помощи рассуждений чисто логических, то есть выписанная нами формула (A and B and ... and C -> T) допускает чисто логическое доказательство, а потому истинна всегда, независимо от своей внутренней "начинки". Знание того, будет ли эта формула тавтологией, равноценна знанию того, выводится ли утверждение T из наших аксиом, а это есть уже некий вполне содержательный факт.
Приведём другие примеры тавтологий, которые менее "очевидны". Например, таковой будет формула (Ey)(Ax)Q(x,y) -> (Ax)(Ey)Q(x,y). Она будет истинна всегда, независимо от того, как и на какой области мы проинтерпретируем Q. Убедиться в этом весьма легко, если вдуматься в смысл того, о чём здесь говорится. Можно также предъявить и чисто логическое доказательство этой тавтологии, опираясь на правила (1) -- (5). Желающие в этом опять-таки могут убедиться.
А вот если мы поменяем местами посылку и заключение, то формула (Ax)(Ey)Q(x,y) -> (Ey)(Ax)Q(x,y) тавтологией уже не будет. Имеется очень много интерпретаций, в которых эта формула оказывается ложной. Например, если в качестве "предметной области" взять множество чисел (натуральных, целых -- каких угодно), а за Q(x,y) принять факт равенства этих чисел, то есть x=y, то можно пронаблюдать, что при этом получится. Посылка импликации окажется истинной, потому что для любого числа x существует число y, равное ему -- это само число x и есть. А вот заключение импликации будет уже ложно: оно утверждает, что существует некоторое "волшебное" число y, которое равно каждому числу x. Понятно, что такого быть не может, и наша импликация оказывается ложной в указанной интерпретации. Тем самым она уже не есть тавтология -- даже если бы оказалось, что во многих других интерпретациях она истинна.
Зададимся теперь вопросом, какой набор правил логического рассуждения можно было бы назвать "полным"? Всё, что можно вывести при помощи этих правил, всегда истинно, при какой бы то ни было интерпретации. То есть логически выводятся "из ничего" только тавтологии, сиречь "логические законы". Но все ли это тавтологии? Теорема Гёделя о полноте как раз и утверждает (в одной из своих формулировок), что все без исключения. Это подтверждает, что система правил логического вывода (1) -- (5) полна в означенном выше смысле.
В самом начале нашего изложения мы формулировали теорему как утверждение о том, что всякая непротиворечивая теория имеет модель, и обещали изложить доказательство. Это сейчас и будет проделано, но для начала мы покажем, почему из этого факта сразу же вытекает выводимость любой тавтологии. Рассуждение очень простое: возьмём произвольную тавтологию Ф. Рассмотрим "теорию", состоящую из одной-единственной формулы not(Ф), которая есть отрицание Ф. Может ли эта теория иметь модель? Очевидно, нет: поскольку Ф -- это тавтология, она истинна во всех интерпретациях. Поэтому not(Ф) ложна во всех интерпретациях, то есть в принципе невозможно указать модель для нашей теории из одной формулы. Тогда отсюда вытекает, что наша теория противоречива (мы опиремся здесь на пока что не доказанный факт о наличии хотя бы одной модели у всякой непротиворечивой теории). Противоречивость означает, что из условия not(Ф) выводится логическое противоречие. Но тогда, согласно правилу (3) рассуждения "от противного", это логически доказывает формулу Ф, что мы и хотели установить.
10. Итак, сейчас нам осталось изложить главную часть -- доказательство того факта, что всякая непротиворечивая теория T имеет модель. Оценим, что нам для этого может потребоваться. Представим себе на время, что искомая модель уже построена, и мы о ней "всё знаем". Тогда для любой замкнутой формулы (то есть формулы, не зависящей от переменных) мы знаем, истинна или ложна она на этой модели. Все формулы нашей теории T должны при этом войти в число истинных формул. То есть теория T станет частью какой-то большей теории T*, состоящей из всех истинных на модели формул. Последняя теория будет непротиворечивой (так как имеет модель), и она кроме всего прочего будет полной, то есть для любой замкнутой формулы Ф она будет содержать либо Ф, либо not(Ф).
Те читатели, которые знакомы с теоремой Гёделя о неполноте, не должны упускать из виду одно обстоятельство: эта знаменитая теорема ни в коем случае не утверждает, что полных непротиворечивых теорий не существует. Они, конечно же, существуют, даже будучи "достаточно сильными", то есть при условии, что они "содержат арифметику". Дело в том, что в теореме о неполноте важнейшим условием является то, что аксиомы теории "явно заданы", то есть существует чисто "механическая" процедура отличения аксиом от всего остального. Но когда мы работаем с классом всех истинных формул (допустим, для той же арифметики), у нас нет в распоряжении средства отличить истинную формулу от не истинной. Наличие такого средства означало бы, что мы вообще досконально изучили "всю математику".
Итак, продолжим наше изложение. Помимо того, что было сказано выше о теории T*, она обладает ещё одной важной особенностью. Представим себе некоторое "всеобщее" утверждение, которое на нашей модели (существование которой мы временно предположили) не выполнено. То есть некоторая формула вида (Ax)Ф(x) является ложной. Согласно определению истинности формул (вытекающему из содержательной трактовки квантора всеобщности), формула Ф(x) должна быть ложна на некотором элементе d предметной области D нашей модели. При этом удобно расширить наш язык, пополнив его новыми константами -- элементами множества D, из которых состоит модель. В этом случае Ф(d) получится формулой, и тогда она должна принадлежать теории T* (с учётом "обогащения" языка, которое мы сделали). Поэтому далее мы можем попытаться построить такую непротиворечивую теорию T*, которая содержала бы T, была полной, а также для любого "всеобщего" утверждения, которое не должно быть истинным, содержала бы частный пример, указывающий на то, на каком именно элементе не выполняется условие вида Ф(x).
Проведённый выше анализ позволяет ответить на вопрос, из чего следует пытаться строить модель. Ведь поначалу это совершенно не ясно: у нас есть лишь набор формул без какой-либо содержательной интерпретации. И потому оcтаётся открытым вопрос о "строительном материале". В любом случае, мы собираемся строить модель из каких-то букв, символов. Но каков содержательный смысл этих символов? Сделанные нами рассуждения "эвристического" характера подсказывают, что модель должна строиться из контрпримеров к "всеобщим" утверждениям теории. Здесь подразумеваются, конечно, те всеобщие утверждения, которые "не верны". В нашем случае это будет означать, что в той теории, которую мы будем строить, расширяя T (и имея в виду получение теории T*), часть "всеобщих" (то есть начинающихся с квантора всеобщности) утверждений будет опровергаться. И вот из контрпримеров к ним мы и будем строить модель.
Мы ограничимся при нашем доказательстве случаем, когда множество символов теории является счётным, то есть эти символы можно занумеровать натуральными числами. Хотя не всякое множество таково (скажем, точки прямой занумеровать нельзя в силу классической теоремы Кантора -- их оказывается "слишком много"), этот случай будет рассмотрен нами как основной, так как на нём проще всего проследить "пружины" доказательства. В конце мы сделаем замечание, касающееся того, как можно перенести это доказательство и на самый общий случай.
Наша стратегия будет такой: мы будем постепенно расширять теорию T с обязательным условием, что при расширении мы не теряем свойство непротиворечивости, за чем мы будем постоянно следить. Помимо добавления новых утверждений к теории, мы будем расширять и её "сигнатуру", то есть в данном случае -- набор предметных констант. Это расширение будет делаться посредством бесконечной серии этапов, и на каждом этапе у нас будет иметься некая непротиворечивая теория S, содержащая T. Опишем сейчас две основные операции, которые мы будем осуществлять на каждом этапе.
Прежде всего, мы будем строить пополнение теории S следующим образом. Занумеруем каким-то образом все замкнутые формулы теории S. Их будет бесконечно много; обозначим их через Ф1, Ф2, ..., Фn, ... . Идя вдоль этого бесконечного списка, мы каждую очередную формулу будем либо присоединять к нашей теории, либо пропускать. Руководствуемся мы при этом одним очень простым правилом. Если присоедиение очередной формулы Фn к уже имеющейся на данном шаге теории приводит к противоречию, то мы эту формулу пропускаем, а в противном случае -- присоединяем. Такая процедура гарантирует непротиворечивость того, что мы имеем, просто по построению. В результате этого бесконечного процесса присоединения к теории новых формул, из теории S возникает непротиворечивая теория, которую мы будем обозначать через C(S) и называть "пополнением" теории S. Принцип её построения очень простой: мы хотим "определиться" по каждому вопросу, который в принципе может возникнуть, и мы при этом соглашаемся со всем, с чем в принципе можем согласиться, избегая возникновения противоречий.
Тут уместно напомнить, что непротиворечивость теории, возникающей после просмотра очередной формулы списка имеет место в силу выбранного нами принципа, и потому C(S) тоже непротиворечива в силу уже звучавшего однажды соображения. Противоречие, которое следует из бесконечного множества формул, следут также и из конечной "части" этого множества -- просто в силу того, что в любом доказательстве, представляющем собой текст конечной длины, мы ссылаемся лишь на конечное число "аксиом". Поэтому, если бы противоречие возникло после присоединения бесконечного числа формул, нами добавленных, то оно возникло бы на каком-то конечном шаге, чего быть не может. Ещё было бы естественно обосновать, почему теория C(S) получается полная, что оправдывало бы её название. Этот факт хотя и верен, но он нам не нужен: мы после завершения всего "строительства" проверим полноту той теории, которая нам будет реально нужна.
Теперь опишем вторую операцию, которую мы будем осуществлять по отношении к теориям. Это как раз и есть то самое расширение "алфавита" предметных констант -- с присоединением новых утверждений с участием этих символов. Как мы сказали, возникновение каждой новой константы мы связываем с обнаружением "всеобщего" утверждения, которое "не выполняется". В последнем мы можем быть уверены тогда, когда мы располагаем отрицанием такого утверждения, то есть имеющаяся на тот момент теория у нас содержит формулу вида not((Ax)Ф(x)). По своему смыслу, эта формула означает существование "контрпримера" к Ф, то есть такого x, для которого выполнено not(Ф(x)). То есть это на самом деле есть утверждение о существовании чего-то. Хотя мы отказались от использования квантора существования, но такие формулы мы далее будем называть "экзистенциальными", или E-формулами. А всю операцию в целом, которую сейчас опишем -- экзистенциальным пополнением теории S. Обозначаться она будет через Ex(S).
Строится она вот как. Прежде всего, все E-формулы теории S мы нумеруем. Это даёт нам бесконечный список, идя вдоль которого мы на каждом шаге будем работать с какой-то E-формулой вида not((Ax)Ф(x)). Мы будем всякий раз добавлять свою константу d для каждой такой формулы (я использую "общее" обозначение d, дабы не вводить серию букв с индексами) и добавляем к теории новую формулу not(Ф(d)), смысл которой в том, что Ф не выполнено на элементе d.
Это ключевой момент доказательства. Нужно обосновать, почему присоединение такой формулы не приводит нас к противоречию. Допустим, что противоречие всё-таки возникло. Поскольку предыдущая теория была непротиворечивой, это означает, что в ней выводимо отрицание той формулы, которую мы присоединили. То есть выводима формула Ф(d) -- опять же в силу рассуждения "от противного": коль скоро отрицание Ф(d) ведёт к противоречию, то это доказывает Ф(d). (Ещё точнее было бы сказать, что эта выводимость имеет место в той теории, которая была на предыдущем шаге, и к которой мы добавили новый символ d в качестве предметной константы.) Теперь сделаем вот что: в имеющемся доказательстве заменим во всех формулах "свежую константу" d, которая ни в одной из формул теории ранее не встречалась, на какую-то переменную x, которая также в доказательстве не использовалась. Что мы этим получим? Не что иное, как вывод формулы Ф(x). Если мы теперь применим правило (4), то это позволяет нам считать доказанной "обобщённую" формулу, то есть (Ax)Ф(x). Заметим, что этот вывод может быть осуществлён в теории, которая была у нас до того, как мы добавили новую формулу. Однако в этой теории у нас была формула not((Ax)Ф(x)), которая прямо противоречит тому, что мы вывели. Такого быть не может, так как у нас все рассматриваемые теории непротиворечивы. То есть мы показали этим рассуждением, что наше допущение о возникновении противоречия после добавления новой формулы Ф(d), приводит нас к ситуации, которой быть не может. Следовательно, после присоединения новой формулы противоречия не будет.
11. Мы прошли сейчас как бы через "перевал". Далее последует относительно лёгкий "спуск". Мы строим "экзистенциальное пополнение" теории S, добавляя новые константы и новые формулы, и получаем в итоге непротиворечивую теорию Ex(S). Это завершает описание второй важной операции, которую мы будем применять к нашим теориям. Теперь вот как будет выглядеть основная конструкция, которая также будет строиться по шагам. Мы последовательно будем строить теории T0, T1, ..., Tn, ... , где в качестве T0 будет взята сама наша "изначальная" теория T, для которой мы хотим построить модель. Теория T1 получается из неё так: мы сначала применяем к T0 первую операцию (то есть "пополнение"), а потом к получившейся теории -- вторую операцию ("экзистенциальное пополнение"). Точно так же строим T2: пополняем T1, и "экзистенциально пополняем" то, что при этом получается. Можно записать общее правило перехода от теории Tn к "следующей" теории Tn+1 в виде формулы:
Tn+1 = Ex(C(Tn))
В итоге у нас возникает расширяющаяся "цепочка" теорий, каждая из которых является частью всех остальных. В силу того, что обе операции сохраняют непротиворечивость теорий, каждая наша теория Tn будет непротиворечива. Объединение всех этих "расширяющихся" теорий мы обозначим через T*, и оно тоже будет непротиворечиво как теория. Сейчас нам нужно проверить, что полученная теория полна. Напомним, что это означает: что для любой замкнутой формулы Ф, у нас либо сама Ф, либо её отрицание принадлежит T*.
Формула Ф может содержать константы, которые мы добавляли в процессе наших построений. Но этих констант в любом случае конечное число, и на каком-то n-м шаге все они были уже добавлены. Это означает, что при переходе от теории Tn к теории Tn+1, на этапе построения пополнения теории Tn, мы непременно просматривали формулу Ф в числе прочих замкнутых формул. Каждую из просматриваемых формул мы либо присоединяли, либо отвергали. И если мы присоединили Ф, то доказывать нечего: она у нас входит в T*. А что значит, что мы её отвергли? Это значит, что её присоединение к теории в момент рассмотрения приводило бы к логическому противоречию. Тогда присоединение Ф к более "широкой" теории T* тем более должно приводить к противоречию. Запомним это, и применим те же соображения к формуле not(Ф), которая тоже замкнута, и содержит те же константы. Если мы её присоединяли в процессе просмотра, то доказывать опять-таки нечего. А если отвергли, то присоединение not(Ф) к T* даёт противоречивую теорию. Мы вообще-то уже анализировали такую ситуацию, и знаем, что это значит: мы сначала выводим из not(Ф) противоречие, оставаясь в пределах теории T*. Затем, применяя правило (3), мы тем самым "от противного" выводим Ф в теории T*. Но присоединение к теории T* её логического следствия, каковым является Ф, ни к какому противоречию приводить не может, поскольку T* непротиворечива. Осталось сравнить это с тем, что мы запомнили выше, откуда станет ясно, что T* обязана быть полной.
Итак, мы осуществили своего рода "программу-минимум", построив ту теорию T*, о которой мы говорили в ходе наших "эвристических" рассуждений. Как же теперь построить модель? Понятно, что в качестве предметной области D надо взять не что иное как множество всех предметных констант, добавляемых нами в ходе всего процесса. Это будет некое счётное множество. Теперь надо проинтерпретировать символы нашего языка, на котором пишутся формулы теории T. Мы проинтерпретируем сразу все символы "объемлющей" теории T*, причём константы можно не интерпретировать -- они как бы "играют самих себя", так как входят в предметную область. Интерпретировать нужно лишь предикатные символы. Пусть P -- один из таких символов, и пусть он будет k-местным. Ему надо сопоставить отношение на D, тоже k-местное, то есть про любой упорядоченный набор из k элементов множества D (не обязательно различных), нужно сказать, в каком случае мы считаем, что эти элементы находятся в рассматриваемом отношении. Решение вопроса тут напрашивается само собой: надо подставить эти элементы в роли констант в предикат P, что даст нам замкнутую формулу вида P(d1,..., dk). Теории T* принадлежит либо сама эта формула, либо её отрицание, причём ввиду непротиворечивости верно только одно из этих положений. Если формула входит в T*, то считаем, что наши элементы предметной области находятся в данном отношении, а если не входит, то не находятся. Мы сделали не что иное, как "содержательно" проинтерпретировали предикатный символ P, и так следует поступить с каждым из символов.
Поскольку интерпретация построена, то про каждую замкнутую формулу языка теории T* можно говорить, истинна или ложна она в этой интерпретации. Чего нам не хватает? Мы хотим доказать, что все положения теории T в построенной интерпретации истинны. То есть получена искомая модель M теории T. Для того, чтобы сделать этот последний шаг в нашем доказательстве (являющийся по сути проверкой) мы докажем вот что: всякая замкнутая формула теории T* истинна на M (то есть в построенной интерпретации) тогда и только тогда, когда эта формула принадлежит T*. Иными словами, мы хотим проверить то, что T* есть не что иное как список всех истин, касающихся M. Хочется назвать M словом "модель", но пока это преждевременно, так как M пока что есть лишь интерпретация теории (с предметной областью D), и мы сейчас проверим, что это в самом деле модель теории T (и даже теории T*).
ПРОДОЛЖЕНИЕ (часть 3)
К ОБСУЖДЕНИЮ
В данной части поста, я считаю наиболее важными и принципиальными пункты 10 -- 11, где описывается процесс построения модели. Полезно также перечитать пункт 7 -- для тех, кто не знаком с правилами логического рассуждения, которые мы здесь выделяем в качестве основных. В пунктах 8 -- 9 у меня собраны в основном иллюстративные примеры, а в заключительном пункте 12, который мне пришлось разместить в третьей части, идёт серия формальных проверок того, что перед этим было построено. Я вообще-то планировал уложиться в две части, но пришлось сделать три из-за ограничений на длину записей, которая существует в ЖЖ. Так или иначе, я считаю, что на пункт 10 следует обратить особое внимание всем тем, кто в первую очередь интересуется вопросом "из чего же, из чего же, из чего же сделаны наши модели?" :)
7. Прежде всего, я хочу напомнить те основные правила логического рассуждения, которые я выделял в качестве "базовых" в серии предыдущих постов на эту тему. Для того, чтобы сократить число этих правил, мы прежде всего хотим сократить число используемых нами логических связок до отрицания и импликации. Этим мы ничего не теряем, так как все остальные связки через них выражаются. Так, (p or q) есть не что иное как (not(p) -> q), а под (p and q) теперь можно понимать not(not(p) or not(q)). Конечно, сами формулы становятся более громоздкими, если отказаться от связок "или", "и", но нам никто не запрещает их использовать в качестве сокращённых обозначений, что мы далее и будем делать. Но при этом получается, что для исчисления высказываний нам достаточно всего трёх правил логического рассуждения. Напомним их здесь.
(1) Правило Отсечения, или "модус поненс": если доказано A, а также доказано A->B, то разрешается считать доказанным B.
(2) Правило Условного Рассуждения: для доказательства утверждения вида A->B, разрешается принять A в качестве дополнительного предположения (условия), и доказать B при этом условии.
(3) Правило Рассуждения От Противного: для доказательства утверждения B достаточно привести к противоречию утверждение not(B), то есть вывести из него как некоторое утверждение A, так и его отрицание not(A).
Помимо этих правил, мы часто применяем и другие -- например "правило разбора случаев". Но все эти правила можно вывести из правил (1), (2), (3), и в таком качестве далее их использовать. Особенность выписанных правил в том, что они позволяют доказать любой "закон логики" на уровне исчисления высказываний. (То есть без использования логических кванторов.) Под "законом логики" здесь понимается такая формула, которая истинна всегда, независимо от истинностных значений входящих в неё высказывательных переменных.
Однако исчисление высказываний представляет собой довольно узкий фрагмент логики, и для получения "полноценной" картины (способной вобрать в себя "всю математику"), нужно привлекать исчисление предикатов, "устройство" которого я коротко напомнил в предыдущем посте. Для формулировки недостающих правил логического рассуждения (а их будет ещё два), мы минимизируем число используемых нами логических кванторов, оставляя лишь квантор всеобщности. Дело в том, что квантор существования через него выражается следующим образом: если нам надо сказать, что существует некий объект x, удовлетворяющий какому-то условию Ф (оно обычно зависит от x, но мы это здесь не выделяем), то вместо этого можно сказать логически эквивалентную по смыслу вещь. А именно, если мы утверждаем, что Ф выполнено для некоторого x, то мы этим отрицаем? Если бы всё обстояло иначе, то Ф не выполнялось бы никогда. То есть при любом x имело бы место не-Ф. Осталось выписать отрицание этого факта. Таким образом, под (Ex)Ф мы в дальнейшем будем понимать не что иное как not((Ax)(not(Ф))) -- отрицание того, что всегда имеет место не-Ф.
Теперь осталось сформулировать ещё два правила, а также добавить одну небольшую оговорку.
(4) Правило Обобщения: если доказана формула вида Ф(x) для произвольного x, то разрешается считать доказанной формулу (Ax)Ф(x).
(5) Правило Перехода К Частному Случаю: Если доказана формула (Ax)Ф(x), то разрешается считать доказанной формулу Ф(t) для любого выражения t.
Чуть позже мы уточним, что мы далее будем понимать под "выражением". Пока ограничимся тем, что в нашей версии изложения в качестве t можно брать либо переменную, либо константу, но о константах мы поговорим в следующем пункте.
Уточнение, которое требуется сделать, касается правила (2). В отличие от исчисления высказываний, условие A из формулировки правила (2), теперь может зависеть от каких-то переменных, то есть иметь вид A=A(x,y,...,z). И в этом случае, когда мы принимаем A в качестве предположения, то мы его принимаем как бы для фиксированных значений переменных x, y, ..., z. И тогда, по смыслу самого этого предположения, мы не можем в процессе доказательства утверждения B применять правило (4) по отношению ни к одной из переменных x, y, ..., z. Эту оговорку мы сейчас вынесем в качестве "дополнения" к правилу (2).
(*) В процессе условного рассуждения, то есть вывода утверждения B из условия A, не разрешается применять Правило Обобщения к переменным, от которых зависит A.
Может так оказаться, что A не зависит ни от каких переменных -- такие формулы мы далее называем замкнутыми. В этом случае никаких ограничений на условное рассуждение оговорка (*) не накладывает.
8. Сделаем некоторое добавление к описанию языка исчисления предикатов. Нам будет нужно, помимо переменных, использовать также константы, то есть специальные символы, вводимые для обозначения фиксированных объектов. О них вообще-то можно было сказать чуть раньше, но мы решили упомянуть о них именно сейчас. Чем отличаются константы от переменных при их использовании? По сути дела, только тем, что по ним нельзя производить обобщение, то есть "навешивать" квантор всеобщности по этим константам. Если x -- переменная, то формула (Ax)Ф, записываемая также иногда в виде (Ax)Ф(x), всегда имет смысл и разрешена к использованию. Но если c есть символ некой константы, то ни (Ac)Ф, ни (Ac)Ф(c) смысла не имеет и формулой не считается.
Нужно иметь в виду, что константы здесь используются "буквенные", а не "численные". Если нам где-то надо будет использовать какую-то константу типа 13, то для неё следует завести отдельный символ. Про каждую букву, которую мы используем, должно быть указано, используем ли мы её в качестве переменной, или в качестве константы. Обычно "по умолчанию" буква считается переменной, если отстутствует специальная оговорка, что некий символ был выбран нами в качестве константы.
В некоторых других версиях изложения, могут использоваться ещё и так называемые "функциональные символы" для обозначения разного рода математических операций, и с их помощью из переменных и констант можно образовывать всё более и более сложные "выражения" или "термы". Но я уже отмечал, что привлечения символов для обозначения операций можно избежать. Например, вместо двуместного функционального символа f, призванного обозначать сложение чисел, то есть f(x,y) обозначает выражение x+y, можно ввести трёхместный предикатный символ S, где S(x,y,z) означает x+y=z. Та версия, которую я излагаю здесь, оказывается проще, то есть от функциональных символов мы просто отказываемся, и тогда нашими "выражениями" будет всего-навсего переменные и константы. Это, в частности, упрощает применение правила (5).
Ещё здесь надо упомянуть, что иногда вместо "чистого" исчисления предикатов, с котором мы здесь имеем дело, рассматривается так называемое "исчисление предикатов с равенством", где символ = для обозначения равенства входит в "комплект", а все свойства отношения равенства предполагаются выполненными "по умолчанию". Для такой версии изложения также верна теорема Гёделя о полноте, и доказывается она, по сути дела, так же точно. Поэтому мы об этой версии исчисления далее говорить не будем. В учебниках этому вопросу обычно посвящены отдельные параграфы.
Сейчас нам надо сказать кое-что о формулах, которые оказываются истинными всегда -- как бы мы их ни интерпретировали. Чтобы не увеличивать "техническую" часть изложения, ограничимся каким-то простым примером. Пусть у нас имеется "теория", в список обозначений которой входит одна "предметная константа" c, один одноместный предикатный символ P и один двуместный предикатный символ Q. Список "аксиом" теории мы выберем следующим (здесь я делаю это более или менее "наобум"; с таким же успехом можно было написать в качестве примера и что-то другое). Итак:
(Ax)(P(x)->(Ey)Q(x,y))
not((Ex)Q(x,c))
В выписанных нами формулах, буквы c, P и Q не значат пока ничего. Вообще не известно, для каких "нужд" тут они введены. Поэтому сами формулы суть не что иное как чисто синтаксические выражения, не имеющие никакого "смысла". Но им можно придавать разные "смыслы", как-то пытаясь их содержательно интерпретировать. Когда мы строим интерпретацию формул, то прежде всего задаём "предметную область", обозначаемую далее буквой D. Она может состоять из чего угодно, она может быть конечной или бесконечной по нашему усмотрению. Но требуется, чтобы эта совокупность не была "пустой", то есть она включала в себя хотя бы один "объект". Роль "объектов", как уже говорилось, может играть что угодно.
Допустим, мы решили, что D будет множеством целых чисел. Теперь нам надо указать, как мы интерпретируем константу c. Мы должны выбрать для неё значение, равное какому-то фиксированному целому числу. Положим, например, c=0. Далее нужно как-то проинтерпретировать свойство P(x). Произвол в выборе здесь невероятно велик. Мы можем потребовать, чтобы P(x) означало положительность числа x. Можем потребовать вместо этого, чтобы x не превышало 100. А можем потребовать, чтобы P(x) означало, что x было равно либо 3, либо 7, либо 11. То есть абсолютно любое свойство чисел можно взять -- ограничений нет никаких. Остановимся на самой первой из версий, то есть P(x) будет далее означать, что x больше нуля.
Теперь настал черёд проинтерпретировать содержательно, что такое Q(x,y). Вот несколько примеров, что под этим можно было бы понимать: a) x=y; b) x>y; c) x+2y<100; d) x=13; e) x и y совершенно произвольны. Среди всех этих интерпретаций, а также каких угодно остальных, в данном случае мы не ищем что бы то ни было "разумное". Напротив, сейчас важно осознать, что интерпретация может быть какой угодно, в том числе совершенно "дикой".
После того, как интерпретация задана, каждая формула становится высказыванием, то есть она становится истинной или ложной в заданной интерпретации. Когда мы меняем интерпретацию, то может меняться и истинностное значение высказывания. Мы сейчас для c и для P(x) "закрепим" то, что про них было сказано, что есть c полагаем равным нулю, а P(x) у нас означает, что x>0. А вот для Q(x,y) мы будем по отдельности рассматривать каждую из интерпретаций a) - e).
При этом оказывается, что формула (Ax)(P(x)->(Ey)Q(x,y)) окажется истинной во всех этих интерпретациях кроме d). Рекомендуем всем желающим это проверить. Что касается формулы not((Ex)Q(x,c)), то она во всех пяти случаях a) - e) оказывается ложной! Например, в случае a) эта формула утвеждает, что не существует такого целого числа x, которое было бы равно нулю, но это неправда. Таким образом, ни одна из интепретаций для Q, которые нами были рассмотрены, не даёт нам модель нашей "теории". Примеры мы приводили, не заботясь о будущей истинности наших формул. Если бы мы поставили себе целью сделать обе формулы истинными в данной интерпретации, то в качестве Q(x,y) нам можно было бы взять, например, такое условие как 2x+y=1. Тогда вторая из наших формул становится истинной, потому что на самом деле не существует такого целого x, для которого выполнено равенство 2x+c=1, поскольку c=0. И первая формула у нас остаётся истинной, потому что для любого целого x, в том числе и для положительного, найдётся такое целое y, при котором будет верно Q(x,y) -- достаточно положить y=1-2x. Таким образом, рассмотренная нами "теория" имеет "модель". Конечно, это не есть пример какой-то "интересной" теории, для которой существование модели трудно установить -- это не более чем иллюстрация вводимых понятий.
9. Выше мы сказали о том, что такое интерпретация формул, и что такое модель теории. А сейчас следует особо выделить такой класс формул, которые истинны всегда, при любой возможной интерпретации. Про такие формулы можно сказать, что они представляют собой "законы логики" -- при самом широком понимании последних. Их также принято называть "тождественно истинными" формулами, или тавтологиями. Есть также синоним -- "логически общезначимые" формулы.
Приведём несколько примеров тавтологий. Скажем, таковой будет формула (Ax)(P(x)->P(x)): она будет истинна всегда -- как бы мы ни интерпретировали P(x). Это действительно "тавтология" даже в "обыденном" понимании слова -- здесь фактически сказано, что из какого-то высказывания следует оно само. Но не все тавтологии таковы -- среди них бывают очень и очень сложные. Более того, я в самом начале одного из старых своих постов показывал, что любое содержательное утверждение можно сформулировать в виде некоторой тавтологии. Этот аргумент я считаю важным, поэтому не лишне его напомнить.
Допустим, мы доказали какое-то содержательное математическое утверждение T, то есть вывели его из аксиом A, B, ..., C. Если теперь мы составим формулу (A and B and ... and C -> T), то она будет истинна всегда, то есть будет тавтологией. Его надо отличать от самого утверждения T, которое тавтологией, вообще говоря, не будет, и доказательство его "истинности" проведено в предположении "истинности" исходных посылок A, B, ..., C. Однако из этих посылок T выводится уже при помощи рассуждений чисто логических, то есть выписанная нами формула (A and B and ... and C -> T) допускает чисто логическое доказательство, а потому истинна всегда, независимо от своей внутренней "начинки". Знание того, будет ли эта формула тавтологией, равноценна знанию того, выводится ли утверждение T из наших аксиом, а это есть уже некий вполне содержательный факт.
Приведём другие примеры тавтологий, которые менее "очевидны". Например, таковой будет формула (Ey)(Ax)Q(x,y) -> (Ax)(Ey)Q(x,y). Она будет истинна всегда, независимо от того, как и на какой области мы проинтерпретируем Q. Убедиться в этом весьма легко, если вдуматься в смысл того, о чём здесь говорится. Можно также предъявить и чисто логическое доказательство этой тавтологии, опираясь на правила (1) -- (5). Желающие в этом опять-таки могут убедиться.
А вот если мы поменяем местами посылку и заключение, то формула (Ax)(Ey)Q(x,y) -> (Ey)(Ax)Q(x,y) тавтологией уже не будет. Имеется очень много интерпретаций, в которых эта формула оказывается ложной. Например, если в качестве "предметной области" взять множество чисел (натуральных, целых -- каких угодно), а за Q(x,y) принять факт равенства этих чисел, то есть x=y, то можно пронаблюдать, что при этом получится. Посылка импликации окажется истинной, потому что для любого числа x существует число y, равное ему -- это само число x и есть. А вот заключение импликации будет уже ложно: оно утверждает, что существует некоторое "волшебное" число y, которое равно каждому числу x. Понятно, что такого быть не может, и наша импликация оказывается ложной в указанной интерпретации. Тем самым она уже не есть тавтология -- даже если бы оказалось, что во многих других интерпретациях она истинна.
Зададимся теперь вопросом, какой набор правил логического рассуждения можно было бы назвать "полным"? Всё, что можно вывести при помощи этих правил, всегда истинно, при какой бы то ни было интерпретации. То есть логически выводятся "из ничего" только тавтологии, сиречь "логические законы". Но все ли это тавтологии? Теорема Гёделя о полноте как раз и утверждает (в одной из своих формулировок), что все без исключения. Это подтверждает, что система правил логического вывода (1) -- (5) полна в означенном выше смысле.
В самом начале нашего изложения мы формулировали теорему как утверждение о том, что всякая непротиворечивая теория имеет модель, и обещали изложить доказательство. Это сейчас и будет проделано, но для начала мы покажем, почему из этого факта сразу же вытекает выводимость любой тавтологии. Рассуждение очень простое: возьмём произвольную тавтологию Ф. Рассмотрим "теорию", состоящую из одной-единственной формулы not(Ф), которая есть отрицание Ф. Может ли эта теория иметь модель? Очевидно, нет: поскольку Ф -- это тавтология, она истинна во всех интерпретациях. Поэтому not(Ф) ложна во всех интерпретациях, то есть в принципе невозможно указать модель для нашей теории из одной формулы. Тогда отсюда вытекает, что наша теория противоречива (мы опиремся здесь на пока что не доказанный факт о наличии хотя бы одной модели у всякой непротиворечивой теории). Противоречивость означает, что из условия not(Ф) выводится логическое противоречие. Но тогда, согласно правилу (3) рассуждения "от противного", это логически доказывает формулу Ф, что мы и хотели установить.
10. Итак, сейчас нам осталось изложить главную часть -- доказательство того факта, что всякая непротиворечивая теория T имеет модель. Оценим, что нам для этого может потребоваться. Представим себе на время, что искомая модель уже построена, и мы о ней "всё знаем". Тогда для любой замкнутой формулы (то есть формулы, не зависящей от переменных) мы знаем, истинна или ложна она на этой модели. Все формулы нашей теории T должны при этом войти в число истинных формул. То есть теория T станет частью какой-то большей теории T*, состоящей из всех истинных на модели формул. Последняя теория будет непротиворечивой (так как имеет модель), и она кроме всего прочего будет полной, то есть для любой замкнутой формулы Ф она будет содержать либо Ф, либо not(Ф).
Те читатели, которые знакомы с теоремой Гёделя о неполноте, не должны упускать из виду одно обстоятельство: эта знаменитая теорема ни в коем случае не утверждает, что полных непротиворечивых теорий не существует. Они, конечно же, существуют, даже будучи "достаточно сильными", то есть при условии, что они "содержат арифметику". Дело в том, что в теореме о неполноте важнейшим условием является то, что аксиомы теории "явно заданы", то есть существует чисто "механическая" процедура отличения аксиом от всего остального. Но когда мы работаем с классом всех истинных формул (допустим, для той же арифметики), у нас нет в распоряжении средства отличить истинную формулу от не истинной. Наличие такого средства означало бы, что мы вообще досконально изучили "всю математику".
Итак, продолжим наше изложение. Помимо того, что было сказано выше о теории T*, она обладает ещё одной важной особенностью. Представим себе некоторое "всеобщее" утверждение, которое на нашей модели (существование которой мы временно предположили) не выполнено. То есть некоторая формула вида (Ax)Ф(x) является ложной. Согласно определению истинности формул (вытекающему из содержательной трактовки квантора всеобщности), формула Ф(x) должна быть ложна на некотором элементе d предметной области D нашей модели. При этом удобно расширить наш язык, пополнив его новыми константами -- элементами множества D, из которых состоит модель. В этом случае Ф(d) получится формулой, и тогда она должна принадлежать теории T* (с учётом "обогащения" языка, которое мы сделали). Поэтому далее мы можем попытаться построить такую непротиворечивую теорию T*, которая содержала бы T, была полной, а также для любого "всеобщего" утверждения, которое не должно быть истинным, содержала бы частный пример, указывающий на то, на каком именно элементе не выполняется условие вида Ф(x).
Проведённый выше анализ позволяет ответить на вопрос, из чего следует пытаться строить модель. Ведь поначалу это совершенно не ясно: у нас есть лишь набор формул без какой-либо содержательной интерпретации. И потому оcтаётся открытым вопрос о "строительном материале". В любом случае, мы собираемся строить модель из каких-то букв, символов. Но каков содержательный смысл этих символов? Сделанные нами рассуждения "эвристического" характера подсказывают, что модель должна строиться из контрпримеров к "всеобщим" утверждениям теории. Здесь подразумеваются, конечно, те всеобщие утверждения, которые "не верны". В нашем случае это будет означать, что в той теории, которую мы будем строить, расширяя T (и имея в виду получение теории T*), часть "всеобщих" (то есть начинающихся с квантора всеобщности) утверждений будет опровергаться. И вот из контрпримеров к ним мы и будем строить модель.
Мы ограничимся при нашем доказательстве случаем, когда множество символов теории является счётным, то есть эти символы можно занумеровать натуральными числами. Хотя не всякое множество таково (скажем, точки прямой занумеровать нельзя в силу классической теоремы Кантора -- их оказывается "слишком много"), этот случай будет рассмотрен нами как основной, так как на нём проще всего проследить "пружины" доказательства. В конце мы сделаем замечание, касающееся того, как можно перенести это доказательство и на самый общий случай.
Наша стратегия будет такой: мы будем постепенно расширять теорию T с обязательным условием, что при расширении мы не теряем свойство непротиворечивости, за чем мы будем постоянно следить. Помимо добавления новых утверждений к теории, мы будем расширять и её "сигнатуру", то есть в данном случае -- набор предметных констант. Это расширение будет делаться посредством бесконечной серии этапов, и на каждом этапе у нас будет иметься некая непротиворечивая теория S, содержащая T. Опишем сейчас две основные операции, которые мы будем осуществлять на каждом этапе.
Прежде всего, мы будем строить пополнение теории S следующим образом. Занумеруем каким-то образом все замкнутые формулы теории S. Их будет бесконечно много; обозначим их через Ф1, Ф2, ..., Фn, ... . Идя вдоль этого бесконечного списка, мы каждую очередную формулу будем либо присоединять к нашей теории, либо пропускать. Руководствуемся мы при этом одним очень простым правилом. Если присоедиение очередной формулы Фn к уже имеющейся на данном шаге теории приводит к противоречию, то мы эту формулу пропускаем, а в противном случае -- присоединяем. Такая процедура гарантирует непротиворечивость того, что мы имеем, просто по построению. В результате этого бесконечного процесса присоединения к теории новых формул, из теории S возникает непротиворечивая теория, которую мы будем обозначать через C(S) и называть "пополнением" теории S. Принцип её построения очень простой: мы хотим "определиться" по каждому вопросу, который в принципе может возникнуть, и мы при этом соглашаемся со всем, с чем в принципе можем согласиться, избегая возникновения противоречий.
Тут уместно напомнить, что непротиворечивость теории, возникающей после просмотра очередной формулы списка имеет место в силу выбранного нами принципа, и потому C(S) тоже непротиворечива в силу уже звучавшего однажды соображения. Противоречие, которое следует из бесконечного множества формул, следут также и из конечной "части" этого множества -- просто в силу того, что в любом доказательстве, представляющем собой текст конечной длины, мы ссылаемся лишь на конечное число "аксиом". Поэтому, если бы противоречие возникло после присоединения бесконечного числа формул, нами добавленных, то оно возникло бы на каком-то конечном шаге, чего быть не может. Ещё было бы естественно обосновать, почему теория C(S) получается полная, что оправдывало бы её название. Этот факт хотя и верен, но он нам не нужен: мы после завершения всего "строительства" проверим полноту той теории, которая нам будет реально нужна.
Теперь опишем вторую операцию, которую мы будем осуществлять по отношении к теориям. Это как раз и есть то самое расширение "алфавита" предметных констант -- с присоединением новых утверждений с участием этих символов. Как мы сказали, возникновение каждой новой константы мы связываем с обнаружением "всеобщего" утверждения, которое "не выполняется". В последнем мы можем быть уверены тогда, когда мы располагаем отрицанием такого утверждения, то есть имеющаяся на тот момент теория у нас содержит формулу вида not((Ax)Ф(x)). По своему смыслу, эта формула означает существование "контрпримера" к Ф, то есть такого x, для которого выполнено not(Ф(x)). То есть это на самом деле есть утверждение о существовании чего-то. Хотя мы отказались от использования квантора существования, но такие формулы мы далее будем называть "экзистенциальными", или E-формулами. А всю операцию в целом, которую сейчас опишем -- экзистенциальным пополнением теории S. Обозначаться она будет через Ex(S).
Строится она вот как. Прежде всего, все E-формулы теории S мы нумеруем. Это даёт нам бесконечный список, идя вдоль которого мы на каждом шаге будем работать с какой-то E-формулой вида not((Ax)Ф(x)). Мы будем всякий раз добавлять свою константу d для каждой такой формулы (я использую "общее" обозначение d, дабы не вводить серию букв с индексами) и добавляем к теории новую формулу not(Ф(d)), смысл которой в том, что Ф не выполнено на элементе d.
Это ключевой момент доказательства. Нужно обосновать, почему присоединение такой формулы не приводит нас к противоречию. Допустим, что противоречие всё-таки возникло. Поскольку предыдущая теория была непротиворечивой, это означает, что в ней выводимо отрицание той формулы, которую мы присоединили. То есть выводима формула Ф(d) -- опять же в силу рассуждения "от противного": коль скоро отрицание Ф(d) ведёт к противоречию, то это доказывает Ф(d). (Ещё точнее было бы сказать, что эта выводимость имеет место в той теории, которая была на предыдущем шаге, и к которой мы добавили новый символ d в качестве предметной константы.) Теперь сделаем вот что: в имеющемся доказательстве заменим во всех формулах "свежую константу" d, которая ни в одной из формул теории ранее не встречалась, на какую-то переменную x, которая также в доказательстве не использовалась. Что мы этим получим? Не что иное, как вывод формулы Ф(x). Если мы теперь применим правило (4), то это позволяет нам считать доказанной "обобщённую" формулу, то есть (Ax)Ф(x). Заметим, что этот вывод может быть осуществлён в теории, которая была у нас до того, как мы добавили новую формулу. Однако в этой теории у нас была формула not((Ax)Ф(x)), которая прямо противоречит тому, что мы вывели. Такого быть не может, так как у нас все рассматриваемые теории непротиворечивы. То есть мы показали этим рассуждением, что наше допущение о возникновении противоречия после добавления новой формулы Ф(d), приводит нас к ситуации, которой быть не может. Следовательно, после присоединения новой формулы противоречия не будет.
11. Мы прошли сейчас как бы через "перевал". Далее последует относительно лёгкий "спуск". Мы строим "экзистенциальное пополнение" теории S, добавляя новые константы и новые формулы, и получаем в итоге непротиворечивую теорию Ex(S). Это завершает описание второй важной операции, которую мы будем применять к нашим теориям. Теперь вот как будет выглядеть основная конструкция, которая также будет строиться по шагам. Мы последовательно будем строить теории T0, T1, ..., Tn, ... , где в качестве T0 будет взята сама наша "изначальная" теория T, для которой мы хотим построить модель. Теория T1 получается из неё так: мы сначала применяем к T0 первую операцию (то есть "пополнение"), а потом к получившейся теории -- вторую операцию ("экзистенциальное пополнение"). Точно так же строим T2: пополняем T1, и "экзистенциально пополняем" то, что при этом получается. Можно записать общее правило перехода от теории Tn к "следующей" теории Tn+1 в виде формулы:
Tn+1 = Ex(C(Tn))
В итоге у нас возникает расширяющаяся "цепочка" теорий, каждая из которых является частью всех остальных. В силу того, что обе операции сохраняют непротиворечивость теорий, каждая наша теория Tn будет непротиворечива. Объединение всех этих "расширяющихся" теорий мы обозначим через T*, и оно тоже будет непротиворечиво как теория. Сейчас нам нужно проверить, что полученная теория полна. Напомним, что это означает: что для любой замкнутой формулы Ф, у нас либо сама Ф, либо её отрицание принадлежит T*.
Формула Ф может содержать константы, которые мы добавляли в процессе наших построений. Но этих констант в любом случае конечное число, и на каком-то n-м шаге все они были уже добавлены. Это означает, что при переходе от теории Tn к теории Tn+1, на этапе построения пополнения теории Tn, мы непременно просматривали формулу Ф в числе прочих замкнутых формул. Каждую из просматриваемых формул мы либо присоединяли, либо отвергали. И если мы присоединили Ф, то доказывать нечего: она у нас входит в T*. А что значит, что мы её отвергли? Это значит, что её присоединение к теории в момент рассмотрения приводило бы к логическому противоречию. Тогда присоединение Ф к более "широкой" теории T* тем более должно приводить к противоречию. Запомним это, и применим те же соображения к формуле not(Ф), которая тоже замкнута, и содержит те же константы. Если мы её присоединяли в процессе просмотра, то доказывать опять-таки нечего. А если отвергли, то присоединение not(Ф) к T* даёт противоречивую теорию. Мы вообще-то уже анализировали такую ситуацию, и знаем, что это значит: мы сначала выводим из not(Ф) противоречие, оставаясь в пределах теории T*. Затем, применяя правило (3), мы тем самым "от противного" выводим Ф в теории T*. Но присоединение к теории T* её логического следствия, каковым является Ф, ни к какому противоречию приводить не может, поскольку T* непротиворечива. Осталось сравнить это с тем, что мы запомнили выше, откуда станет ясно, что T* обязана быть полной.
Итак, мы осуществили своего рода "программу-минимум", построив ту теорию T*, о которой мы говорили в ходе наших "эвристических" рассуждений. Как же теперь построить модель? Понятно, что в качестве предметной области D надо взять не что иное как множество всех предметных констант, добавляемых нами в ходе всего процесса. Это будет некое счётное множество. Теперь надо проинтерпретировать символы нашего языка, на котором пишутся формулы теории T. Мы проинтерпретируем сразу все символы "объемлющей" теории T*, причём константы можно не интерпретировать -- они как бы "играют самих себя", так как входят в предметную область. Интерпретировать нужно лишь предикатные символы. Пусть P -- один из таких символов, и пусть он будет k-местным. Ему надо сопоставить отношение на D, тоже k-местное, то есть про любой упорядоченный набор из k элементов множества D (не обязательно различных), нужно сказать, в каком случае мы считаем, что эти элементы находятся в рассматриваемом отношении. Решение вопроса тут напрашивается само собой: надо подставить эти элементы в роли констант в предикат P, что даст нам замкнутую формулу вида P(d1,..., dk). Теории T* принадлежит либо сама эта формула, либо её отрицание, причём ввиду непротиворечивости верно только одно из этих положений. Если формула входит в T*, то считаем, что наши элементы предметной области находятся в данном отношении, а если не входит, то не находятся. Мы сделали не что иное, как "содержательно" проинтерпретировали предикатный символ P, и так следует поступить с каждым из символов.
Поскольку интерпретация построена, то про каждую замкнутую формулу языка теории T* можно говорить, истинна или ложна она в этой интерпретации. Чего нам не хватает? Мы хотим доказать, что все положения теории T в построенной интерпретации истинны. То есть получена искомая модель M теории T. Для того, чтобы сделать этот последний шаг в нашем доказательстве (являющийся по сути проверкой) мы докажем вот что: всякая замкнутая формула теории T* истинна на M (то есть в построенной интерпретации) тогда и только тогда, когда эта формула принадлежит T*. Иными словами, мы хотим проверить то, что T* есть не что иное как список всех истин, касающихся M. Хочется назвать M словом "модель", но пока это преждевременно, так как M пока что есть лишь интерпретация теории (с предметной областью D), и мы сейчас проверим, что это в самом деле модель теории T (и даже теории T*).
ПРОДОЛЖЕНИЕ (часть 3)
К ОБСУЖДЕНИЮ