Полнота ИВ

Опр. ИВ называется полным, если в нем выводима любая тавтология (ТИФ).

Т. (о полноте) ИВ полно, т.е. если формула является тавтологией, то она выводима в ИВ.

Доказательство:

Пусть А – ТИФ, тогда Аs=А для любого набора s.

Применим лемму о полноте

x1s, х2s, …хns├Аs=А.

Пусть s – набор, имеющий вид s=<g1, g2, …, gn-1, 1>. Для этого набора получаем:

x1s, х2s, …хn-1s, хn├А………………..(1).

Возьмем другой набор s=<g1, g2, …, gn-1, 0>. Для него имеем по лемме о полноте:

x1s, х2s, …хn-1s, ├А…………………(2).

К соотношениям (1) и (2) применим правило удаления дизъюнкции:

x1s, х2s, …хn-1s, ├А, расшифруем дизъюнкцию:

├ – пример 1.

Выводимые формулы из списка гипотез можно исключать (элеменировать) по свойству 3°:

x1s, х2s, …хn-1s├А.

Аналогично удаляются остальные гипотезы. Через конечное число шагов получим: х1├А

├А, применяем удаление дизъюнкции: ├А Þ ├А Þ├А.

Пример: Пусть А – тавтология, содержащая 2 переменные.

По лемме справедливы выводимости:

Следствие: Формула выводима в ИВ Û, когда она является тавтологией.

Это вытекает из теоремы о полноте и Т1 из предыдущего пункта.

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

Разрешимость И.В.

Опр. ИВ называется разрешимым, если существует алгоритм (метод), позволяющий по любой формуле определить, выводима она этом исчислении или нет и ИВ неразрешимо в противном случае.

Т. ИВ (построенное нами) разрешимо.

Разрешающий алгоритм представляет собой построение таблицы истинности, если формула тождественно истинная, то она выводима.

Независимость системы аксиом

Опр. Аксиома А из системы аксиом S называется независящей от остальных аксиом этой системы, если ее нельзя вывести (доказать) из множества S\{A} всех остальных аксиом системы S, кроме аксиомы А.

Опр. Система аксиом S называется независимой, если каждая ее аксиома не зависит от остальных.

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

Лемма 1. Аксиома (А1) не зависит от аксиом (А2) и (А3) формализованного ИВ.

Доказательство. Рассмотрим трехэлементное множество М={0, 1, 2} и введем на нем 2 операции: унарную, сопоставляющую каждому элементу АÎМ, элемент, обозначаемый и бинарную, сопоставляющую каждой паре А и В элементов из М элемент из М, обозначаемый А®В по правилам, определяемым таблицами:

Если переменным, входящим в формулу ИВ придать некоторые значения из М, то согласно введенным правилам сама формула примет значение из М. Формулу, всегда принимающую значение 0, назовем выделенной.

Покажем, что всякая формула, получающаяся по схеме аксиом (А2) является выделенной. Для этого составим таблицу значений формулы (А2):А®(В®С)®((А®В)®(А®С))

А	В	С	В®С	А®(В®С)	А®В	А®С	(А®В)®(А®С)	(А2)

Покажем, что всякая формула, получающаяся по схеме аксиом (А3), также является выделенной:

А	В				А®В	(А3)

В третьих покажем, что правило вывода МР сохраняет свойство выделенности. Это видно из таблицы, определяющей операцию ®. Формулы А и А®В принимают одновременно значение 0 только в первой строке, но в этой строке формула В также принимает значение 0.

Т.о., всякая формула, выводимая из аксиом (А2) и (А3) с помощью правила вывода МР является выделенной.

Докажем, что формула (А1) не является выделенной, т.е. ее нельзя вывести из (А2), (А3) с помощью правила МР.

Пусть А=1, В=2:

А®(В®А)=1®(2®1)=1®0=2¹0.

Модель построена. (А1) не зависит от (А2) и (А3).

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