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

Исчисление предикатов – это формальная система, которая включает алфавит, синтаксические правила построения формул в алфавите, аксиомы (общезначимые исходные формулы), правила вывода, позволяющие строить новые формулы. Выше были определены алфавит и синтаксические правила построения формул в логике предикатов. Исчисление предикатов, подобно исчислению высказываний, добавляет к алфавиту логики предикатов символ секвенции (выводимости) ├, используемый для образования секвенций.

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

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

Определим множество аксиом классического исчисления предикатов:

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

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

1. A®(B®А);

2. (A®(B®C))®((A®B)®(A®C));

3. A®(B®A&B);

4. A&B®A;

5. A&B®B;

6. (A®C)®((B®C)®((AÚB)®C);

7. A®(AÚB);

8. B®(AÚB);

9. (A®B)®((A®ØB)®ØA);

10. ØØA®A;

К этому множеству аксиом добавляются формулы, образованные с использованием кванторов. Если free (x, t, j)[1], то общезначимы формулы:

11. ("xj(x)®j(x/t)); (правило универсальной подстановки);

12. "x(s ® j(x)) ® (s ® "x j(x));

13. (j(x/t)®$xj(x)); (правило экзистенциальной конкретизации)

14. "x(j(x) ® s)®($x j(x) ® s).

Здесь А, В, С, j, s – произвольные формулы, так что каждая строка вышеприведенного списка задает схему аксиом исчисления предикатов. Фиксируя А, В, С, из каждой схемы аксиом можно получить бесконечное множество конкретных аксиом.

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

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

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

Приведем доказательства аксиом логики предикатов 11-14, вводящих кванторы.

Правило универсальной подстановки: ╞( ).

Пусть I["xj(x)]=0. Так как 0®x=1, доказательство в этом случае окончено.

Пусть I["xj(x)]=1. Логическое значение формулы, образованной квантором общности, определяется как минимум из логических значений формулы, находящейся в области действия квантора. Поэтому сделанное предположение означает, что . Пусть t - постоянный терм. Интерпретация терма t – это конкретный элемент предметной области, и логическое значение формулы Согласно определению импликации и в этом случае импликация истинна (1®1=1). Следовательно, данная формула общезначима. Если терм t параметрический и свободен для переменной x в формуле j(x), то результатом подстановки станет формула-условие. Произведя замыкание полученной формулы, получим "x:

Доказательство окончено.

Доказательство правила экзистенциальной конкретизации аналогично.

Докажем общезначимость: если ╞("x(j(x) ® s)®($x j(x)®s)).

Данное выражение означает, что при любых логических значениях атомов, входящих в «большую» формулу, и в любой интерпретации формула остается истинной. В формулу j(x) переменная x входит свободно, а формула s не содержит свободных вхождений переменной x. Если в «большую» формулу входят свободно другие переменные, по ним необходимо провести замыкание путем навешивания квантора общности по всем переменным, кроме переменной x. Введем обозначение

Результатом замыкания будет новая формулировка теоремы:

╞"x ®

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

Если посылка импликации "x ложна, то доказательство окончено, так как импликация с ложной посылкой истинна.

Если же посылка импликации "x истинна, то в соответствии с правилом определения логического значения формулы, образованной квантором общности Если при этом I[s]=1, то доказательство окончено. Если I[s]=0, то тогда и только тогда, когда . Но при этом . Следовательно, I[ ]=1.

Теорема доказана.

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

Фигуры следующих двух видов называются правилами вывода исчисления предикатов: , . Здесь А и В - произвольные формулы, х-произвольная переменная. Первое правило - модус поненс (modus ponens), второе правило – правило обобщения. При применении правила обобщения необходимо учитывать, что формула А, из которой выводится формула "xA, не должна содержать свободно переменную х.

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

Дата добавления: 2014-11-08; просмотров: 831; Нарушение авторских прав

Мы поможем в написании ваших работ!