Натуральная система исчисления предикатов

Постулатами системы (исходными правилами) являются все правила натуральной системы исчисления высказываний и правила для кванторов.

 Правила вывода для выражений с кванторами:

∀в :

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

Если в выводе получена формула ∃х А(х} и нужно вывес­ти В, не выводимую непосредственно из имеющихся фор­мул, вводим допущение А(х), применяя способ рассуждения согласно ∃и.

Рассмотрим несколько примеров выводов.

Схема доказательства формул вида: ¬∃x A(x) ⊃∀x¬A(x):

+ 1. ¬∃x A(x) [1].

+ 2. A(x) [2].

   3. ∃x A(x) [2] – из 2, ∃в.

   4. ¬ A(x) [1] – из 1,3, ¬в.

   5. ∀x¬A(x) [1] – из 4, ∀в.

   6. ¬∃x A(x) ⊃∀x¬A(x) [ - ] – из 5, ⊃в.

Схемы доказательств рассмотренных в аксиоматической системе аксиом «введения ∀ в консеквент» и «введения ∃ в антецедент»:

Предполагается, что А не содержит х свободно.

+  1. ∀x (A ⊃ B(x)) [1].

+  2. А [2].

3. A ⊃ В(х) [1] —из 1, ∀и.

4. В(х) [1, 2] —из3 и 2, ⊃и.

5. ∀x B(x) [1, 2] —из 4, ∀в.

6. A⊃∀x B(x) [1] —из5, ⊃в.

7. ∀x (A ⊃ B(x)) ⊃ (A ⊃∀x B(x)) [ - ] —из 6, ⊃в.

+  1. A ⊃ (В(х) ⊃ A) [1].

+  2. ∃x B(x) [2].

+  3. В(х) [З].

4. В(х) ⊃ A [1]—из 1, ∀и.

5. А [1, 3] — из 3, 4, ⊃в.

6. A [1, 2]— из 5, ∃и.

7. ∃x B(x) ⊃ А [1]—из 6, ⊃в.

8. ∃x (B(x) ⊃ А) ⊃ (∃x B(x) ⊃ А) — из 7, ⊃в.

Сформулированное здесь исчисление, как и приведенная выше аксиоматическая система исчисления предикатов, представляет собой адекватную формализацию понятий ло­гического следования и закона логики. Это значит, что для них справедливы теоремы:

Г ⊨ B е. т. е. Г ⊢ B и ⊨ A е. т. е. ⊢ A.

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

I. Взаимовыразимость кванторов:

1. ∀x A(x) ~ ¬∃x¬A(x). 2. ∃x A(x) ~ ¬∀x¬A(x). 

II. Законы образования контрадикторной противополож­ности:

1. ¬∀x A(x) ~ ∃x¬A(x).  2. ¬∃x A(x) ~ ∀x¬A(x).

 III. Законы пронесения кванторов:

1. ((∀x A(x) & ∀x B(x)) ~ ∀x(A(x) & B(x))).

2. ((∃x A(x) v ∃x B(x)) ~ ∃x (A(x) v B(x))).

3. (∃x (A(x) & B(x)) ⊃ (∃x A(x) & ∃x B(x))).

4. ((∀x A(x) v ∀x B(x)) ⊃ ∀x (A(x) v B(x))).

5. (∀x (A v B(x)) ~ (A v ∀x B(x))), если x не свободна в A.

6. (∃x (A & B(x)) ~ (A & ∃x B(x))), если х не свободна в А.

7. (∀x A(x) ⊃ B(x)) ⊃ (∀x A(x) ⊃ ∀x B(x))).

IV. Перестановка кванторов

1. ∀x ∀y A(x, y) ~ ∀y∀x A(x, y).

2. ∃x ∃y A(x, y) ~ ∃y ∃x A(x, y).

3. ∃x ∀y A(x, y) ⊃ ∀y ∃x A(x, y). 

V. Исключение квантора общности и введение квантора существования.

1. ∀x A(x) ⊃ A(t).      2. A(t) ⊃ ∃x A(x).

В обоих случаях А(t) есть результат правильной подста­новки терма t вместо х в А(х).

VI. Законы устранения вырожденных кванторов. 1. ∀x А ~ А.    2. ∃x А ~ А, где А не содержит х свободно.

VII. Связь кванторов ∀ и ∃.

∀x A(x) ⊃ ∃x A(x).

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

Пример эквивалентных преобразований формулы

∀x (P(x) ⊃ ¬ Q(x)) ⊃ ¬ ∃x (P(x) & Q(x)).

с использованием некоторых из указанных в этом и пред­ыдущем параграфе схем эквивалентностей:

∀x (P(x) ⊃ ¬ Q(x)) ⊃ ¬ ∃x (P(x) & Q(x)) ≡

≡ ¬∀x (P(x) ⊃ ¬ Q(x)) v ¬ ∃x (P(x) & Q(x)) ≡

≡ ∃x ¬(P(x) ⊃ ¬ Q(x)) v ¬ ∃x (P(x) & Q(x)) ≡

≡ ∃x (P(x) & ¬¬ Q(x)) v ¬ ∃x (P(x) & Q(x)) ≡

≡ ∃x (P(x) & Q(x)) v ¬ ∃x (P(x) & Q(x)) ≡

≡ ∃x (P(x) & Q(x)) v ∀x¬ (P(x) & Q(x)) ≡

≡ ∃x (P(x) & Q(x)) v ∀x (¬P(x) & ¬Q(x)).

Разработанный в современной символической логике ме­тод построения логических исчислений является важнейшим ее результатом. Его теоретическая и практическая значи­мость состоит в том, что благодаря ему возникает возмож­ность доказательства любой формулы, представляющей за­кон логики, из бесконечного множества таких формул, а также осуществлять соответствующий вывод для любого слу­чая — опять-таки из бесконечного множества случаев от

ношения логического следования. В основе логических ис­числений, как мы видели, лежат специальные логические языки. Наряду с рассмотренными выше возможностями ис­пользования этих языков для решения многих логических вопросов, и в первую очередь для точного определения ос­новных понятий логики (логическое следование и закон ло­гики), следует заметить, что в этих языках имеются, по су­ществу, точные понятия логической формы и логического содержания мыслей, которые мы используем в дальнейшем.