Игошин Математическая логика и теория алгоритмов (1019110), страница 34
Текст из файла (страница 34)
Вспоминая теорему 15.3, о, заключаем, что 6, Н ~- 6-+ Н. Итак, рассмотренные четыре случая приводят к заключению: для любого набора о нулей и единиц справедлива выводимость 6', Н' ~- Г, которая вместе с выводимостями (1) и (2) дает следующую выводимостгк Х, ', Х;2, ..., Х„" »- Г'(Хь Хз, ..., Х„). Тем самым сделан шаг индукцйи, и можно заключить, что утверждение леммы справедливо для любой формулы Г. Сз Полнота формализованного исчисления высказываний.
В первом пункте настоящего параграфа было сказано, что полнота формализованного исчисления высказываний состоит в совпадении множества доказуемых формул с множеством тавтологий. Включение первого множества во второе (первая часть теоремы полноты) было установлено в теореме 16.1. Теперь нами все подготовлено к тому, чтобы доказать вторую часть теоремы о полноте формализованного исчисления высказываний. Теорема 16.5. Всякая тождественно истинная формула (или тавтология) алгебры высказываний доказуема в формализованном исчислении высказываний.
Символических ~ Г=» ~- Г. Доказательство. Пусть формула Г(Хь Х,, ..., Х„) является тавтологией алгебры высказываний. На основании леммы 16.4 о выводимости, имеем Х, Х", ..., Х„'" ь — Г'(Хп Хз, ..., Х) для любого набора о = (оп оз, ...„о„) из нулей и единиц.
Поскольку формула Г(Хп Х,, ..., Х„) при любой подстановке превращается в истинное высказывание (она — тавтология), то для любого набора о = (о„о,, ..., о„) о-двойником формулы Г будет сама эта формула, т.е. Г = Гдля любого о. Тогда Х, Х, ..., Х„'" ь- Г(Х„ Хз, ..., Х„). В частности, для о = (оп о„..., о„п 1) имеем (в этом случае Хя = Х„' = Х„) л Х;, Хт, ..., Х„';, Х„- Г(Х„Х„..., Х„), (П а лля о = (о„он ..., о„п 0) имеем (в этом случае Х„" = Х„Я = Х„) Х, ', Х, ..., Х„'", — Х„~ — Г(Хп Хз, ..., Х„).
(2) 138 Из выводимостей (1) и (2) по правилу удаления дизъюнкции (теорема 15.!О, д) получаем Х, Х", ..., Х„'", Х„г Х„»- г"(Х!, Хг, , Х„). Поскольку формула Х„!» Х„выводима из аксиом (см. определение связки ~ в начале 5 15 и пример 15.2), то ее можно исключить из числа посылок последней выводимости. Тогда Х,',Хг,...,Х„" ! — Р(Х»,Хг, ...,Х„), Далее нужно брать в качестве а наборы следующих видов: а = (а», аг..
1, а„) и а = (ап аг, ..., О, о„), для которых соответственно получим Х, Х, ..., Х„'"-; —, Х„, ! — Р(Х„Хг, ..., Х„). Отсюда, также по правилу удаления дизъюнкции, получаем Х! !, Кг~г, ..., Х "1»,Х„! ч Х„! ! с(Х», Хг, "., Х„) и далее Х;!, Х;, ..., Х;,; Р(Хп Хг, —, Х).
Проделав и раз эту процедуру, придем к заключению, что»- Г, т.е. формула г доказуема в формализованном исчислении высказываний. П Объединив теоремы 16.1 и 16.5, получим теорему о полноте. Теорема 1б.б (о полноте формализованного исчисления высказываний). Формула тогда и только тогда доказуема в формализованном исчислении высказываний (является теоремой исчисления), когда она является тавтологией алгебры высказываний. Символическщ»- г"с=~ ~ Г. Теорема адекватности. Теорема адекватности является обобщением предыдущей теоремы о полноте и вытекает из нее. Теорема 1б. 7(адекватности).
Формула 6 выводима в формализованном исчислении высказываний из конечного множества гипотез Г тогда и только тогда, когда она является логическим следствием всех формул из этого множества. Символически: рь сг Доказательство. Пусть г„г"„..., Г„»- 6. Тогда, по следствию 15.6 из теоремы о дедукции, данное утверждение эквивалентно тому, что р! + (~г + -' » (~т-!» (~т + 6))" ) Это утверждение, в свою очередь, эквивалентно, на основании теоремы полноты„следующему: ~ г! — г (гг — ».- — » (с -! + (г + б))" ).
139 Теперь можно использовать результаты алгебры высказываний. На основании теоремы 4.4, г последняя формула равносильна формуле (Г1 л Гз л ... л Г,„) — + О. (Точнее, на основании этой теоремы можно утверждать равносильность данных формул лишь при т = 2, но ясно, что утверждение нетрудно распространить и на произвольное натуральное число т, например, методом математической индукции, что рекомендуется проделать самостоятельно; см. также )чь !.29, г.
Задачника). Тогда из тождественной истинности одной из формул и их равносильности заключаем, что и вторая формула также будет тавтологией (см. замечание 4.7). Итак, (Г! л Г2 л ... л Г ) + О. Это утверждение на основании теоремы 6.4 эквивалентно следующему: Гь р;, ..., Г 6, что и требовалось доказать. П Непротиворечивость формализованного исчисления высказываний. Непротиворечивость — важнейшее свойство, которым должна обладать аксиоматическая теория. Противоречивая теория никакой ценности не имеет. Определение 16.8.
Аксиоматическая теория называется непротиворечивой, если ни для какого утверждения А, сформулированного в терминах этой теории, само утверждение А и его отрицание 4 не могут быть одновременно теоремами данной теории. Если для некоторого утверждения А теории оба утверждения А и 4 — теоремы этой теории, то аксиоматическая теория называется противоречивой.
Применительно к формализованному исчислению высказываний непротиворечивость означает, что в нем не существует такой формулы Г, что сама формула и ее отрицание — Гявляются теоремами формализованного исчисления высказываний, т.е. выводимы из аксиом. Следующая теорема утверждает, что это действительно так. Теорема 1б.9 (о непротиворечивости формализованного исчисления высказываний). Формализованное исчисление высказываний есть непротиворечивая аксиоматическая теория.
Доказательство. Допустим противное, т.е. предположим, что формализованное исчисление высказываний противоречиво. Значит, имеется такая формула Г, что Ги — Гявляются теоремами формализованного исчисления высказываний. Тогда по теореме 16.1 каждая из формул Ги — Г является тавтологией алгебры высказываний. Но последнее невозможно на основании определения тавтологии.
Следовательно, формализованное исчисление высказываний непротиворечиво. П Разрешимость формализованного исчисления высказываний. Определение 1б. 10. Аксиоматическая теория называется разрешимой, если 140 существует алгоритм, позволяющий для любого утверждения, сформулированного в терминах теории, ответить на вопрос, будет или нет это утверждение теоремой данной теории. Теорема 16.11 (разрешимости формализованного исчисления высказываний).
Формализованное исчисление высказываний есть разрешимая аксиоматическая теория. Доказательство. Для доказательства теоремы нужно указать алгоритм, позволяющий для каждой формулы формализованного исчисления высказываний отвечать на вопрос, можно или нельзя вывести ее из аксиом. Такой алгоритм есть. На основании теоремы 16.6 о полноте формализованного исчисления высказываний доказуемость формулы в формализованном исчислении высказываний эквивалентна тождественной истинности данной формулы в алгебре высказываний.
Для проверки последнего свойства нужно составить таблицу истинности формулы. Если последний столбец таблицы будет состоять лишь из единиц, то формула является тавтологией, а следовательно, и теоремой формализованного исчисления высказываний. Если же там встретятся нули, то формула — не тавтология, а значит, и не теорема. П й 17. Независимость системы аксиом формализованного исчисления высказываний В этом параграфе будет подвергнута анализу основа аксиоматической теории высказываний„т.е. система аксиом, на которой она базируется, для установления важного ее свойства. Понятие независимости.
После того как теория построена (З 15) и установлен ряд ее свойств (з 16), следует обратиться к ее истокам — к системе аксиом — для решения ряда вопросов. Почему в качестве аксиом выбраны именно эти формулы? Можно ли взять другие формулы в качестве аксиом? (Уже отмечалось, что имеется множество других аксиоматик для аксиоматической теории высказываний.) Можно ли сократить число аксиом до двух или одной? Можно ли из данной системы аксиом безболезненно исключить одну или две формулы? Ответу на последний вопрос и посвящается настоящий параграф.
Олределе~ие 17.1. Аксиома А из системы аксиом з, называется независящей от остальных аксиом этой системы„если ее нельзя вывести (доказать) из множества ь'х(А) всех остальных аксиом системы ь. Система аксиом Х называется независимой, если каждая ее аксиома не зависит от остальных. Из определения следует, как нужно доказывать независимость той или иной аксиомы от остальных аксиом данной системы. Нужно смоделировать одновременно все аксиомы данной системы, кроме той, независимость которой доказывается, т.е.
построить модель, в которой бы выполнялись все аксиомы данной системы, 141 кроме анализируемой аксиомы. Это означает, что каждому первоначальному понятию и отношениям между понятиями нужно придать конкретное содержание посредством каких-то конкретных предметов и отношений между ними. Причем сделать это нужно так, чтобы выбранные конкретные предметы и отношения между ними обладали свойствами, сформулированными в аксиомах из системы ЕЛ (А), и не обладали бы свойством А.
Такая совокупность конкретных предметов и отношений между ними называется моделью системы аксиом Е\(А). Наличие ее доказывает независимость аксиомы А от аксиом из Е~(А). В самом деле, ведь если А можно было бы вывести из Е~ (А), то во всякой модели, в которой выполнялись бы все аксиомы из Е'~(А), непременно выполнялась бы и аксиома А, и такой модели, в которой выполнялись бы все аксиомы из Е'~(А) и не выполнялась А, просто не сушествовало бы. Докажем, что система аксиом (А1), (А2), (АЗ) формализованного исчисления высказываний независима с помощью построения соответствующих моделей. Независимость аксиомы (А1). Доказательство осуществляется построением модели, в которой выполняются аксиомы (А2) и (АЗ), но не выполняется аксиома (А!). Лемма 17.2.
Аксиома (А1) не зависит от остальных аксиом (А2) и (АЗ) формализованного исчисления высказываний. Доказательство. Рассмотрим трехэлементное множество М = (О, 1, 2) и введем в нем две операции. Первая операция— унарная, сопоставляюшая каждому элементу А е М элемент из М, обозначаемый А; вторая — бинарная, сопоставляющая любым двум элементам А, В е М элемент из М, обозначаемый А — ь В.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
