Сводка определений и основных фактов, страница 2

л

а

,

а

- множество замкнутых формул. Тогда ϕ₀ называется логическим следствием Г (обозначается

), если каждая модель для Г является моделью для ϕ₀.

Сведем задачу нахождения логического следствия к проблеме общезначимости.

Теорема (о логическом следствии). Если

- замкнутые формулы, то

эквивалентно

(т.е. для любого логического следствия данного множества формул такая импликация общезначима).

Множество всех логических следствий – это и есть множество всех логических законов.

Замечание. Существуют формулы, выполнимые на конечных интерпретациях и невыполнимые на бесконечных.

Рассмотрим формулу

, где

,

,

.

Теорема: На любой интерпретации I, такой, что - конечное множество,

выполнима, однако

не общезначима.

Определение. Упорядоченная пара множеств формул

называется семантической таблицей.

Если пересечение Г и Δ не пусто, то такая семантическая таблица называется закрытой.

Если ϕ - формула, то таблицей для формулы ϕ назовем семантическую таблицу

Содержательный смысл семантической таблицы таков: Г – множество формул, которые мы хотим считать истинными, Δ - множество формул, которые мы хотим считать ложными. Тогда закрытая таблица противоречива, а таблица для формулы ϕ будет являться исходным состоянием для доказательства общезначимости формулы ϕ от противного.

Определение. Таблица называется выполнимой, если существует интерпретация I, такая, что любая формула ϕ из множества Г будет выполнима в данной интерпретации, а любая формула ψ из множества Δ выполнимой в данной интерпретации не будет.

Утверждение. Закрытая таблица не является выполнимой.

Для доказательства общезначимости формулы, следует преобразовать ее таблицу. Эта операция называется табличным выводом.

Определение. Правилом табличного вывода называется фигура вида

.

Введем следующую систему правил:

1.

:

. L означает, что мы преобразовываем левую часть таблицы, причем отрицание – главная логическая связка в формуле ϕ.

2.

:

.

3. :

.

4. :

. В данном случае происходит ветвление процесса табличного вывода, и выполнимость Т₀ эквивалентна выполнимости или Т₁, или Т₂.

5.

:

.

6.

:

.

7. :

.

8. :

.

С помощью данных правил можно существенно упростить таблицу. Для упрощения формул с кванторами требуется ввести дополнительные понятия.

Определение. Подстановкой называется любое отображение

. Областью подстановки называется множество

. Если область подстановки конечна, то такая подстановка называется конечной. Множество всех конечных подстановок будем обозначать как Subst. Если θ - конечная подстановка, то она представима в виде множества связок:

.

Определение. Пусть Е – логическое выражение θ - постановка

. Тогда запись вида Еθ будет называться результатом применения подстановки θ к Е. Он определяется следующим образом:

1) Е – переменная (). Тогда .

2) Е – константа (Е = с). Тогда

.

3) Е – составной терм (). Тогда

.

4) Е – атомарная формула (). Тогда

.

5) Е – формула вида

, где означает конъюнкцию, дизъюнкцию или импликацию. Тогда

, а если Е – формула вида

, то

.

6) Е – формула с квантором

или

. Тогда

.

Определение. Переменная х является свободной для терма t в формуле ϕ, если в ϕ нет свободных вхождений переменной х в области действия кванторов, связывающих переменные из множества (множества переменных терма t).

На основе понятия подстановки введем 4 новых правила табличного вывода:

9.

:

при условии, что переменная х в формуле ϕ(х) свободна для терма t.

10.

:

, где с – это константа, которая не содержится в Г, Δ или ϕ(х).

11.

:

.

12.

:

Таким образом, имеем 12 правил, располагая которыми, можно построить табличный вывод.

Определение. Табличным выводом семантической таблицы Т₀ называется корневое дерево, вершины которого помечены таблицами, причем это дерево удовлетворяет следующим требованиям:

1. Корневая вершина помечена таблицей Т₀.

2. Каждая висячая вершина должна быть помечена либо закрытой таблицей, либо такой таблицей, что в ней содержатся только атомарные формулы (т.е. без связок и кванторов).

3. Не висячая вершина, помеченная таблицей Т_i, обязательно имеет одного или двух наследников, которые получаются из Т_i по одному из 12 правил табличного вывода.

Дерево (или вывод) считается успешным (успешный вывод называется доказательством), если каждая ветвь дерева завершается закрытой таблицей.

Для табличного вывода как для доказательства общезначимости сразу возникают следующие вопросы:

- корректности;

- полноты (является ли табличный вывод универсальным способом доказательства);

- эффективности (каким образом и в каком порядке следует применять правила табличного вывода).

Теорема (корректности): Если таблица Т₀ имеет успешный табличный вывод, то Т₀ невыполнима.

Следствие 1. Если таблица

имеет успешный табличный вывод, то формула ϕ общезначима.

Следствие 2. Если таблица имеет успешный табличный вывод, то формула ϕ является противоречивой.

Теорема (полноты табличного вывода): Если таблица Т₀ невыполнима, то Т₀ имеет успешный табличный вывод.

Следствие 1 (теорема Гёделя о полноте): Если формула ϕ общезначима, то таблица

имеет успешный табличный вывод.

Следствие 2 (теорема Ливенгейма-Сколема о счетной модели): Если формула ϕ выполнима, то ϕ имеет модель с не более, чем счетной бесконечной областью интерпретации.

Следствие 3 (теорема Мальцева о компактности): Пусть

- произвольное множество формул. Тогда Г имеет модель тогда и только тогда, когда каждое ее подмножество имеет модель.

Доказательство утверждения предлагается провести самостоятельно.

2.

М

е

т

о

д

р

е

з

о

л

ю

ц

и

й

Метод резолюций – один из наиболее эффективных способов автоматического доказательства теорем. Общие принципы доказательства утверждений с помощью метода резолюций таковы:

1. Если мы хотим доказать общезначимость формулы ϕ, то для этого достаточно показать, что формула

противоречива (т.е. провести доказательство от противного).

2. Формула ϕ₁ приводится к предваренной нормальной форме ϕ₂, в которой все кванторы стоят в начале формулы.

3. Формула ϕ₂ приводится к сколемовской стандартной форме, в которой отсутствуют кванторы существования:

, где , а . Следует убедиться, что содержимое ϕ не было потеряно.

4. Доказательство общезначимости ϕ сводится к доказательству противоречивости системы дизъюнктов . Для этого применяется правило резолюций Робенсона: . Чтобы применение этого правила стало возможным, Робенсон ввел алгоритм унификации для системы {. Если L’ и L’’ унифицированы, то такой метод построения вывода для общезначимой формулы станет полным.

Введем новую связку

, которая эквивалентна формуле

.

Определение. Формулы ϕ и ψ называются равносильными, если общезначима формула

.

Утверждение. Отношение равносильности является отношением эквивалентности.

Утверждение. Если формулы ϕ и ψ равносильны, то:

1. Из общезначимости ϕ следует общезначимость ψ;

2. Из выполнимости ϕ следует выполнимость ψ;

3. Если I является моделью для ϕ, то она является также моделью для ψ.

Теорема: Следующие пары формул являются равносильными:

у не содержится в

Определение. Запись

означает, что в формуле ϕ содержится подформула ψ; запись

означает замену в формуле ϕ подформулы ψ на χ.

Теорема: Пусть ϕ, ψ, χ - произвольные формулы. Тогда из равносильности ψ и χ следует, что

.

Определение. Литера – это либо атом

, либо

.

Определение. Дизъюнкт – это либо дизъюнкция атомов , либо пустой дизъюнкт - тождественная ложь.

Определение. Предваренная нормальная форма – это формула вида , где - кванторная приставка, а М – бескванторная формула (матрица), являющаяся КНФ вида , где D

_i – непустой дизъюнкт.

Теорема (о предваренной нормальной форме): Для любой замкнутой формулы ϕ существует равносильная ей предваренная нормальная форма ψ.

Определение. Сколемовская стандартная форма – это предваренная нормальная форма вида

.

Теорема (о сколемовской стандартной форме): Для любой замкнутой формулы ϕ существует сколемовская нормальная форма ψ, причем ϕ выполнима тогда и только тогда, когда выполнима ψ.

Лемма (о сколемизации): Пусть замкнутая формула ϕ имеет вид

и пусть также имеется функциональный символ

. Тогда формула ϕ выполнима тогда и только тогда, когда выполнима формула