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

Язык логики предикатов

В случае языка логики предикатов наш алфавит будет состоять из следующих групп символов:

• 1) счетный список предметных переменных xi, X2,…;
• 2) счетный список предметных констант <4,02,.;
• 3) счетный список функциональных символов /1, /2, • • •;
• 4) счетный список предикатных символов Р, Р₂>…;
• 5) логические константы И, Л;
• 6) логические связки V, &, —?, «->;
• 7) кванторы V и 3;
• 8) скобки ^и(^и, ^н)» и запятая ^и," •

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

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

Т1) Однобуквенное слово, состоящее из предметной переменной либо предметной константы, есть терм.

Т2) Если $ 1,…, f_n — термы и д — функциональный символ арности п, то слово g (t 1,…, t_n) — есть терм.

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

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

Ф2) Если ?1,…, t_n — термы и g — предикатный символ арности п, то слово g (tu …, t_n) есть формула логики предикатов.

ФЗ) Если / и g — формулы логики предикатов, то слова (-*/). (/ V g), (f&g), (/ -" д), (/ д) суть формулы логики предикатов (такие формулы будем называть атомарными или атомами).

Ф4) Если / — формула логики предикатов их — предметная переменная, то слова (Vx/) и (3х/) суть формулы логики предикатов.

Интерпретацией языка логики предикатов называем четверку (М, F, Fi, F3), такую что:

• а) М — непустое множество, называемое областью интерпретации;
• б) F{ — функция, сопоставляющая каждой предметной константе некоторый элемент из М;
• в) F2 — функция, сопоставляющая каждому функциональному символу / арности п некоторую n-местную функцию, определенную на М и принимающую значения из М.
• г) F₃ — функция, сопоставляющая каждому предикатному символу Р арности п некоторой n-местный предикат определенный на М (функцию со значениями И, Л).

Если задана интерпретация I = (М, F, F₃, F₃), то каждый терм t языка логики предикатов определяет в этой интерпретации некоторую функцию (4)/, определенную на М и принимающую значения из М, а каждая формула / — предикат (/)/, определенный на М (в вырожденных случаях (?)/ может отождествляться с элементом М, а (/)/ с логической константой).

Здесь используется следующее индуктивное определение:

• 1) Если х — предметная переменная, то (х)/ есть тождественная функция от переменной х определенная на М.
• 2) Если а — предметная константа, то (а); есть элемент Fj (а) из М.
• 3) Если для термов ty,…, t_n уже определены …, (t_n)j, / — функциональный символ арности п и ф = Рг (/) — функция от п переменных, отображающая М^п в М, то

4) (И), = И, (Л); = Л.

• 5) Если для термов t,…, t_n уже определены (ti)/,…,(<�")/, Р — предикатный символ арности п и -к = F₃(P) — предикат от п переменных, отображающий М" в (И, Л), то
• 6) Если для /ид уже определены (/)/ и (/)/,
• (/ V p)/i (/&#)/, (/ ff)/, (/ <�"*

истинностных функций для ->, V,&,->, к (/)/ и (<;)/.

7) Если уже определен предикат (/)/ = (xj,…, х_п), то (Vx,/)/ = i/>(xi,…, Xi_i, Xi₊i,…, x_n) — предикат, принимающий значение И на таких наборах e*i,…, aj_i, aj₊i,…, a_n элементов Л/, что для каждого at из М значение ф (аi,…, a_n) есть И. Аналогично, (3xj/)/ = ?(х_ь…, x₄_i,*_j+i,…, х") — предикат, принимающий значение И на таких наборах aj,…, aj_i, aj₊i,…, o_n элементов М, что существует а* из М, что значение ф (ос,…, а") есть И.

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

В формуле 3xi ((Vx2/'i (x2,xi))vP2(^2.a^;i)) первое вхождение переменной хг связанное, а второе — свободное, оба вхождения переменной Xj связанные. Тем самым, у этой формулы одна свободная переменная — хгФормула ((3xiPi (xi)) —"(Ухг-Рг^г))) — пример замкнутой формулы.

Терм t называется свободным для переменной Xi в формуле логики предикатов /, если никакое свободное вхождение х* в / не лежит в области действия никакого квантора Qxj, где Q 6 {V, 3}, Xj — переменная, входящая в терм t.

Например, терм /(xj, хз) свободен для х в формуле.

но не свободен для xj в формуле.

Если / — есть формула логики предикатов, х — свободная предметная переменная формулы / и t — терм, то через Sf /

обозначим результат подстановки в / терма t вместо всех свободных вхождений переменной х.

Лемма 15 (об интерпретациях). Если / — есть формула логики предикатов, х — свободная предметная переменная формулы / и t — терм, свободный для переменной х в }, то для любой интерпретации I формула (Sff)j определяет предикат, получающийся подстановкой в (/)/ функции (t) / вместо переменной х.

Доказательство этой леммы может получено индукцией по построению формулы / и рекомендуется в качестве самостоятельного упражнения.

Если формула / определяет в интерпретации / предикат, тождественно равный И, то она называется истинной в I, a. I в этом случае называется моделью для /.

Формулу логики предикатов / называем общезначимой, если она истинна во всех интерпретациях, и выполнимой, если хотя бы в одной интерпретации она определяет не тождественно ложный предикат.

Если формула Д &… &/" —> /о общезначима, то /о называется логическим следствием формул /ь • • •, /_п, если формула h <-* /2 общезначима, то формулы f и /2 называются эквивалентными.

Формула ((-'Pi (xi)) V Pi (xi)) есть пример общезначимой формулы. Формула ((->Pi (ii)) V Pi (fi (xi))) — выполнима, но не общезначима.

Далее, как и в случае логики высказываний, договоримся опускать скобки, подразумевая, что -> — самая приоритетная операция, и в случае, когда порядок расставления скобок не существенен (например, для ассоциативных операций). Кроме того, договоримся опускать скобки в формулах вида (QiiQiA)), где Q, Qz — любые кванторы. Например, вместо.

будем писать ^хЗх'р1х₃Р (xi, X2, x₃).

Для указания дедуктивной системы, перечисляющей все общезначимые формулы логики предикатов, воспользуемся имеющимися у нас схемами аксиом А1)-А3), в которых теперь /, <7, h — произвольные формулы логики предикатов, и добавим к ним следующие две схемы аксиом:

А4) Если /, д — формулы логики предикатов их — предметная переменная, не являющаяся свободной переменной формулы /, то формула (Vx (/ —" д)) —?(/—" (Vx#)) есть аксиома.

А5) Если / — есть формула логики предикатов, х — предметная переменная и t — терм, свободный для переменной х в /, то формула (Vx/) —" S*/ есть аксиома.

Правилами вывода в этой дедуктивной системе являются уже известное нам правило modus ponens, а также новое правило (известное как правило обобщения), позволяющее из формулы / выводить формулу (Vx/). Как и в случае логики высказываний, ограничиваемся только логическими связками -" и причем из кванторов используем только квантор общности. Легко видеть, что квантор существования может быть выражен через квантор общности и отрицание: формулы З_хЛ (х) и ^_,(Vx («^,A (x))) эквивалентны.

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

Теорема 21 (Геделя о полноте исчисления предикатов).

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

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

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

Теорема 22 (Черч). Для логики предикатов не существует алгоритма, распознающего общезначимые формулы.

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