Игошин Математическая логика и теория алгоритмов (1019110), страница 65

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 65)

Применяя дважды правило МР (учитывая при этом теорему (ЕЯ7)), получаем: (АЬа л 1сЬ) — ~ 1ас. Сделав в закон силлогизма другую подстановку Х|1сЬ л АЬа, У|АЬа л 1сЬ, У|Гас, придем к формуле ((1сЬ л АЬа) -э (АЬа л 1сЬ)) — ~ — ~ (((АЬа л 1сЬ) -+ 1ас) -+ ((1сЬ л АЬа) -+ 1ас)).

Учитывая выводимость посылки этой формулы (см. второй абзац в доказательстве формулы 9)) и только что установленную выводимость посылки остающейся формулы, после двукратного применения правила МР придем к требуемой формуле. 14) Из АаЬ вЂ” > 1аЬ (теорема (РБЗа)) с помощью подстановки а|с получаем: АсЬ -+ 1сЬ.

В выводимую формулу исчисления высказываний ((Х л У) — э 2) -+ ((И -+ Х) -э ((Р л У) -э У)) делаем подстановку Х| 1сЬ, У| АЬа, У|1ас, У|АсЬ. В результате получаем формулу ((1сЬ л АЬа) — э 1ас) -+ ((АсЬ -+ 1сЬ) — э ((АсЬ л АЬа) -+ 1ас)). Учитывая формулу 13) и выведенную вначале формулу, после двукратного применения правила МР приходим к требуемой формуле. Докажите выводимость остальных аристотелевых силлогизмов. П 261 й 29. Свойства формализованного исчисления предикатов Формализованное исчисление предикатов (ФИП) развито достаточно глубоко (см. э 25 и Задачник, Э 11), и теперь, как и в случае формализованного исчисления высказываний, надлежит рассмотреть свойства (или метатеорию) этого исчисления.

Но теперь в области предикатов логика достигает такой выразительной силы, что становится логическим основанием конкретных математических теорий, и теоремы (по сути, метатеоремы) о логике рассуждений достигают поистине философской глубины. Оправданность аксиоматизации. Теорема оправданности аксиоматизации утверждает, что если Ф ь- Г, то Ф ~ Г, т.е. из синтаксической выводимости следует семантическая выводимость. Ее очевидным следствием будет утверждение о том, что всякая теорема ФИП является общезначимой формулой (тавтологией) логики предикатов. Смысл этой теоремы состоит в утверждении фактически того, что мы не были «излишне щедры» в выборе аксиом и правил вывода для нашего формального исчисления и не включили в их число ничего лишнего, ибо доказуемыми в этом исчислении оказываются лишь общезначимые формулы логики предикатов.

Доказательство этой теоремы не очень сложное, и мы получим ее в качестве следствия несколько более общей теоремы. Обратное же утверждение «если Ф ~ Г, то Ф»- Г» (т.е. при выборе аксиом и правил вывода мы не проявили и «излишней скромности», и для всякой общезначимой формулы логики предикатов в нашем ФИП вполне достаточно формальных средств, чтобы доказать ее), уже не столь очевидно, и доказательство его, приводимое дальше, потребует от нас значительно больших усилий. Теорема оправданности имеет глубокий смысл: она оправдывает наши занятия математикой, убеждая в том, что наши логические рассуждения и умопостроения не уводят нас от смысла и от практики.

Теорема 29.1. Если в алгебраической системе М выполняются все формулы из множества Ф и из Ф синтаксически выводима формула Г, то Г также выполняется в М: М ~ Ф и Ф»- Г=» М ~ Г. Д о к а з а т е л ь с т в о разделим на три этапа. На п е р в о м отметим, что каждая аксиома ФИП есть тождественно истинная формула.

Что касается аксиом А1, А2, АЗ исчисления высказываний, то их тождественная истинность установлена нами в алгебре высказываний (см. теоремы 3.1 з, 3.3, а, л). Общезначимость аксиом РА1 и РА2 установлена в теореме 21.13. На втором этапе покажем, что все три правила вывода, используемые в ФИП, обладают следующим семантическим свойством.

Если алгебраическая система М служит моделью для всех посылок правила вывода, то М будет моделью и для формулы, 262 получаемой из данных формул с помощью данного правила вывода. Докажем это утверждение для трех из правил вывода. П р а в и л о МР. Допустим, что М м Г-» 6 и М ~ Р. Докажем, что тогда М ~ 6. Возьмем любую подстановку а констант из М.

Тогда, по условию, каждое из высказываний Г(а) — > 6(а) и г(а), получаемых соответственно из формул Р-> 6 и Г в результате подстановки предметных констант а, будет истинным. Тогда истинным будет и высказывание 6(а), т.е. М ~ „6. Это и означает, что М~ 6. 'Ф-правило. Допустим, что М ~ 6(у) — » г(х, у), где х не входит свободно в формулу 6, а у обозначает все свободные предметные переменные в формулах Р и 6 (в à — кроме х). Тогда сделанное допущение означает, что для любых элементов а, Ь е М (где М вЂ” носитель алгебраической системы М) высказывание 6(Ь) — > Г(а, Ь) истинно в М. Рассмотрим теперь высказывание 6(Ь) — > ('Фх)(г(х, Ь)) и покажем, что оно истинно в М при любом Ь е М. В самом деле, если 6(Ь) ложно, то рассматриваемое высказывание истинно. Если же 6(Ь) истинно, то, по отмеченному выше, истинным будет и высказывание Г(а, Ь).

Поскольку оно будет истинным при любом а е М, то отсюда вытекает истинность для таких Ь е М высказывания ('чх)(Г(х, Ь)). Это, в свою очередь, влечет истинность высказывания 6(Ь) — » (чх)(Г(х, Ь)) для тех Ье М, для которых 6(Ь) истинно. Итак, высказывание 6(Ь) — » ('чх)(Г(х, Ь)) истинно для любых Ь е М.

Это и означает, что М ~ 6(у) -+ (Чх)(Г(х, у)). В-правило. Подобно предыдущему правилу, доказывается, что если М ~ Г(х) — » 6, то М ~ (Эх)(Г(х)) -+ 6. Наконец, на т р е т ь е м этапе докажем угверждение самой теоремы. Пусть М ~ Ф и Ф»- Р. Последнее означает, что имеется вывод В„Вн ..., В„формулы Риз множества формул Ф (в частности, В„ж Р). Покажем, что каждый элемент этой последовательности является формулой, выполняющейся в М. Доказательство проведем индукцией по номеру к формулы в рассматриваемом выводе. При к= 1, если В, е Ф, то, по условию, М Вь Если В,— аксиома, то она общезначима и, в частности, М ~ Вь Предположим теперь, что при всех к < н (и а 2) все формулы В„выполняются в М, т.е.

М ~ В». Рассмотрим формулу В„. Если В„а Ф или „— аксиома, то, как отмечено выше, М ~ В„. Если же В„получена из предыдущих формул последовательности по одному из трех правил вывода, то (на основании выполнимости всех предьшущих формул в М) в силу утверждений (см. второй этап) заключаем, что и В„выполняется в М, т.е.

М ~ В„. Окончательно заключаем, что все формулы последовательности В„Вп ..., В„истинны в М, в частности М ~ )г. Теорема полностью доказана. П Следствие 29.2 (теорема оправданности). )чз синтаксической выводимости следует семантическая выводимость, т.е. если Ф»- Р, тоФ~Р, 263 До к азател ьств о. Пусть Ф г- Р' и пусть М вЂ” любая алгебраическая система, в которой выполняются все формулы из Ф, т.е.

М ~ Ф, Тогда по доказанной теореме М ~ г. По определению семантического следствия это и означает, что Ф ~ Г. Следствие 29.3. Всякая доказуемая дюрмула является общезначимой (т.е. любая теорема истинна): если ь- г", то ~ Е Доказательство получается из предыдущего следствия при Ф= О.

Непротиворечивость формализованного исчисления предикатов. Важнейшим компонентом критерия оправданности всякой математической теории является ее непротиворечивость, т.е. невозможность доказательства в ней некоторого утверждения и его отрицания одновременно. Трудности, связанные с доказательством этого свойства математических теорий (а одной из причин этих трудностей, несомненно, было отсутствие в содержательных математических теориях точного понятия доказательства), привели к тому, что в математике более естественным стал другой признак непротиворечивости теории, основанный на возможностях реализации этой теории, ее моделируемости. Но в то же время этот подход и привел к возникновению парадоксов в математике, которые, в свою очередь, привели к возникновению науки об основаниях математики и к концепциям формального подхода к понятиям доказательства и математической (аксиоматической) теории.

Одной из задач этого подхода была выработка такого формального понятия доказательства, при котором для конкретной математической теории понятие ее формальной непротиворечивости совпало бы с понятием ее содержательной непротиворечивости. Факт такого совпадения, в силу точности определения доказательства, становится математической теоремой (точнее, метатеоремой). Отметим, что привыкание в математике к эквивалентности этих двух понятий непротиворечивости было непростым.

В частности, неприятие современниками неевклидовых геометрий Лобачевского — Боян объясняется также и тем, что законность этих теорий обосновывалась отсутствием в них противоречий — аргументом, совпадающим по существу с современным понятием формальной непротиворечивости. Геометрические модели для этих теорий, доказывающие их содержательную непротиворечивость, были найдены позднее. Наша задача состоит в том, чтобы в рамках формализованного (узкого) исчисления предикатов дать точные определения двух понятий непротиворечивости и установить их эквивалентность. Напомним, что формула логики предикатов называется обще- значимой„если она истинна в любой интерпретации, и нротиворечивой, если она ложна в любой интерпретации, т.е.

если ее отрицание общезначимо. Эти семантические понятия, связывающие непротиворечивость с истинностью, позволяют сформулировать понятие семантически непротиворечивой теории. 264 Определение 29.4. Формальная теория называется семантически непротиворечивой, если ни одна из ее теорем (формул) не является противоречивой, т.е. ложной при любой ее интерпретации.

Характеристики

Список файлов книги