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

Вывод в исчислении предикатов — это не пустая и конечная последовательность формул, каждая из которых является либо посылкой, либо получена из предыдущих формул согласно одному из дедуктивных принципов так, что после применения правил É_в и Ø_в все формулы, начиная с последней посылки и вплоть до результата применения данного правила, не используются в дальнейших шагах построения вывода, при этом ни одна переменная не ограничивает сама себя и ни одна индивидуальная переменная не ограничивается абсолютно более одного раза. В том случае, если никакая абсолютно ограничивавшаяся в выводе переменная не встречается свободно в неисключённых посылках и заключении, имеет место завершённый вывод. Определение доказательства в классическом исчислении предикатов идентично определению доказательства в классическом исчислении высказываний, поэтому завершённое доказательство понимается как завершённый вывод из пустого множества неисключённых посылок. Пошаговый переход от одной формулы к другой осуществляется в исчислении предикатов посредством выполнения всех правил вывода, применяемых в исчислении высказываний, к которым добавляются кванторные правила вывода, а именно: 1) введения, 2) исключения кванторов. К дедуктивным принципам введения кванторов относятся правила:

1.1. — введения квантора общности (обозначим символом «"_в»), выражаемое схемой:

А (x/ y, z₁, …, z_n)

^{______________________} , гдеy— абсолютное ограничение, z₁, …, z_n — ограничение.

"x A (x, z₁, …, z_n)

1.2. — введения квантора существования (обозначим символом «$_в»), выражаемое схемой:

А (x/ t)

^___________ .

$x А (x)

2.1.— исключения квантора общности (обозначим символом «"_и»), выражаемое схемой:

"x А (x)

^___________ .

А (x/ t)

2.2. — исключения квантора существования (обозначим символом «$_и»), выражаемое схемой:

$x А (x, z₁, …, z_n)

^{______________________} , гдеy— абсолютное ограничение, z₁, …, z_n — ограничение.

А (x/ y, z₁, …, zg_n)

В правилах «введения квантора существования» и «исключения квантора общности» запись A(x/t) означает результат правильного замещения термом t всех имеющихся в формуле A(x) свободных вхождений предметной переменной x.