Синтаксис логики предикатов

Синтаксис ЛП представляет собой расширение синтаксиса ЛВ и включает перечень определяемых знаков алфавита ЛП (табл. 7.1) и пра­вил построения из них термов и формул ЛП.

Пусть, как и прежде, буквы греческого алфавита φ, φ, у...

В терминах заданного табл. 7.1 алфавита ЛП можно конструировать термы и формулы - символические эквиваленты простых и сложных вы­сказываний согласно следующим правилам.

Таблица 7.1

Алфавит логики предикатов

Примечание: иных знаков, кроме указанных в п. 1-12, в логике предикатов нет.

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

2. Для всех n ≥ 0, n-местный предикат Pⁿ,сопровождаемый nтер­мами, P_t1 , является атомарной формулой ЛП. Терм t., соединен­

ный знаком «=» с другим термом t.,есть атомарная формула ЛП. Ничто другое не является атомарной формулой ЛП.

Для определения, какие последовательности знаков из табл. 7.1 яв­ляются формулами ЛП, введем понятие подформулы (которое повторяет определение, приведенное для формул ЛВ).

Подформула - формула ЛП, входящая в состав дру­гой формулы ЛП

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

Главный логический оператор неатомарной фор­мулы ЛП - союз или квантор, который при ее пост­роении вводится последним

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

¹Метапеременная ξ, вместо которой могут подставляться предметные пере­менные х, у, z,. , читается как «кси».

Напомним, что формула подчеркивается в том случае, если она явля­ется подформулой нижестоящей формулы.

Главным логическим оператором в рассматриваемой формуле явля­ется квантор общности (х), так как при построении дерева формулы он вводится последним. Если бы не было этого квантора, главным логичес­ким оператором был бы знак конъюнкции &.

Следующее выражение не является формулой ЛП:

Введем точные определения области действия логического союза (повторяет определение для формул ЛВ) и квантора.

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

Область действия квантора составляет подформу­

ла, которая начинается сразу после квантора

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

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

лее сложный характер. Для ее осуществления необходимо иметь следу­ющее:

1) предикатные знаки для обозначения свойств вещей или их отно­шений друг к другу;

2) предметные константы для обозначения имен собственных ве­щей;

3) предметные переменные для обозначения области действия кван­тора общности или существования;

4) функциональные знаки для обозначения операций над константа­ми.

Рассмотрим несколько примеров формализации высказываний в ЛП. Примем соглашение не ставить внешних скобок в формулах ЛП, начина­ющихся с кванторов.

7.3.