- •Исчисления высказываний
- •Определение формального исчисления
- •Исчисление высказываний генценовского типа
- •Эквивалентность формул
- •Нормальные формы
- •Семантика исчисления секвенций
- •Исчисление высказываний гильбертовского типа
- •Алгоритмы проверки общезначимости и противоречивости в ив
- •Логика и исчисления предикатов
- •Алгебраические системы. Формулы сигнатуры σ. Истинность формулы на алгебраической системе
- •Секвенциальное исчисление предикатов
- •Эквивалентность формул в
- •Нормальные формы
- •Теорема о существовании модели
- •Исчисление предикатов гильбертовского типа
- •Скулемизация алгебраических систем
- •Метод резолюций в исчислении предикатов
- •Некоторые проблемы аксиоматического исчисления предикатов
- •Разрешимость
- •Непротиворечивость и независимость
- •Полнота в узком смысле
- •Полнота в широком смысле
- •Элементы теории алгоритмов
- •Машины Тьюринга
- •Функции, вычислимые на машинах Тьюринга.
- •Рекурсивные функции и отношения
- •Примитивно рекурсивные функции.
- •Примитивно рекурсивные отношения.
- •Частично рекурсивные функции.
- •Рекурсивно перечислимые отношения
- •Неразрешимость исчисления предикатов. Теорема Геделя о неполноте. Разрешимые и неразрешимые теории.
Теорема о существовании модели
Определение. Множество формул сигнатуры называется противоречивым или несовместным, если для некоторых формул в доказуема секвенция .
Множество формул сигнатуры , не являющееся противоречивым, называется непротиворечивым или совместным.
Определение. Формула сигнатуры называется логическим следствием множества формул сигнатуры , если в доказуема секвенция для некоторых формул .
Теорема о существовании модели: Если - совместное множество формул сигнатуры , то имеет модель мощности, не превосходящей .
Следствие 1 (теорема Геделя о полноте). Любая тождественно истинная секвенция доказуема в .
Т.е. проверка доказуемости сводится к проверке тождественно истинности, но в отличие от ИВ в общем случае не существует алгоритма распознавания доказуемости формул , т.е. - неразрешимо. Однако метод резолюций позволяет определить невыполнимость формул.
Определение. Множество формул сигнатуры называется локально выполнимым, если любое конечное подмножество множества выполнимо.
Следствие 2 (теорема Мальцева о компактности). Каждое локально выполнимое множество формул сигнатуры - выполнимо.
Следствие 3. Если для любого множество формул сигнатуры имеет модель мощности , то имеет бесконечную модель.
Исчисление предикатов гильбертовского типа
Формулами называются формулы , секвенций нет.
Аксиомами являются следующие формулы для любых формул φ, , χ, :
()
()((())())
()
()
()(()(()))
()
()
()(()(()))
()(())
Правила вывода в :
,
где x не входит свободно в .
Аналогично определяются понятия доказательства формулы (|- ) и вывод из гипотез .
Предложение 1. Для любых формул φ, сигнатуры в справедливы следующие соотношения:
Доказательство.
а) Пусть - доказуемое предложение, например , тогда
b) для доказательства возьмем вторую аксиому с подстановкой , , , тогда получим
в аксиому 1 подставим , , продолжим доказательство:
с) аналогично
d) .
Справедлива теорема о дедукции: Если Γ,φ ├, то Г ├, где Г ― набор некоторых формул φ1, ..., φn..
Теорема об эквивалентности и
Секвенция 1,... ,n ├ доказуема в тогда и только тогда, когда формула выводима в из формул 1,... ,n .
Секвенция 1,... ,n ├ доказуема в тогда и только тогда, когда формула выводима в из формул 1,... ,n .
Следствие. - непротиворечиво.
Скулемизация алгебраических систем
Рассмотрим конструкцию, предложенную Скулемом и позволяющую расширять сигнатуру данной алгебраической системы так, чтобы появилась возможность "убирать" кванторы у формул. Необходимость такого преобразования объясняется тем, что работать с формулами, содержащими кванторы, значительно трудней, чем с бескванторными. Далее будет изложен метод резолюций в исчислении предикатов, использующий скулемизацию.
Алгебраическая система A = <Α; Σ> называется обогащением алгебраической системы A' = <Α';Σ'>, если А = Α', Σ' Σ и совпадают интерпретации всех сигнатурных символов из Σ' в системах A и A'.
Если система A сигнатуры Σ является обогащением системы A' сигнатуры Σ', то A' называется обеднением алгебраической системы A.
Пример 1. Система A = <Ζ; +, •, 0,1> является обогащением системы B = <Ζ;+,0,1>, а система C= <Ζ;+,0> — обеднением системы B.
Определение. Пусть Σ — некоторая сигнатура, — сигнатура, полученная из Σ добавлением:
а) новых константных символов для каждой формулы φ
сигнатуры Σ, имеющей вид ;
б) новых n-местных функциональных символов для каждой формулы сигнатуры Σ, имеющей n > 0 свободных переменных.
Тогда сигнатура называется скулемизацией сигнатуры Σ. Через S(Σ) обозначим множество следующих предложений сигнатуры , называемых аксиомами Скулема:
а) для каждой формулы сигнатуры Σ;
б) для каждой формулы (п > 0) сигнатуры Σ.
Согласно аксиомам Скулема из существования элемента, который можно подставить вместо переменной в формулу следует возможность подстановки значения некоторой функции (константы ), зависящего от оставшихся свободных переменных.
Определение. Если A — алгебраическая система сигнатуры Σ, то любое ее обогащение AS = <Α; >, являющееся моделью множества S(Σ), называется скулемизацией системы A. Возникающие при обогащении константы и операции, соответствующие символам и , называются скулемовскими константами и скулемовскими функциями соответственно.
Отметим, что в отличие от и S(Σ) скулемизация AS не определяется однозначно, поскольку из существования элементов, которые можно подставлять вместо переменных , вообще говоря, не следует их единственность.
Предложение 1. Любая алгебраическая система A имеет некоторую скулемизацию AS .
Доказательство. Если , то в качестве значения берем элемент , для которого A╞ , если такой элемент существует, и произвольный элемент , если такого нет. Для формулы (n > 0) и элементов в качестве берем элемент , для которого A╞ , если такой элемент существует, и произвольный элемент , если такого нет.
Скулемизация позволяет "убирать" кванторы у формул старой сигнатуры Σ. Однако после обогащения появляются формулы новой сигнатуры , в которых кванторы "остаются". Для устранения этого недостатка используется проведение скулемизации счетное число раз.
Пусть Σ — сигнатура, S(Σ) — множество аксиом Скулема для сигнатуры Σ. Положим по индукции , . Cигнатура называется полной скулемизацией сигнатуры Σ.
Определение. Если A — алгебраическая система сигнатуры Σ, то любое ее обогащение AcS = <A; >, являющееся моделью множества , называется полной скулемизацией системы A.
Предложение 2. Любая алгебраическая система A имеет некоторую полную скулемизацию AcS.
При работе с методом резолюций нам предстоит с помощью скулемизации снимать кванторы с формул, находящихся в предклазуальной нормальной форме. Говорят, что формула φ находится в клазуалъной нормальной форме (КлНФ), если она получается из формулы φ, находящейся в предклазуальной нормальной форме, удалением всех кванторов существования с одновременной заменой соответствующих переменных на термы, определяемые аксиомами Скулема, и последующим удалением всех кванторов всеобщности.
Пример 2. В примере 1 главы о нормальных формах найдена формула
xyuv (φ(x, у) (и,v)),
находящаяся в ПКНФ. С помощью скулемовских функций и (заменяющих переменные у и u соответственно), эта формула преобразуется к следующей формуле, находящейся в КлНФ: (φ(x, ) ( ,v)).
Пример 3.Ввести скулемовские функции для формулы: . Так как предикат имеет конкретный вид, то и подбирем некоторые конкретные скулемовские функции для области определения . Пусть и , тогда подбирем f1 и f2, чтобы формула была истинна для любых x, y. Например, и , тогда