Игошин Математическая логика и теория алгоритмов (1019110), страница 67
Текст из файла (страница 67)
Отсюда по правилу введения квантора общности (ВКО, см. Задачник, №! 1.7, а) получаем Г, (Зх)(В(х))» — (~Уу)(- В(у)). (2) Кроме того, по теореме из задачи № 11.6, б Задачника легко получается выводимость ('Фу)(- В(у))»- — (Зу)(В(у)). Наконец, в силу выбора переменной у, которая свободна для х в формуле 268 В(х), и на основании правила переименования связанных переменных (см. Задачник, М 1!.4, б) из последней выводимости заключаем, что ('ФуН- В(у))» — — (ЗхНВ(х)), (3) Из выволимостей (2) и (3), в силу транзитивности отношения выводимости (см.
теорему 15.3, в), получаем: Г, (ЗхНВ(х))»- (ЛхНВ(х)). Учитывая, что (ЛхНВ(х)) - =А„, можно заключить, что множество Г 0 (А„) противоречиво. Поскольку Г с Е„, то Г Ц (А„) с Е„с (А„), а значит, множество Е„Ц (А„) также противоречиво, что противоречит исходному условию. Следовательно, и в этом случае множество Е„„, непротиворечиво. 2) Рассмотрим теперь множество Е* = Ц Е„(объединение берется по и от О до ).
Отметим два свойства этого множества формул. Во-первых, множество Е* непротиворечиво. В самом деле, если бы из Е* выводились формулы Ри — Р, то они выводились бы из конечного подмножества множества Е*, которое включалось бы в некоторое Е„, которое, следовательно, было бы противоречивым. Но это не так в силу предыдущего п.
1 доказательства. Вовторых, для любой формулы А исчисления предикатов сигнатуры о' А а Е* или ~А а Е* (свойство полноты множества Е*). Это вытекает непосредственно из построения Е*, так как А = А„для некоторого натурального и. Последнее свойство можно сформулировать несколько в ином виде. Сначала отметим, что А е Е* с=» Е* »- А. В самом деле, импликация слева направо очевидна. Предположив, что Е* »- А и А я Е*, в силу отмеченного свойства получим — А е Е*. В итоге получаем, что Е* противоречиво, что противоречит первому отмеченному выше свойству. Следовательно, второе отмечаемое утверждение принимает вид: Е' »- А или Е* »- А для любой формулы А. 3) Построим теперь саму модель М.
Напомним, что ее сигнатура о = (а,, ап ..4,4, ~п ...; ЄЄ...). Рассмотрим всевозможные термы расширенной сигнатуры о', не содержащие предметных переменных, а содержащие лишь предметные константы ам аь ..., оь с„... Напомним, что термы представляют собой либо сами зти константы, либо выражения вида Д(гп ..., г„,), гдето — функциональный символ из о, а г„..., г„, — термы. Множество всех этих термов и есть базисное множество М модели М. Сигнату~ные опе»грации на этом множестве зададим следующим образом: а; = аь ~; (г„..., г„,) = Я(гп ..., г„,), (1 = О, 1, ...).
Наконец, выполнимость йа М соответствующего сигнатурного отношения определим следующим образом: м Р"(гп ..., г ) с=» е* »- Р,.(г„..., г„,.). (4) 269 4) Проверим, что алгебраическая система М сигнатуры а действительно является моделью исходного множества Е формул исчисления предикатов сигнатуры а, т.е. М ~ Е. Для этого докажем сначала, что лля всякой формулы Г(хь ..., х„) сигнатуры а' и любых термов гь ..., г„в М имеет место следующее угверждение; М ~ В(гн ..., г„) ~=» Е* » — Р(гь ..., г„).
(5) Доказательство будем вести индукцией по числу 7г логических знаков, используемых при построении формулы Е База индукции: 1= 0. Тогда à — атомарная формула, имеющая вид Рт(гь ..., г,), а для нее утверждение (5) верно по определению (4). Ш а г и иду к ци и. Предположим„что для всех формул, в записи которых число логических символов < 7г, утверждение (5) верно. Пусть  — произвольная формула, в записи которой участвует /с+ 1 логический символ. Покажем, что тогда утверждение (5) будет справедливо и для нее.
На основании определения (формулы) формула Гимеет один из следующих видов: А, А -» В, (чх)(В(х)), (Эх)(В(х)). Рассмотрим последовательно каждый из этих случаев. а) Гм — А. Предположим, что М ~ А(го ..., г„). Тогда по определению отрицания это означает, что А(г„..., г„) не выполняется на М: М )' А(г„..., г„).
Отсюда по предположению индукции заключаем, что Е* у~ А(г„..., г„). Следовательно, по свойству полноты множества Е*, отмеченному в п. 2 настоящего доказательства, Е" »- 4(гн ..., г„). Легко видеть, что каждое угверждение настоящего рассуждения допускает обращение, так что М ~ А(г„..., г„) <=» Е* »- -А(гь ..., г„).
б) Гм А — » В. Предположим, что М ~ А(г„..., г„) — » В(г„..., г,). Используя определения импликации, конъюнкции и отрицания, определение (4), полноту Е* и предположение индукции для формул А и В, проводим следующее рассуждение: М ~ А — » В с=» М ~ — (А л — В) е:» М ~ А л — В <=» М )А А, или М ~( — В с=» М ~( А, или М ~ В е» Е*)~ А, или Е' »- В «» Е' » — 4, или Е*» — В.
Теперь мы находимся в области формализованного исчисления высказываний. Дальнейшие рассуждения таковы. Из каждого из угверждений Е* »- А и Г» — В по правилу ~-вв следует Е* »- А ~ В, т.е. Е* »- А — » В. Теперь нужно проделать обратное рассуждение. Предположим, что Е* »- А — » В и Е*»- А. Следовательно, по второму свойству множества Е* из п. 2 настоящего доказательства Г»- А.
Тогда из выводимостей Г»- А — » В и Е* »- А и правила МР (А -» В, А»- В) следует, что Е* »- В. Итак, мы доказали, что М ~ А — » В е~ Е* »- А -» В. в) Р ьэ (Чх)(В(х, г„..., г„)). Предположим, что М ~ ('Фх)(В(х, Гь ..., Г„)). По определению квантора общности это означает, что М ~ В(б гн ..., г„) для каждого элемента г в М. Таким образом, по 270 предположению индукции (5) получим, что Х' ~- В(0 гн ..., г„). Отсюда, в силу правила введения квантора общности, заключаем, что Х" ~- (ч'х)(В(х, ~„..., г„)). Обратно, пусть Х* ~- (Ъх)(В(х, гь ..., г„)).
Вместе с аксиомой РА1: (Ъх)(В(х, ~„..., г„)) — > В(0 гн ..., г„), в силу правила МР, это дает: Х' ~- В(0 1„.„, г„). На основании предположения индукции (5) отсюда следует, что М ~ В(б гн ..., г„). Поскольку данная выполнимость на модели М имеет место лля любого элемента г я М, поэтому на основании определения квантора общности отсюда следует, что М ~ ('чх)(В(х, го ..., г„)). г) г" и (Зх)(В(х, г„..., г„)).
Предположим, что М ~ (Зх)(В(х, ~н ..., г„)). Тогда по определению квантора существования М ~ . В(ам г„..., г„) для некоторого элемента ав я М. В силу предположения индукции (5) отсюда получаем Х" ~- В(ав, гн ..., 1„). Вместе с аксиомой РА2: В(а„гн ..., г„) -+ (Зх)(В(х, г„..., г„)), в силу правила МР„это дает: Х' ~- (Зх)(В(х, гп ..., г„)). Обратно, пусть Х* ~- (Зх)(В(х, ~„..., г„)). Поскольку (Зх)(В(х, ь, ..., г„)) — замкнутая формула сигнатуры о', то она содержится в последовательности Аь Аь ..., А„, ... всех таких формул. Предположим, что это формула А„. Тогда множество Х„() (А„) непротиворечиво. (Если бы оно было противоречиво, то Х„„равнялось бы Х Ц ( А„), т.е. формула -А входила бы в множество Х' и последнее было бы противоречивым, что не так в силу п. 2 настоящего доказательства.) Поскольку, кроме того, А начинается с квантора существования, то в этом случае Х,, = Х 0 (А„, В(с„, Гн ..., Г„)) и, значит, В(см Г„..., г„) е Х*.
Следовательно, для формулы В(см гь ..., г„) по предположению индукции имеем М ~ В(см гп ..., г„) для некоторой константы сг е М. Тогда по определению квантора существования М ~ (Зх)(В(х, гн ..., г„)). Итак, мы доказали, что всякая формула, выводимая из Х* (и, в частности, принадлежащая Х'), истинна (выполнима) на модели М. В частности, на М выполняются и все формулы исходной совокупности Х = Хе ~ Х*, т.е. М вЂ” действительно модель непротиворечивого множества формул Х.
Теорема полностью доказана. П Теорема Геделя о существовании модели позволяет доказать теорему, обратную к теореме 29.8, и они вместе образуют следующую важную метатеорему. Теорема 39.11 (о непротиворечивости). Множество формул узкого исчисления предикатов семантически непротиворечиво тогда и только тогда, когда оно синтаксически непротиворечиво. Доказательство. Необходимостьестьтеорема 29.8. Обратно, если множество формул синтаксически непротиворечиво, то по теореме 29.10 оно имеет модель, а тогда по лемме 29.7 оно семантически непротиворечиво. П Наконец, объединим в одну метатеорему следствие из теоремы 29.8 и теорему 29.10. Получим следующее.
271 Теорема 29. 13 (о непротиворечивости). Множество формул узкого исчисления предикатов синтаксически (дедуктивно) непротиворечиво тогда и только тогда, когда оно имеет модель. П Приведем интересный комментарий, который лает теореме о непротиворечивости известный логик Р. Линдон [7.16, с. 79 — 80), по мнению которого доказательства (дедуктивной) непротиворечивости какой-либо теории посредством указания ее модели широко распространены в абстрактной математике.
Менее очевидное из утверждений теоремы о непротиворечивости — о существовании модели у каждой дедуктивно непротиворечивой теории— используется далеко не так часто. Возможно, это объясняется тем, что математики не слишком-то большое значение придают понятию существования; теорему о непротиворечивости можно как раз и рассматривать как скромное, но зато точное выражение довольно-таки расплывчатого мнения, что существование в математике — это не что иное, как непротиворечивость. Возможности применения теоремы о непротиворечивости к проблемам установления непротиворечивости конкретных теорий весьма ограниченны: дело в том, что построение модели обычно требует принятия в метаязыке допущений, значительно более сильных, нежели те, которые выражаются предметной теорией.
Другой путь установления непротиворечивости какой-нибудь аксиоматической теории состоит в том, чтобы с помощью чисто синтаксических рассмотрений показать, что в данной теории нельзя доказать тождественно ложную формулу. Область применения этого метода, однако, также невелика. Теорема Геделя не позволяет надеяться на получение доказательства непротиворечивости теории, если не допускать в теории, предназначенной для такого доказательства на метаязыке, по меньшей мере столь же сильных средств, что и в рассматриваемой предметной теории. Убеждение в непротиворечивости достаточно сложных математических теорий базируется в конечном счете на интуиции и опыте.
Полнота и адекватность формализованного исчисления преднкатов. Доказав теорему Геделя о существовании модели (теорема 29.10), можно доказать теорему, обратную теореме оправданности (следствие 29.2 из теоремы 29.1), т.е. утверждение о том, что из семантической выводимости следует синтаксическая выводимость.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
