 |
Натуральная система исчисления предикатов
|
|
|
|
Постулатами системы (исходными правилами) являются все правила натуральной системы исчисления высказываний и правила для кванторов.
Правила вывода для выражений с кванторами:
|
| ||||
∀в:
∀и:
|
|
∃в:
|
|
|
Понятие вывода и доказательства остаются формально теми же, которые были сформулированы в исчислении высказываний, разница лишь в том, что при ссылке на правила вывода теперь имеются в виду и вновь введенные правила для выражений с кванторами. К числу указанных в предыдущем параграфе эвристических принципов введения допущений может быть добавлен еще один.
Если в выводе получена формула ∃ х А(х} и нужно вывести В, не выводимую непосредственно из имеющихся формул, вводим допущение А(х), применяя способ рассуждения согласно ∃и.
Рассмотрим несколько примеров выводов.
Схема доказательства формул вида: ∃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)).
Разработанный в современной символической логике метод построения логических исчислений является важнейшим ее результатом. Его теоретическая и практическая значимость состоит в том, что благодаря ему возникает возможность доказательства любой формулы, представляющей закон логики, из бесконечного множества таких формул, а также осуществлять соответствующий вывод для любого случая — опять-таки из бесконечного множества случаев от
ношения логического следования. В основе логических исчислений, как мы видели, лежат специальные логические языки. Наряду с рассмотренными выше возможностями использования этих языков для решения многих логических вопросов, и в первую очередь для точного определения основных понятий логики (логическое следование и закон логики), следует заметить, что в этих языках имеются, по существу, точные понятия логической формы и логического содержания мыслей, которые мы используем в дальнейшем.
Министерство образования Российской Федерации
Марийский Государственный Технический Университет
Факультет Информатики и Вычислительной Техники
Кафедра ИВС
Реферат
по математической логике и теории алгоритмов на тему:
“Структура исчисления предикатов
построение логического вывода”
Выполнили студенты I-го курса
Факультета ИВТ: Зубарев А., Столяров А.,
Докукин А., Китирисов Г.
Йошкар-Ола, 2003г.
Содержание:
Введение………………………………………………….1
Синтаксис языка логики предикатов …………………..1
Свободные и связные вхождения
переменных в формулы……………………3
|
|
|
Семантика языка логики предикатов…………………..4
Логика предикатов……………………………………...11
Логическое следование…………………………………11
Закон логики предикатов……………………………….12
Исчисление предикатов………………………………....13
Натуральная система исчисления предикатов………...15
Литература……………………………………………….16
Список литературы
1. Е. К. Войшвилло, М. Г. Дегтярев Логика, Москва, 2001.
2. А.А. Марков, Н. М. Нагорный Теория алгорифмов, Москва, 1984.
|
|
|
