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

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

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

при условии, что никакое допущение из Г не содержит x свободно;

A[Г] ∀x A[Г]

∀в:

 

∀и:

	Результат правильной подстановки терма t вместо x в A(x);

∀x A(x) [Г] A(t) [Г]

 

∃в:

A(t) [Г] ∃x A(x) [Г]

	Здесь ∃x A(x) – имеющееся в выводе допущение, а В и никакое допущение из Г не содержат x свободно.

 

B[Г, A(x)] B[Г, ∃x A(x)]

∃и:

 

 

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

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

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

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

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

+ 2. A(x) [2].

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

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

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

6. ∃x A(x) ⊃∀xA(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) ~ ∃xA(x). 2. ∃x A(x) ~ ∀xA(x).  

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

1. ∀x A(x) ~ ∃xA(x). 2. ∃x A(x) ~ ∀xA(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)).

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

Список литературы

1. Е. К. Войшвилло, М. Г. Дегтярев Логика, Москва, 2001.

2. А.А. Марков, Н. М. Нагорный Теория алгорифмов, Москва, 1984.