∃и :Понятие вывода и доказательства остаются формально теми же, которые были сформулированы в исчислении высказываний, разница лишь в том, что при ссылке на правила вывода теперь имеются в виду и вновь введенные правила для выражений с кванторами. К числу указанных в предыдущем параграфе эвристических принципов введения допущений может быть добавлен еще один.
Если в выводе получена формула ∃х А(х} и нужно вывести В, не выводимую непосредственно из имеющихся формул, вводим допущение А(х), применяя способ рассуждения согласно ∃и.
Рассмотрим несколько примеров выводов.
Схема доказательства формул вида: ¬∃xA(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. ∀xB(x)[1, 2] —из 4, ∀в.
6. A⊃∀xB(x) [1] —из5, ⊃в.
7. ∀x (A⊃ B(x)) ⊃ (A⊃∀xB(x)) [ - ]—из 6, ⊃в.
+ 1. A⊃ (В(х) ⊃ A) [1].
+ 2. ∃xB(x) [2].
+ 3. В(х) [З].
4. В(х) ⊃ A [1]—из 1, ∀и.
5. А [1, 3] — из 3, 4, ⊃в.
6. A [1, 2]— из 5, ∃и.
7. ∃xB(x) ⊃ А [1]—из 6, ⊃в.
8. ∃x (B(x) ⊃ А) ⊃ (∃xB(x) ⊃ А) — из 7, ⊃в.
Сформулированное здесь исчисление, как и приведенная выше аксиоматическая система исчисления предикатов, представляет собой адекватную формализацию понятий логического следования и закона логики. Это значит, что для них справедливы теоремы:
Г ⊨ B е. т. е. Г ⊢ B и ⊨ A е. т. е. ⊢ A.
В заключение параграфа в дополнение к ранее сформулированным эквивалентностям языка логики высказываний приведем схемы наиболее важных законов логики, относящихся к языку логики предикатов, которые читатель может использовать также в качестве упражнений для выводов и доказательств:
I. Взаимовыразимость кванторов:
1. ∀xA(x) ~ ¬∃x¬A(x). 2. ∃xA(x) ~ ¬∀x¬A(x).
II. Законы образования контрадикторной противоположности:
1. ¬∀xA(x) ~ ∃x¬A(x). 2. ¬∃xA(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 (AvB(x)) ~ (Av∀xB(x))), если x не свободна в A.
6. (∃x (A & B(x)) ~ (A & ∃xB(x))), если х не свободна в А.
7. (∀x A(x) ⊃ B(x)) ⊃ (∀x A(x) ⊃ ∀x B(x))).
IV. Перестановка кванторов
1. ∀x∀yA(x, y) ~ ∀y∀xA(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) ⊃ ∃xA(x).
В обоих случаях А(t) есть результат правильной подстановки терма t вместо х в А(х).
VI. Законы устранения вырожденных кванторов. 1. ∀xА ~ А. 2. ∃x А ~ А, где А не содержит х свободно.
VII. Связь кванторов ∀ и ∃.
∀xA(x) ⊃ ∃xA(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.
