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

Исчисление предикатов называют еще теорий первого порядка.

В исчислении предикатов, так же как и в исчислении высказываний, на первом по важности месте стоит проблема разрешимости.

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

Теперь же вопрос следует поставить иначе. Принимает ли данная функция значение 1 при:

а) любых предметных переменных и любых предикатах,

б) на некотором множестве предметных переменных и любых предикатах,

в) при некоторых значениях предметных переменных и любых предикатах,

г) является ли она тождественно ложной, т.е. невыполнимой?

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

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

Аксиоматическая теория и правила вывода и составляют исчисления предикатов.

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

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

Аксиомы исчисления предиката.

Пусть A, B и C - любые формулы.

Аксиома 1. A → (B→C).

Аксиома 2. (A → (B→C)) →((A → B) (A→C)).

Аксиома 3. (неB→неA) →((неB → A)→ B).

Аксиома 4. ( х_i) A(х_i) → A(х_j), где формула A(х_i) не содержит переменной х_j.

Аксиома 5. A(х_i) → ( х_j) A(х_j), где формула A(х_i) не содержит переменной х_j.

Правила вывода исчисления предикатов.

(1) Пусть (А(х) → В) и В не содержит переменной х, тогда

((( x)A(x) → В)

Это правило связывания квантором существования.

(2) Пусть В → А(х) и В не содержит переменной х, тогда

(В → (( x)A(x)))

Это правило связывания квантором общности.

(3) Связанную переменную формулы В можно заменить другой переменной, не являющейся свободной в В. Это правило переименования связанной переменной.