какие формулы являются теоремами или аксиомами исчисления предикатов

Какие формулы являются теоремами (аксиомами) исчисления предикатов?

Здравствуйте. Вот мое задание: какие формулы являются теоремами (аксиомами) исчисления предикатов?
1) ¬(A&¬A)
2) ¬(A∨¬A)
3) B⊃A∨B
4) A&B⊃A

Из данных вариантов я выбрала 2) и 3), но это неверно. Может подскажете какую литературу почитать на данную тему. Учебник и то, что выдал гугл не очень мне помогло. Например, 3) я понимаю как: В следует из А или В; 4) перевела как А и В следует из А.

Преобразование формулы исчисления предикатов в стандартную форму
Собственно мне нужно решить проблему автоматического преобразования формулы исчисления предикатов в.

Какие из следующих выражений являются формулами логики предикатов?
Какие из следующих выражений являются формулами логики предикатов? В каждой формуле выделить.

Доказать выводимость формулы аксиомами А1-А3 и модус поненс
Свела по теореме дедукции к тому,что надо доказать только выводимость С. Но что-то не получается

Можете почитать следующие книги.

Зюзьков В.М. Введение в математическую логику. ТГУ, 2017
Хаггарти Р. Дискретная математика для программистов. 2-е изд. М.: Техносфера, 2012

На самом деле, сгодится почти любая книга по логике или дискретной математике.

Доказать выводимость формулы основными аксиомами и модус поненс
Пыталась привести конъюнкцию к импликации,что-то не очень. Подскажите с чего начать?

Доказать, что во всяком исчислении высказываний следующие формулы будут теоремами
Доказать,что во всяком исчислении высказываний,в котором правилом вывода является правило МР и в.

Исчисления предикатов
Приведите пример такой формулы F, что подстановка y/x в F корректна, но формула ∀xF →.

Метод резолюций исчисления предикатов
Здравствуйте, подскажите пожалуйста ошибку в этой задаче. Некоторые пациенты любят своих.

Источник

Формализованное исчисление предикатов

Задача формализованного исчисления предикатов (ФИП) та же, что и формализованного исчисления высказываний (ФИВ), — дать аксиоматическую теорию совокупности всех общезначимых формул (тавтологий) логики предикатов, т. е. научиться выводить (доказывать) все такие формулы и только их, исходя из выбранной системы аксиом и с использованием выбранных правил вывода.

Язык формализованного исчисления предикатов

а) если — предикатная буква, — термы, то — формула; при этом все вхождения переменных в эту формулу называются свободными;

г) никаких других формул, кроме тех, которые строятся по правилам а, б, в, нет.

Совокупность называется сигнатурой рассматриваемого исчисления предикатов. Если в сигнатуре отсутствуют функциональные символы, (а значит, функциональные термы), то возникающее исчисление предикатов называется чистым исчислением предикатов. Оно строится для произвольной предметной области и не зависит от взаимосвязи между предметами в этой области. Это чисто логическая теория. Именно о таком чистом исчислении предикатов и пойдет речь. Если же такие связи имеются и они описываются функциями на этой предметной области, то логика проникает в эту область и в эти связи и возникает логическая теория соответствующей математической Дисциплины, или, как говорят, некая формальная математическая теория.

Система аксиом исчисления предикатов

Указанная система состоит из двух групп из которых первая — это аксиомы формализованного исчисления высказываний:

где под понимаются уже любые формулы исчисления предикатов.

Вторая группа аксиом (схем аксиом) — это собственно предикатные аксиомы (схемы аксиом), т.е. аксиомы с кванторами. Выберем в качестве них следующие (называемые аксиомами Бернайса):

Правила вывода в формальном исчислении высказываний

К правилу вывода modus ponens из исчисления высказываний добавляются еще два правила вывода:

Теория формального вывода

Отметим сначала, что так как все формулы, выводимые в исчислении высказываний, являются также выводимыми в исчислении предикатов, то, совершая подстановки в выводимые формулы исчисления высказываний, мы будем получать выводимые формулы исчисления предикатов. (Тем не менее всякую выводимую формулу исчисления предикатов таким способом получить нельзя.) Следовательно, все производные правила вывода, установленные для исчисления высказываний, остаются справедливыми и для исчисления предикатов, и мы будем в логике предикатов широко пользоваться этим.

Дальнейшее изучение формализованного исчисления предикатов строится в форме систематизированной подборки задач на доказательство теорем ФИП. Подборка начинается с построения выводов из аксиом. Затем рассматривается построение выводов из гипотез. Наконец — теорема о дедукции и ее применение к доказательству теорем ФИП. Теорема о дедукции в ФИП формулируется так же, как и в ФИВ:

Источник

Исчисление предикатов

Содержание

Исчисление предикатов [ править ]

Предикаты могут быть 0-местными, в этом случае это хорошо нам известные пропозициональные переменные, принимающие какие-то истинностные значения, в происхождение которых мы не вникаем.

Чтобы построить новое исчисление, нам требуется указать 3 компонента: язык, аксиомы и правила вывода.

Язык [ править ]

Добавим к языку исчисления высказываний новые конструкции с предикатами и получим язык исчисления предикатов. Вот расширенная грамматика:

Добавились 3 новых сущности:

(b) предикаты (они обобщили пропозициональные переменные)

(c) кванторы: всеобщности ( [math] \forall [/math] ) и существования ( [math] \exists [/math] ).

Аксиомы [ править ]

Определение:

Будем говорить, что переменная [math]y[/math] свободна для [math]x[/math] при подстановке в формулу [math]\psi[/math] (или просто свободна для подстановки вместо [math]x[/math] ), если после подстановки [math]y[/math] вместо свободных вхождений [math]x[/math] ни одно ее вхождение не станет связанным.

(11) [math]\forall(\psi) \rightarrow (\psi[x := \alpha]) [/math]

(12) [math](\psi[x := \alpha]) \rightarrow \exists(\psi) [/math]

Пример, когда нарушение свободы для подстановки приводит к противоречию:

[math] \forall(\psi) \to (\psi[x := \alpha]) \\ \psi := \exists a \lnot P(a) = P(b), x := b, \alpha := a \\ \forall b \exists a (\lnot P(a) = P(b)) \to \exists a (\lnot P(a) = P(a)) \\ [/math]

[math] \exists a (\lnot P(a) = P(a)) [/math]

Все аксиомы, порожденные данными схемами в новом языке, мы назовем аксиомами исчисления предикатов.

Правила вывода [ править ]

Добавив эти схемы к схеме для правила Modus ponens исчисления высказываний, мы сможем породить множество правил вывода.

Итог [ править ]

Определение:

Формальная система, составленная из указанного языка, множества аксиом и множества правил вывода, называется исчислением предикатов.

Обратите внимание на требование отсутствия свободных переменных в допущениях.

Доказательство:[math]\triangleright[/math]Упражнение.[math]\triangleleft[/math]

Доказательство разбором случаев. 3 старых случая те же, добавилось 2 новых правила вывода.

Источник

6. Исчисление предикатов

Рассмотрим построение теории первого порядка.

Компонентами теории первого порядка являются следующие.

1. Алфавит составляют:

· Предметные константы – буквы начала латинского алфавита с натуральными индексами: , , …, , , … Предметные символы – это имена (обозначения) предметов.

· Предметные переменные – буквы конца латинского алфавита с натуральными индексами: , , …, , , …

· Функциональные буквы – строчные буквы латинского алфавита с натуральными индексами (верхний индекс указывает число переменных, нижний – номер функциональной буквы): , , …

· Предикатные буквы – заглавные буквы латинского алфавита с натуральными индексами (верхний индекс указывает число переменных, нижний – номер предикатной буквы): , , . (индексы можно не указывать).

· Логические связки: .

· Квантор всеобщности .

· Синтаксические символы – скобки (, ) и запятая.

2. Формула определяется несколькими этапами. Вначале вводится понятие терма.

Определение. 1) Предметные константы и предметные переменные есть Термы.

2) Если , , …, , – термы, – функциональная буква, то – терм.

3) Символ является термом тогда и только тогда, когда это следует из 1) и 2).

Примеры. 1. Пусть – предметная переменная, – предметная константа, , – функциональные буквы. Тогда , – термы.

2. Пусть – предметная переменная, – предметная константа, , – функциональные буквы. Тогда , – термы. Здесь символы , имеют только формальный смысл и не интерпретируются как обозначения тригонометрических функций.

Определение. Если , , …, , – термы, – предикатная буква, то символ называется элементарной формулой.

Другими словами, элементарная формула образуется при применении предикатной буквы к термам.

Примеры. 1. В условиях первого примера, если – предикатная буква, то – элементарная формула.

2. В условиях второго примера, если – предикатная буква, то – элементарная формула.

Теперь определим формулу логики предикатов.

Определение. 1) Всякая элементарная формула есть формула.

2) Если , – формулы, то формулами являются также символы , , .

3) Символ является формулой тогда и только тогда, когда это следует из 1) и 2).

Примеры. 1. В условиях первого примера, – формула.

2. В условиях второго примера, – формула.

В теории первого порядка, как и в исчислении высказываний, допускаются формулы с другими логическими связками, а также допускается использование квантора существования. Известна формула (см. Глава 5. Предикаты.).

Здесь мы ненадолго отвлечемся от построения теории первого порядка и рассмотрим некоторые понятия, связанные с формулами.

Определение. Пусть – формула, – переменная, которая входит в формулу (один или несколько раз). Вхождение в формулу называется Связанным, если либо – переменная в кванторе (), либо находится в области действия квантора . Если вхождение в не связано, то оно называется свободным.

Пример. В формуле вхождения обеих переменных свободные.

В формуле вхождения переменной в посылку связаны, а вхождение в следствие свободно. Вхождение переменной свободно, так как отсутствует квантор .

В формуле вхождения обеих переменных связаны.

Пусть – формула, – переменная в формуле , – терм. Введем обозначение . Тогда – результат подстановки вместо всех свободных вхождений в формулу .

Пример. Рассмотрим подстановку вместо всех свободных вхождений в формулы из предыдущего примера.

В формуле вхождение свободное, следовательно, получаем .

В формуле вхождения переменной в посылку связаны, а вхождение в следствие свободно. Получаем: .

В формуле вхождения обеих переменных связаны, поэтому осуществить подстановку невозможно.

Определение. Терм называется свободным для переменной в формуле тогда и только тогда, когда никакое свободное вхождение в формулу не лежит в области действия квантора , где – переменная в терме .

Пример. Рассмотрим формулу и терм . не свободен для переменной в данной формуле, так как лежит в области действия квантора, тем более не свободен для переменной .

Пусть теперь дан терм . свободен для переменной .

Уточним понятие интерпретации для множества формул теории первого порядка.

Определение. Интерпретацией множества формул называется область интерпретации и заданное на ней соответствие, которое каждой предикатной букве ставит в соответствие -местный предикат на , каждой функциональной букве – -местную функцию на , каждой предметной константе – элемент множества .

При интерпретации формулы превращаются в предикаты на множестве . Если формула не имеет свободных переменных, то после интерпретации она превращается в высказывание.

Пример. На множестве рассмотрим формулу . Интерпретируем эту формулу следующим образом: . Тогда мы получим предикат .

Рассмотрим теперь формулу . При интерпретации она превращается в истинное высказывание .

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

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

Определение. Формулы и называются Логически эквивалентными тогда и только тогда, когда формула логически общезначима.

Справедлива теорема, аналогичная теореме из логики высказываний.

Теорема. Отношение логической эквивалентности является отношением эквивалентности.

Определение. Говорят, что формула Логически влечет формулу (из формулы Логически следует формула ), если формула является логически общезначимой.

Теорема. Отношение логического следствия является отношением предпорядка.

Определение. Формула называется Противоречивой, если она ложна в любой интерпретации.

Теорема. Пусть – формула, – переменная в формуле , терм свободен для переменной в формуле . Тогда формула общезначима.

Доказательство. Пусть имеется некоторая интерпретация исходной формулы, то есть множество и – предикат на . Покажем, что – тождественно истинный предикат. Возьмем произвольный набор значений переменных . Подставим этот набор в предикат. Получим высказывание:

.

Покажем, что это высказывание истинно. Возможны два случая.

1. , следовательно .

2. .

Соотношение выполнено при любых значениях . Подставим этот набор значений в терм : . Подставим последнее выражение в предикат . Получим:

.

Но, поскольку терм свободен для переменной в формуле , получаем:

Следовательно, по свойству импликации получаем, что , что и требовалось доказать.

Теорема. Пусть не является свободной переменной в формуле , – некоторая формула. Тогда формула общезначима.

Доказательство аналогично доказательству предыдущей теоремы.

Теперь мы можем вернуться к построению теории первого порядка.

3. Аксиомы теории первого порядка делятся на два класса:

1) .

2) .

3) .

4) , где терм свободен для переменной в формуле .

5) , где – несвободная переменная в формуле .

Отметим, что аксиомы 1) – 3) – тавтологии, 4) и 5) – общезначимые формулы.

У каждой теории первого порядка свои собственные аксиомы.

├.

2) Правило обобщения Gen.

├.

Определение. Теория первого порядка без собственных аксиом называется исчислением предикатов первого порядка (или чистым исчислением предикатов).

Без доказательства приведем теоремы.

Теорема. Всякая теорема исчисления предикатов логически общезначима, то есть исчисление предикатов непротиворечиво.

Теорема о полноте. Всякая логически общезначимая формула является теоремой исчисления предикатов.

Рассмотрим несколько примеров теорий первого порядка с собственными аксиомами, (приведем только собственные аксиомы). Для удобства вместо предикатных и функциональных букв будем записывать привычные символы.

Источник