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

В логике первого порядка используются традиционные для любой логики: атомы (атомарные формулы), логические связки (И, ИЛИ, НЕ, ИМПЛИКАЦИЯ, ТОЖДЕСТВО), а также термы, предикаты и кванторы.

Для построения атомов разрешается использовать следующие четыре типа символов:

• 1) Индивидные символы, или константы. Это обычно имена объектов такие, как Мэри, Джон, или числа 3, 5 и др.
• 2) Символы предметных переменных. Это обычно строчные буквы х, у, z, возможно, с индексами.
• 3) Функциональные символы. Это обычно строчные буквы f g, h, … или осмысленные слова из строчных букв такие, как отец и плюс.
• 4) Предикатные символы. Это обычно прописные буквы Р, Q, R, … или осмысленные слова из прописных букв такие, как БОЛЬШЕ или ЛЮБИТ.

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

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

Аналогично, если предикатный символ Р имеет п аргументов, то Р называется п-местным предикатным символом. Например, отец — одноместный функциональный символ, а БОЛЬШЕ и ЛЮБИТ — двухместные предикатные символы.

Функция есть отображение, которое отображает список констант в данную константу. Например, отец — функция, которая отображает человека по имени Джон в человека, который есть отец Джона. Следовательно, отец (Джон) представляет человека, даже если его имя неизвестно. В логике первого порядка мы называем выражение отец (Джон) термом.

Определение 2.1. Термы определяются рекурсивно следующим образом:

• 1) Константа есть терм.
• 2) Переменная есть терм.
• 3) Если/ есть «-местный функциональный символ и t_h …, t_n — термы, то fit,… Л) -терм.
• 4) Никаких термов, кроме порожденных применением указанных выше правил, нет.

Так как х и 1 — термы, а плюс — двухместный функциональный символ, то плюс (х, 1) есть терм согласно приведенному определению.

Легко видеть, что плюс (плюс (х, 1), х) и отец (отец (Джон)) — также термы; первый обозначает ((х+1) +х), а второй — дедушку Джона.

Предикат есть отображение, которое отображает список констант в И (истину) или Л (ложь).

Например, если БОЛЬШЕ есть предикат, то БОЛЬШЕ (5,3) есть Я, но БОЛЬШЕ (1, 3) есть Л.

Определив термы, мы можем теперь дать формальное определение атома логики первого порядка.

Определение 2.2. Если Р — «-местный предикатный символ и tt» — термы, то P (t_h … t") - атом (или атомарная формула).

Для построения формул мы можем использовать пять логических связок, приведенных выше, а также два специальных символа V и Д чтобы характеризовать переменные. Символы V и 3 называются соответственно кванторами (все) общности и существования.

Если х — переменная, то (Vx) читается как «для всех х», «для каждого х» или «для всякого л», тогда как (3 х) читается «существует х», «для некоторых х» или «по крайней мере для одного х».

Определение 2.3. Правильно построенные формулы (п.п.ф.) или формулы логики первого порядка рекурсивно определяются следующим образом:

• 1) Атом есть формула.
• 2) Если F и G — формулы, то -> (F), (F vG), (F л G), (F —" G) и (F&#G) — формулы.
• 3) Если F — формула, а х — свободная переменная в F,

то (Vx) F и (3x)F — формулы.

4) Формулы порождаются только конечным числом применений правил 1), 2) и 3).

Пример 2.1.

Переведем утверждение «Каждый человек смертен. Конфуций человек. Следовательно, Конфуций смертен» в формулу.

Обозначим «х есть человек» через ЧЕЛОВЕК (х) и «х смертен» через СМЕРТЕН (х). Тогда утверждение «каждый человек смертен» может быть представлено формулой.

(Ух) (ЧЕЛОВЕК (х) -> СМЕРТЕН (х)),

а утверждение «Конфуций — человек» — формулой ЧЕЛОВЕК (Конфуций)

и «Конфуций смертен» — формулой СМЕРТЕН (Конфуций).

Утверждение в целом теперь может быть представлено формулой.

(Ух) (ЧЕЛОВЕК (х) -> СМЕРТЕН (х)) л ЧЕЛОВЕК (Конфуций) -> СМЕРТЕН (Конфуций).

Формальное доказательство определяется как конечная последовательность формул FI, F2…/Этакая, что каждая формула Fi либо являет ся аксиомой, либо выводима при помощи одного из правил вывода из предшествующих ей формул /у, где j < i.

Формула Т называется теоремой, если существует доказательство, в котором она является последней, т. е. Fr = Т.

В частности, всякая аксиома является теоремой.

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

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

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

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

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