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

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

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

В этом разделе логики выделяют три класса формул:

· Тождественно истинные формулы - при исполнении логических и кванторных операций принимают значение «истины» для всех интерпретаций предметных постоянных, функциональных и предикатных символов. Большинство из них - аксиомы исчисления предикатов. Например: ∃_x(F(x))↔¬∀_x(¬F(x)).

· Тождественно ложные формулы - при исполнении логических и кванторных операций принимают значение «ложь» для всех интерпретаций предметных постоянных, функциональных и предикатных символов. Например, ∃_x(F(x))&∀_x(¬F(x)).

· Выводимые формулы - при исполнении логических и кванторных операций принимают значение «истина» не для всех интерпретаций предметных постоянных, функциональных и предикатных символов. Например, ∃_x(F(x))→¬∀_x(F(x)). Выводимость формулы записывается так: F₁,F₂,…, F_n|⎯ F, где слева от знака выводимости записывают множество посылок и необходимых аксиом, а справа – заключение F («верно, что F выводимо из посылок и аксиом F₁,F₂,...,F_n»). Другая форма вывода заключения:

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

Вывод заключения на языке математической логики - это доказательство теоремы |⎯F₁&F₂&…&F_n→F. В процессе доказательства последовательно используют аксиомы и законы логики предикатов, правила введения и удаления кванторов, специфические правила исчисления предикатов, правила modus ponens и modus tollens.

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

П1.Удаление квантора всеобщности: если выводима формула ∀x(F(x)), то, заменив предметную переменную x на терм t, можно удалить квантор всеобщности и получить выводимую формулу:

П2. Введение квантора всеобщности:

a) если выводима формула F(t), то, заменив терм t на предметную переменную x, можно ввести квантор всеобщности и получить выводимую формулу:

b) если выводима формула (F₁(t)→F₂(x)) и F₁(t) не содержит свободной переменной x, то выводима формула:

П3. Удаление квантора существования: если выводима формула ∃_x(F(x)), то, заменив предметную переменную х на предметную постоянную ‘а’, можно удалить квантор существования и получить выводимую формулу:

П4. Введение квантора существования:

a) если выводима формула F(t), то, заменив терм t на предметную переменную x в заданной области интерпретации, можно ввести квантор существования и получить выводимую формулу:

b) если выводима формула F₁(x)→F₂(t) и F₂ не содержит свободной переменной x, то выводима формула:

П5. Формирование ПНФ формулы:

a) если при исполнении логических операций один из предикатов формулы F_i не содержит переменной x, связанной в другом предикате формулы F_j, и формулы выводимы, то выводима одна из формул:

b) если выводимы формулы ∀_x(F₁(x))∨∀_x(F₂(x)) и ∃_x(F₁(x))&∃_x(F₂(x)), то при смене в левой формуле имени переменной получим также выводимые формулы:

Дата добавления: 2014-01-04