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

В основе исчисления предикатов лежит язык логики пре­дикатов. В остальном оно является расширением исчисления высказываний.

Аксиоматическую систему исчисления предикатов мы по­лучим, добавив к перечисленным выше схемам аксиомати­ческого исчисления высказываний (имея в виду, конечно, переход к языку логики предикатов) следующие четыре схе­мы и одно правило:

1. ∀x A(x) ⊃ A(t) — схема ∀и .

2. A(t) ⊃∃х А(х) — схема ∃в.

3. ∀x (В ⊃ С(х)) ⊃ (В ⊃∀x С(х))  схема введения ∀ в консеквент .

4. ∀x (С(х) ⊃  В) ⊃ (∃x⊃C(x) ⊃ В) — схема введения ∃ в анте­цедент.

A(t) — результат правильной подстановки терма ( вместо х в А(х); В — не содержит х свободно.

Правило ∀в (правило введения квантора общности, иное

A(t) название: правило обобщения): —— (из А непосредственно

выводимо∀x A).

Формально мы сохраняем прежнее определение вывода и доказательства (ясно, что, по существу, изменение состоит в том, что теперь могут использоваться новые аксиомы и но­вое правило), однако, если мы хотим, чтобы отношение фор­мальной выводимости было аналогом семантического поня­тия следования, необходимо ограничить применение ∀в : оно может применяться к некоторой формуле А(х) для обобще­ния лишь по таким переменным х, которые не содержатся свободно в допущениях, от которых зависит эта формула. Чтобы смысл этого ограничения был ясным, мы должны определить понятие зависимости некоторой формулы выво­да от допущений (гипотез). Везде в дальнейшем будем иметь в виду выводы с анализом (то есть обоснованием каждого его шага ссылками либо на принадлежность формулы этого шага к множеству взятых гипотез или аксиом системы, либо на формулы, из которых она получатся, и используемые при этом правила).

Формула В данного вывода зависит от некоторого допу­щения А, если и только если: а) она есть само допущение А;

б) получается из некоторых формул по правилам системы (из С⊃В и С по m. р. или из С по ∀в), какая-нибудь из кото­рых зависит от А. Более простым образом понятие зависимо­сти разъясняется в описываемой далее системе натурального вывода, значительно проще осуществляются там сами выво­ды и доказательства.