Варианты заданий
Применяя правила подстановки и заключения, доказать, что следующие формулы являются теоремами исчисления высказываний (1 – 8).
Применяя правила подстановки и заключения, построить вывод формул из данной системы посылок (9 - 13).
Являются ли выводами в исчислении высказываний следующие последовательности формул (14 – 16).
B
Применяя производные правила вывода, показать, что доказуемы формулы (17 – 34).
U B, P Q ú- (U P) (B Q)
U B, P Q ú- (U P) (B Q)
U B, P Q ú- (B P) (U Q)
ú-
ú-
(P Q) ((Q R) (P R))
(P Q) ((R P) (R Q))
Q ® R (P Ú Q) ®(P Ú R)
(P ® Q) Ú (Q ® P),
P ® (Q® (P Q))
(P ® Q) Ú (P ® Q)
(P ® Q)®((P ® (Q ® R)) ® (P ® R)))
(P ® Q)®((P ® (Q ® R)) ® (P ® R)))
((P® Q) ® ((P ® Q) ® P))
(( Q ® P) ® (( Q ® P) ® Q))
Q ((P Q) (Q P)
Q (P Q) (P Q)
Q (P R Q Q)
Применяя производные правила вывода, построить вывод формул (35 – 41).
,
Применяя производные правила вывода, построить вывод формул. Проверить, справедлива ли выводимость в обратную сторону, если да, то построить вывод (42 – 57).
A (C P) (A C) P
() P
P Q (P)
P R Q ú- ((P ® R) ® ((® R)
(P Q) (P (Q R)) ú- ( P R)
ú-
ú-
2. Исчисления предикатов.
Определим исчисление предикатов гильбертовского типа ИП. Это исчисление является расширением исчисления высказываний ИВ.
В алфавит ИВ добавим строчные латинские буквы для обозначения предметных переменных и символы кванторов и. Язык исчисления составляют формулы, определяемые также, как в алгебре предикатов.
Аксиоматика исчисления дополняется двумя схемами аксиом:
,
где - произвольная формула, содержащая свободные вхождения переменнойx, причем ни одно из них не находится в области действия квантора по переменнойy, аполучена иззаменой свободных вхожденийx наy.
К правилу заключения ИВ добавляются два правила, связанные с кванторами. Пусть и– формулы, которые содержат и не содержат свободные вхождения переменнойxсоответственно.
Правило обобщения (введения )
.
Правило введения
.
Правила естественного вывода дополняются 4-мя правилами. Пусть
Правило введения квантора .
Если T |- U(x), то T |- xU(x).
Правило удаления квантора .
Если T |- xU(x), то T |- U(y).
Правило введения квантора .
Если T |- U(y), то T |- xU(x).
Правило удаления квантора .
Если T, U(x) |- V, то T, xU(x) |- V.
Рассмотрим примеры вывода в ИП.
Задание 1. Доказать, что в ИП
|.
Решение.
1. | |
1 |
2. | |
15 (1) |
3. |- |
8 |
4. |- |
8 |
5. |- |
4 (2, 3) |
6. |- |
4 (2, 4) |
7. |- |
14 (5) |
8. |- |
14 (6) |
9. |- |
Теорема ИП |
10. |- |
4 (7, 9) |
11. |- |
Теорема ИП |
12. |- |
4 (8, 11) |
13. ,|- |
7 |
14. | |
4 (10, 12, 13) |
Задание 2. Доказать, что в ИП
|.
Решение.
1. | |
1 |
2. |- |
16 (1) |
3. |- |
Теорема ИП |
4. |- |
9 |
5. |- |
4 (2, 3, 4) |
6. | |
1 |
7. |- |
16 (6) |
8. |- |
Теорема ИП |
9. |- |
9 |
10. |- |
4 (7, 8, 9) |
11. |- |
10 (5, 10) |
12. | |
17 (11) |
Прикладные исчисления предикатов строятся добавлением к исчислению предикатов своих собственных аксиом. Причем, в прикладных исчислениях предикатов вводится понятие терма. Термами являются:
предметные переменные и константы;
предметные функции.
В аксиомах прикладных исчислений предикатов наряду с предметными переменными могут использоваться произвольные термы.
Всюду далее будут рассматриваться прикладные исчисления предикатов первого порядка, т. е. исчисления, в которых кванторами связываются только предметные переменные, а не предикаты и функции.
Исчисление с равенством.
В данном исчислении вводится предикат =, а к аксиомам ИП добавляются аксиомы равенства.
E1.
E2.
Здесь Е1 является аксиомой, а Е2 – схемой аксиомы, где – произвольная формула, а– формула, полученная иззаменой некоторых вхожденийx на y.
Теорема. В любой теории с равенством:
|- для любого термаt;
|-;
|-.
Формальная арифметика.
Формальная арифметика определяется как исчисление с равенством на предметном множестве , в котором вводятся предметная константа 0 и предметные функции + , , , задаваемые аксиомами.
A1.
A2.
A3.
A4.
A5.
A6.
A7.
A8.
Здесь А1-А7 – аксиомы, а А8 – схема аксиомы, определяющая доказательство по индукции.
Задание 3. Доказать, что в формальной арифметике
|.
Решение. Рассмотрим вначале идею доказательства, а затем оформим её в виде формального вывода. Доказательство проведём от противного, предположим, что , тогда у него существует предыдущий элементt, такой что . Так как, то , что противоречит аксиоме А2, следовательно,. Тогда по условию , а в силу А4 , а, значит, .
1. | |
6 (А3) |
2. ,|- |
6 (Е2) |
3. ,, |- |
2 (2) |
4. , |- |
3 (1, 3) |
5. |
А5 |
6. , |- |
Свойство 3) предиката = |
7. |- |
А2 |
8. , |- |
2 (7) |
9. |- |
11 (6, 8) |
10. |- |
12 |
11. |- |
4 (9, 10) |
12. , |- |
6 (Е2) |
13. |
А4 |
14. , |- |
Свойство 3) предиката |
15. |- |
3 (11, 14) |
16. ,|- |
7 |
17. |- |
4 (11, 15, 16) |
Задание 4. Распространить формальную арифметику на множество целых чисел .
Решение. Для того чтобы распространить формальную арифметику на множество , нужно определить константу 0 и предметные функции на множестве , используя определённые на множестве ô функции и константу.
Так как оба множества ô и Ù счётны, то между ними можно установить взаимнооднозначное соответствие, т. е ô Ù . Тогда определим 0 множества Ù как образ нулевого элемента ô 0 =. Для того чтобы определить функцию следования для целого элементаz, возьмём прообраз этого элемента из ô, вычислим для него следующий элемент, а затем отобразим его в Ù, т. е. . Аналогично определяются функции + и :
,
.