05 Исчисление высказываний.
Ошибка.
Попробуйте повторить позже
Построить вывод из аксиом ИВ следующей формулы: .
1. -
;
2. -
;
3.
MP 1, 2.
Ошибка.
Попробуйте повторить позже
Доказать обращение теоремы дедукции. А именно:
Пусть для каких-то формул
и
. Тогда, если расширить множество гамма формулой
фи, то есть рассмотреть
, то
.
Докажем, что если из можно было вывести
, то из
и добавленной к ней
можно будет
вывести
.
По условию нам дано, что .
Давайте фиксируем этот вывод.
1.
2.
...
n. .
Где на каждом шаге каждая - это либо аксиома, либо гипотеза из
, либо
получена из
предыдущих формул по правилу
.
Но теперь мы должны выести из множества гипотез
. Значит, мы можем теперь
пользоваться нашей
как гипотезой.
Давайте допишем её следующим шагом как гипотезу к нашему выводу:
1.
2.
...
n. ;
n+1. .
Далее, мы можем применить к формулам с шагов n и n+1 Modus Ponens:
1.
2.
...
n. ;
n+1. ;
n+2.
MP.
То что у нас получилось - это вывод , но уже из множества гипотез
.
Ошибка.
Попробуйте повторить позже
Доказать правило силлогизма:
Давайте вначале построим вывод
1. - гипотеза;
2. - гипотеза;
3. - гипотеза;
4.
MP
3, 1.
5.
MP
4, 2.
И мы получили вывод формулы из множества гипотез
Но тогда по теореме о дедукции отсюда следует, что можно вывести .
Ошибка.
Попробуйте повторить позже
Пусть - любая формула. Доказать, что
(То есть если в гипотезах у нас есть какая-то формула вместе со своим отрицанием, то из такого множества гипотез можно вывести абсолютно любую формулу).
1. - гипотеза;
2. -
;
3. - гипотеза;
4. -
;
5.
MP
1, 2.
6.
MP
3, 4.
7. -
;
8.
MP
5, 7.
9.
MP
6, 8.
10. -
;
11.
MP
9, 10.
Ошибка.
Попробуйте повторить позже
Показать, что система аксиом ИВ в гильбертовской форме избыточна. А именно, показать, что аксиома
следует уже из остальных аксиом.
Выведем сначала
1. - гипотеза;
2. -
;
3. - гипотеза;
4. -
;
5.
MP
1, 2.
6.
MP
3, 4.
7. -
;
8.
MP
5, 7.
9.
MP
6, 8.
10. -
;
11.
MP
9, 10.
Таким образом, мы вывели
Но тогда по теореме о дедукции
И ещё раз по теореме о дедукции
То есть эта последняя формула выводится из пустого множества гипотез - чисто из
аксиом ИВ.