Семантический способ

Формальные методы вывода решений в аксиоматических теориях.

ЛЕКЦИЯ 8

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

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

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

2. Выбор системы аксиом исчисления предикатов, как и в случае исчисления высказываний, может осуществляться по-разному. Одной из таких систем аксиом может быть система, в которую включены одиннадцать аксиом исчисления высказываний и две дополнительные аксиомы:

" x [ R(x)® R(y)]; R(t)® $ x R(x),

где t не содержит переменной x.

3. К правилам вывода, которые использовались в исчислении высказываний, добавляются ещё два правила:

а) Правило введения квантора общности

R ® Y(x);

R ® " x Y(x)

б) Правило введения квантора существования

Y(x) ® R,

$ xY(x) ® R

если R не зависит от x.

4. Понятие вывода и доказуемой формулы определяются аналогично этим понятиям в исчислении высказываний.

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

условия:

1.Задан язык теории.

2.Опрелено понятие формулы в этой теории.

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

4.Определены правила вывода в этой теории.

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

Например: доказать что ù (C Ú U)® ù C Ù ù U выводима. Рассмотрим два способа доказательства семантический и синтаксический.

Обозначим A=ù (C Ú U) и B=ù C Ù ù U, тогда исходная формула примет вид: A ® B. Составим таблицу истинности для этой формулы.

Таблица 10

C	U	A	B	A ® B

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

Дата добавления: 2015-06-27