logo
DM_shpory

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

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

.

К этим аксиомам добавляются две новые схемы аксиом:

и ,

где (x) — произвольная предикатная формула, в которой переменная x не находится в области действия кванторов y и y, а формула (y) получена заменой в (x) каждого свободного вхождения переменной x на y.

Правилами вывода исчисления предикатов являются правило модус поненс и следующие два правила:

Правило модус поненс (правило отделения, правило вывода в формальной логике) означает, что из истинности формулы A (малая посылка) и  B (большая посылка) следует истинность B.

Выводом формулы  в исчислении предикатов называется конечная последовательность формул 1, . . ., m такая, что каждая из формул i либо есть аксиома, либо получается из некоторых предшествующих ей формул по одному из перечисленных правил вывода, и m совпадает с . Формула  выводима в исчислении предикатов, или является теоремой, если можно построить вывод этой формулы. Согласно теореме Геделя о полноте, все общезначимые предикатные формулы и только они выводимы в классическом исчислении предикатов.

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