Вопрос 6.
Логика предикатов.
Понятие ``предикат'' обобщает понятие ``высказывание''. Неформально говоря, предикат – это высказывание, в которое можно подставлять аргументы. Если аргумент один – то предикат выражает свойство аргумента, если больше – то отношение между аргументами.
Так же, как и в логике высказываний, в Л.п. любое высказывание считается либо истинным, либо ложным. Однако при этом кроме пропозициональных связок «]», «&», «V», «—>», «<—>» используются еще три логических оператора: оператор предикации «<—», квантор общности «V» и квантор существования «Э».
Предваренная нормальная форма предикатов.
Теорема. Для всякого предиката существует равносильная ему предваренная нормальная форма.
Формулы, в которых из логических связок имеются только дизъюнктивные, конъюнктивные и отрицательные, причем отрицание встречается только непосредственно пред предикатом, называются нормальными.
Нормальная формула называется предваренной нормальной, если она не содержит кванторов или все кванторы стоят впереди.
Процедура приведения формулы к предваренной нормальной формуле:
Удаляем все связки, кроме «]», «&», «V».
Чтобы провести отрицание в глубь формулы, применяем вынос квантора через отрицание, используя законы Де Моргана.
Переименовываем переменные, если это необходимо.
Используем специальные формулы, для того чтобы вынести кванторы в начало выражения.
Сколемизация и элиминация.
Сколемизация — это процесс устранения кванторов существования путем их удаления.
1.Если перед квантором существования квантора всеобщности не стояло, то мы его удаляем, а его переменную везде заменяем на константу, которой еще не было.
2. Если пред квантором существования квантор всеобщности стоял, то мы его удаляем, а его переменную везде заменяем на функцию от переменных, по которым были эти кванторы всеобщности.
Элиминация (или устранение) кванторов — это процесс нахождения, для всякой заданной формулы, другой формулы, не содержащей кванторов и эквивалентной данной.
Элиминацию кванторов ввел Альфред Тарский в 1935 году как метод доказательства разрешимости теорий. Метод состоит в предъявлении алгоритма, который по всякой формуле в данном языке строит эквивалентную ей бескванторную формулу. Имея этот метод (и алгоритм проверки выводимости бескванторных формул в данной теории, который для многих важных теорий существует и довольно прост), мы получаем алгоритм проверки выводимости любых формул в данной теории.
Эрбрановский универсум множества дизъюнктов.
Чтобы доказать невыполнимость множества дизъюнктов, нужно доказать его ложность при всех интерпретациях на всех областях. В общем случае это невозможно, так как областей интерпретации формул в логике предикатов бесконечно много. Тем не менее, возможно рассмотрение такой специальной области Н, что S невыполнимо тогда и только тогда, когда S ложно при всех интерпретациях на этой области. Такую область называют эрбрановским универсумом множества S. Он строится следующим образом. Пусть Н0 - это множество констант, встречающихся в S. Если в S не входят константы, то Н0 состоит из одной произвольной константы. Каждое следующее множество H1+j есть объединение Ht и множества всех термов вида fn(ti,t2,...tn) для всех функций fn, встречающихся в S, где t, (j=l,2,...,n) принадлежат Н,. Тогда каждое Н, называется множеством констант i-ro уровня для S и Ноо называется эрбрановским универсумом S.
Теорема Эрбрана.
Теорема Эрбрана позволяет нам для проверки* невыполнимости множества дизъюнктов ограничиваться только рассмотрением его интерпретаций над эрбрановским универсумом S.
Теорема Эрбрана. Множество дизъюнктов S невыполнимо тогда и только тогда, когда существует конечное невыполнимое множество S' основных примеров дизъюнктов S.