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

Содержание слайда: ФОРМАЛЬНЫЕ ЛОГИЧЕСКИЕ ТЕОРИИ Исчисление предикатов Глава 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′ – резольвентой.

Содержание слайда:

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

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