5. Теорема о существовании модели

Определение. Множество формул сигнатуры называется противоречивым или несовместным, если для некоторых формул в доказуема секвенция .

Множество формул сигнатуры , не являющееся противоречивым, называется непротиворечивым или совместным.

Определение. Формула сигнатуры называется логическим следствием множества формул сигнатуры , если в доказуема секвенция для некоторых формул .

Теорема о существовании модели: Если - совместное множество формул сигнатуры , то имеет модель мощности, не превосходящей .

Следствие 1 (теорема Геделя о полноте). Любая тождественно истинная секвенция доказуема в .

Т.е. проверка доказуемости сводится к проверке тождественно истинности, но в отличие от ИВ в общем случае не существует алгоритма распознавания доказуемости формул , т.е. - неразрешимо. Однако метод резолюций позволяет определить невыполнимость формул.

Определение. Множество формул сигнатуры называется локально выполнимым, если любое конечное подмножество множества выполнимо.

Следствие 2 (теорема Мальцева о компактности). Каждое локально выполнимое множество формул сигнатуры - выполнимо.

Следствие 3. Если для любого множество формул сигнатуры имеет модель мощности , то имеет бесконечную модель.

6. Исчисление предикатов гильбертовского типа

Формулами называются формулы , секвенций нет.

Аксиомами являются следующие формулы для любых формул φ, , χ, :

1. ()

2. ()((())())

3. ()

4. ()

5. ()(()(()))

6. ()

7. ()

8. ()(()(()))

9. ()(())

10. 

11. 

12. 

13. 

14. 

Правила вывода в :

2. 

3. ,

где x не входит свободно в .

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

Предложение 1. Для любых формул φ,  сигнатуры в справедливы следующие соотношения:

1. 

2. 

3. 

4. 

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

а) Пусть - доказуемое предложение, например , тогда

b) для доказательства возьмем вторую аксиому с подстановкой , , , тогда получим

в аксиому 1 подставим , , продолжим доказательство:

с) аналогично

d) . 

Справедлива теорема о дедукции: Если Γ,φ ├, то Г ├, где Г ― набор некоторых формул φ₁, ..., φ_n..

Теорема об эквивалентности и

1. Секвенция ₁,... ,_n ├ доказуема в тогда и только тогда, когда формула  выводима в из формул ₁,... ,_n .

2. Секвенция ₁,... ,_n ├ доказуема в тогда и только тогда, когда формула выводима в из формул ₁,... ,_n .

Следствие. - непротиворечиво.

7. Скулемизация алгебраических систем

Рассмотрим конструкцию, предложенную Скулемом и позволяющую расширять сигнатуру данной алгебраической системы так, чтобы появилась возможность "убирать" кванторы у формул. Необходимость такого преобразования объясняется тем, что работать с формулами, содержащими кванторы, значительно трудней, чем с бескванторными. Далее будет изложен метод резолюций в исчислении предикатов, использующий скулемизацию.

Алгебраическая система A = <Α; Σ> называется обогащением алгебраической системы A' = <Α';Σ'>, если А = Α', Σ' Σ и совпадают интерпретации всех сигнатурных символов из Σ' в системах A и A'.

Если система A сигнатуры Σ является обогащением системы A' сигнатуры Σ', то A' называется обеднением алгебраической системы A.

Пример 1. Система A = <Ζ; +, •, 0,1> является обогащением системы B = <Ζ;+,0,1>, а система C= <Ζ;+,0> — обеднением системы B.

Определение. Пусть Σ — некоторая сигнатура, — сигнатура, полученная из Σ добавлением:

а) новых константных символов для каждой формулы φ

сигнатуры Σ, имеющей вид ;

б) новых n-местных функциональных символов для каждой формулы сигнатуры Σ, имеющей n > 0 свободных переменных.

Тогда сигнатура называется скулемизацией сигнатуры Σ. Через S(Σ) обозначим множество следующих предложений сигнатуры , называемых аксиомами Скулема:

а) для каждой формулы сигнатуры Σ;

б) для каждой формулы (п > 0) сигнатуры Σ.

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

Определение. Если A — алгебраическая система сигнатуры Σ, то любое ее обогащение A^S = <Α; >, являющееся моделью множества S(Σ), называется скулемизацией системы A. Возникающие при обогащении константы и операции, соответствующие символам и , называются скулемовскими константами и скулемовскими функциями соответственно.

Отметим, что в отличие от и S(Σ) скулемизация A^S не определяется однозначно, поскольку из существования элементов, которые можно подставлять вместо переменных , вообще говоря, не следует их единственность.

Предложение 1. Любая алгебраическая система A имеет некоторую скулемизацию A^S .

Доказательство. Если , то в качестве значения берем элемент , для которого A╞ , если такой элемент существует, и произвольный элемент , если такого нет. Для формулы (n > 0) и элементов в качестве берем элемент , для которого A╞ , если такой элемент существует, и произвольный элемент , если такого нет. 

Скулемизация позволяет "убирать" кванторы у формул старой сигнатуры Σ. Однако после обогащения появляются формулы новой сигнатуры , в которых кванторы "остаются". Для устранения этого недостатка используется проведение скулемизации счетное число раз.

Пусть Σ — сигнатура, S(Σ) — множество аксиом Скулема для сигнатуры Σ. Положим по индукции , . Cигнатура называется полной скулемизацией сигнатуры Σ.

Определение. Если A — алгебраическая система сигнатуры Σ, то любое ее обогащение A^cS = <A; >, являющееся моделью множества , называется полной скулемизацией системы A.

Предложение 2. Любая алгебраическая система A имеет некоторую полную скулемизацию A^cS.

При работе с методом резолюций нам предстоит с помощью скулемизации снимать кванторы с формул, находящихся в предклазуальной нормальной форме. Говорят, что формула φ находится в клазуалъной нормальной форме (КлНФ), если она получается из формулы φ, находящейся в предклазуальной нормальной форме, удалением всех кванторов существования с одновременной заменой соответствующих переменных на термы, определяемые аксиомами Скулема, и последующим удалением всех кванторов всеобщности.

Пример 2. В примере 1 главы о нормальных формах найдена формула

xyuv (φ(x, у)  (и,v)),

находящаяся в ПКНФ. С помощью скулемовских функций и (заменяющих переменные у и u соответственно), эта формула преобразуется к следующей формуле, находящейся в КлНФ: (φ(x, )  ( ,v)).

Пример 3.Ввести скулемовские функции для формулы: . Так как предикат имеет конкретный вид, то и подбирем некоторые конкретные скулемовские функции для области определения . Пусть и , тогда подбирем f₁ и f₂, чтобы формула была истинна для любых x, y. Например, и , тогда