🗊Презентация Формальные логические теории. Исчисление предикатов

ФОРМАЛЬНЫЕ ЛОГИЧЕСКИЕ ТЕОРИИ Исчисление предикатов Глава 2, стр. 30

Определение исчисления предикатов Определение 2.3. Функция одной или нескольких переменных, которая принимает логическое значение ”истина” или ”ложь”, называется предикатом. Переменные предиката называются предметными переменными.

Алфавит Алфавит исчисления высказываний полностью входит в алфавит исчисления предикатов. Большие латинские буквы получают в исчислении предикатов новый смысл: они могут обозначать как постоянные высказывания (например: A, B ), так и переменные высказывания — предикаты (например: F (x), G(x; y) ). Кроме того, в алфавит исчисления предикатов дополнительно по сравнению с исчислением высказываний входят — маленькие латинские буквы с возможными индексами, называемые предметными переменными (например, y, x1, x2 ); они обозначают некоторые объекты, но, в отличие от предметных констант, каждая из предметных переменных может обозначать любой, совершенно произвольный объект; — квантор всеобщности ; — квантор существования .

Кванторы Операции и выражают собой утверждения всеобщности и существования соответственно. Пусть R(x) — некоторый предикат, принимающий значение ”истина” или ”ложь” для каждого элемента x в некоторой предметной области Ω. Тогда под выражением x R(x) понимается: ”для каждого элемента x области Ω высказывание R(x) истинно”. А под выражением x R(x) понимается: ”существует элемент x области Ω, для которого высказывание R(x) истинно”. Переменная x в этих выражениях называется связанной переменной. Предметная переменная, не связанная никаким квантором, называется свободной переменной.

Множество аксиом исчисления предикатов Аксиомы исчисления предикатов не содержат квантора существования. Для того, чтобы ввести в исчисление квантор существования, свяжем его с квантором всеобщности определением:

Правила вывода исчисления предикатов В исчислении предикатов имеется два правила вывода: Правило MP 2. Правило обобщения Gen Это правило позволяет навешивать квантор всеобщности по произвольной переменной.

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

Теорема о дедукции исчисления предикатов Доказательство. Пусть построен вывод формулы из совокупности гипотез : Так же, как и при доказательстве теоремы о дедукции для исчисления высказываний воспользуемся индукцией по i в выводе из . Дополнительно к вариантам, рассмотренным при доказательстве теоремы для исчисления высказываний, в исчислении предикатов имеется еще только один вариант вывода: формула получена в результате применения правила Gen к некоторой предшествующей формуле , j < i. Тогда формула должна иметь вид и по условию теоремы переменная x не должна входить в свободно. По индуктивному предположению . Рассмотрим вывод Так как = , то из получили доказательство .

Теоремы о полноте Мы уже упоминали понятие общезначимости формул, понимая под ними такие формулы, которые принимают значение ”истина” при всех значениях входящих в эту формулу переменных высказываний. Любая математическая теория интересна не только сама по себе, но и с точки зрения ее приложения в практических целях. Формулы исчисления высказываний могут иметь некоторый смысл и обозначать некоторые высказывания естественного языка, если существует какая–либо интерпретация математической теории. Говоря неформально, интерпретировать математическую теорию — это значит связать с ней некоторую предметную область и указать соответствие формальных объектов математической теории и объектов данной предметной области. Определение 2.5. Формула называется общезначимой, если она истинна при любой интерпретации. Логическая формальная теория называется полной, если любая формула выводима в этой теории тогда и только тогда, когда она общезначима.

Теоремы о полноте Полнота теории гарантирует, что во–первых, теория содержит все необходимое для формального вывода, а во–вторых, что ничего лишнего и неверного в этой теории вывести нельзя. Если теория полна, достаточно просто перебирать все варианты выводов в этой теории и получать различные общезначимые формулы (теоремы). Однако, история математики показывает, что существуют очень трудные теоремы, поиск доказательства которых требует больших творческих усилий и временных затрат. Это наводит на мысль, что полнота математических теорий — достаточно редкое свойство. Так оно и есть на самом деле. Исчисление высказываний является одной из весьма редких теорий, для которых выполняется свойство полноты. Теорема 2.7 ( о полноте исчисления высказываний). Формула выводима в исчислении высказываний тогда и только тогда, когда она общезначима.

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

Теоремы о полноте В отличие от исчисления высказываний для исчисления предикатов существует недоказуемая там формула, которую без противоречия можно присоединить к системе аксиом: Теорема 2.8. Исчисление предикатов не полно в узком смысле. Теорема 2.9. (Теорема о полноте исчисления предикатов – теорема Геделя.) Всякая тождественно истинная формула выводима в исчислении предикатов. Иначе говоря, исчисление предикатов полно только в широком смысле.

Логическое следствие Определение 2.6. Формула называется логическим следствием формулы (или логически следует из ) тогда и только тогда, когда для всякой интерпретации, на которой формула истинна, тоже истинна.

Логическое следствие Рассмотрим определение логического следствия не из одной формулы, а из множества формул. Естественно считать, что на истинность следствия должна оказывать влияние истинность всех исходных формул одновременно. Поэтому имеет смысл в качестве оценки истинности рассмотреть конъюнкцию посылок. Теорема 2.10. Пусть — логическое следствие формулы . Тогда & =

Метод резолюций Одним из способов получения выводов является метод резолюций. Предложенный в 1965 году Дж. Робинсоном этот метод позволяет получить максимально сильное следствие множества формул с помощью систематической процедуры последовательного построения логических следствий. Метод использует тот факт, что если некоторая формула является невыполнимой, то наиболее сильное следствие этой формулы — константа false. Определение 2.8. Резольвентой двух дизъюнктов и называется дизъюнкт . Теорема 2.11. Резольвента является логическим следствием порождающих ее дизъюнктов. Даны предложения: D1 = ∨ D1′ , D2 = ∨D2′ , где L - пропозициональная буква, D1′ и D2′ – предложения (в частности, пустые или содержащие только одну букву или ее отрицание). Правило резолюций формулируется так: D1 , D2 ├ D1′ ∨ D2′ . D1 , D2 называются резольвируемыми предложениями, а D1 ′ ∨ D2′ – резольвентой.

Примеры применения метода резолюций

Примеры применения метода резолюций