Альтернативные системы аксиом
Методическое пособие - Философия
Другие методички по предмету Философия
)=v. Если для любого другого унификатора w тех же самых термов s и t существует такая подстановка , что композиция . Композицию можно рассматривать как суперпозицию. Если для термов существует хотя бы 1 унификатор, то среди унификаторов существует наибольший общий.
При проведении подстановок нужно следовать правилам:
1)Подстановки применяются только для свободных переменных (в том числе и функциональных), во всех местах их вхождения в данную форму.
2)Переменную можно заменить константой, но не наоборот.
3)Не следует заменять переменные содержащие ту же самую переменную т.е. - неправильная. (один пункт пропустил)
)Одна функция не может подставляться вместо другой но может
)Нельзя вместо свободной переменной ввести уже связанную, иначе вводимая подстановка вхождения переменной не должно попадать в область действия квантора, который связывает данную переменную, а если мы заменяем свободную переменную, то делаем это для всех ее вхождений.
A(x:=t) - получаем из формулы А заменой x на t.
Понятие интерпретации в ЛП. Выполнимость, общезначимость, невыполнимость и противоречивость формул
Интерпретации.
Говорим, что задана интерпретацияI для формулы или множество формул I, если задано не пустое множество Р называемое областью интерпретации. Каждому символу сопоставляется элемент из Р, каждому символу предиката сопоставляется отношение. Каждому символу функции реальная функция из множества G. Формула выполнима, если есть интерпретация, в которой она истина.
Определение: Замыканием формул А с параметрами х1,х2,..,хn является формула вида: для каждого х1,х2,..хn А. Формула исчисления предикатов называется общезначимой, если ее замыкание истинно в любой интерпретации. При проверке общей значимости формул важно помнить, что по ее параметрам берутся кванторы всеобщности. Например, квадрат действительного числа положителен, но оно не общезначимо, т.к. 0 в квадрате =0, что не является положительным числом. Общезначимым будет утверждение квадрат любого действительного числа неотрицателен. Формула называется невыполнимой, если замыкание ее отрицания общезначимо. Формула выполнима если не верно, что она невыполнима. Общезначимость формулы - это обобщение тавтологии в ИВ. Можно сформулировать это утверждение более формально. Интерпретация называется моделью формул или множеством формул, если на ней все формулы тождественно истины. Формулы А и В эквивалентны, если каждая из них является логическим следствием другой.
Общезначимость тавтологий
Общезначимые формулы - это обобщение тавтологий в исчислении высказываний. Исчисление высказываний позволят выводить все тавтологии из некоторого набора базисных тавтологий (названных аксиомами) с помощью некоторых правил вывода (на самом деле единственного правила modusponens).
1)Пусть A - тавтология, x1,. . . , xn - набор пропозициональных переменных, которые входят в A, а F1, . . . , Fn - формулы ИП. Тогда формула A(F1, . . . , Fn) общезначима.
2)Докажем, что формула ? x ? y A(x, y)>? y ? x A(x, y) общезначима.
Интерпретацию бинарного предикатного символа удобно представлять в виде ориентированного графа (быть может, бесконечного). Множествовершин графа совпадает с областью интерпретации,а упорядоченная пара (x, y) принадлежит множествурёбер графа тогда и только тогда, когда пара (x, y)принадлежит отношению [A].
При таком понимании посылка написанной формулы означает, что в графе есть вершина x, из которойидут рёбра во все остальные вершины. Но тогда длялюбой вершины графа найдётся входящее в неё ребро(оно выходит из вершины x). Именно это и утверждаетзаключение формулы.
Исчисление предикатов 1-го порядка
Говорят, что задано исчисление предикатов первого порядка, когда:
) задан алфавит:
счётного множества X символов переменных;
счётного множества P предикатных символов;
счётного множества F функциональных символов;
символов пропозициональных связок > и
кванторного символа ?(квантор всеобщности);
служебных символов: скобок закрывающей ) и открывающей (, а также символа запятой,.
2) введено понятие формулы;
) заданы аксиомы исчисления высказываний:
A>(B>A) (A1)
(A>(B>C))>((A>B)>(A>C)) (A2)
(B>A)>(( B>A)>B) (A3)
и кванторныесхемы аксиом:
?xA>A(x:=t) в условиях (A4)
? x(A>B)>(A>?xB) в условиях (A5)
) заданы правила вывода:
modus ponens:
если выводимы формулы A и A>B, то выводима формула B.
правилом обобщения (Gen):
если выводима формула A, то выводима формула ?xA.
Общезначимость для каждого хAA(x:=t)
Теорема. Если терм t свободен для переменной x в формуле A, то формула ?xA>A(x:=t) общезначима.
Доказательство:
Если заключение импликации истинно, то и вся импликация истинна.
Теперь предположим, что в некоторой интерпретации при некоторой оценке переменных ? формула A(x:=t) имеет оценку ложь.
Обозначим через ? оценку терма t при оценке переменных ?. Рассмотрим оценку переменных ??, которая отличается от оценки ? разве что в переменной x, оценка ?? которой равна ?. Сравним оценку формулы A при оценке переменных ?? и оценку формулы A(x:=t) при оценке переменных ?.
Так как терм t свободен для переменной x в формуле A, то свободны все вхождения переменных в экземпляры терма t, подставленные вместо свободных вхождений x. Поэтому при оценке формулы A(x:=t) оценка любой вершины, которая лежит на пути от вершины t к корню, использует лишь оценку ? терм?/p>