Упражнения
1. Применяя правило подстановки, показать, что доказуемы формулы:
2. Применяя правило подстановки и правило заключения, установить доказуемость формул:
1)
;
2)
;
3)
4)
5)
3. Применяя
производные правила вывода, показать,
что доказуема формула
4. Доказать производные правила вывода:
1)
;
2)
;
3)
;
4)
Примечание. Отметим некоторые общие соображения для получения доказуемых формул. Если задана “короткая” формула, для которой надо установить её доказуемость, то нужно мысленно представить, на какую из аксиом она похожа по форме. Затем надо представить, какие переменные и на какие формулы надо в ней заменить, чтобы получить заданную доказуемую формулу.
Если задана “длинная” формула, то нужно мысленно “охватить” одну, а лучше две её последние скобки, и представить, на какую из аксиом эти скобки “похожи” по форме. Затем надо представить, какие переменные в этой части формулы и на какие другие формулы надо заменить, чтобы получить заданную часть формулы. Замена в оставшейся начальной части заданной формулы уже будет практически очевидна.
Примерно по такому же сценарию устанавливается доказуемость формулы путем применения правил подстановки и замены. Сначала надо представить, на последнюю часть какой из “длинных” аксиом “похожа” по форме заданная формула, и подобрать соответствующую замену переменным. Далее смотрят, нельзя ли к полученной промежуточной доказуемой формуле применить ПЗ или ПСЗ, чтобы получить заданную формулу. Если этого сделать нельзя, то смотрят на оставшиеся части промежуточной доказуемой формулы и определяют, на какие из “коротких” аксиом они “похожи”, и устанавливают тем самым их доказуемость.
Затем, применяя ПСЗ, устанавливают доказуемость исходной формулы.
Иногда после первого и даже второго применения правила подстановки бывает необходимо применить правило контрпозиции или снятия двойного отрицания, а уж затем применять ПЗ или ПСЗ.
2.5. Определение формулы, выводимой из совокупности формул н
В исчислении высказываний некоторые формулы могут быть получены не только из совокупности аксиом, но и из совокупности формул Н, не являющихся аксиомами. Такие формулы называют выводимыми из совокупности формул Н. Дадим определение таким формулам.
Пусть у нас имеется
некоторая совокупность формул
Тогда:
всякая формула
является формулой, выводимой из Н;всякая доказуемая формула выводима из Н;
если формулы С и
выводимы
из совокупности Н,
то формула В
также выводима из Н
(правило заключения для выводимых
формул).
То, что некоторая
формула В
выводима из совокупности Н,
записывают так:
.
Число формул совокупности Н может быть самым различным. Если Н=0, то предполагается, что совокупность (множество) Н не содержит никаких других формул, кроме аксиом исчисления высказываний. Если указано, что совокупность Н состоит из некоторых формул, например A,B,C, то предполагается (по умолчанию), что в эту совокупность входят и аксиомы. Причем формулы A, B и C не обязательно должны быть доказуемыми.
Исходя из этого, можно отметить, что класс формул, выводимых из совокупности Н, совпадает с классом доказуемых формул в случае, когда совокупность Н содержит только доказуемые формулы, и в случае, когда совокупность Н пуста.
Если же совокупность формул Н содержит хотя бы одну недоказуемую формулу, то класс формул, выводимых из совокупности Н, шире класса доказуемых формул.
Рассмотрим пример.
Доказать, что из совокупности формул
выводима формула
.
Доказательство.
Так как
и
,
то по определению выводимой формулы
(1)
(2)
Возьмем аксиомы
и I
и выполним
подстановки
и
В результате получим доказуемые формулы,
которые выводимы из Н
по определению, т.е.
(3)
(4)
Так как формула
доказуема (см. подразд. 2.3), то она выводима
из Н:
(5)
Из формул (5) и (3) согласно ПЗ получаем
(6)
Из формул (2) и (4) согласно ПЗ получаем
(7)
Из формул (7) и (6) согласно ПЗ получаем
(8)
И, наконец, из формул (1) и (8) по тому же ПЗ получаем
(9)
Если мы запишем последовательность всех выводимых формул с номерами (1)…(9), то получим
Такая последовательность называется выводом формулы из совокупности формул Н.
Теперь распространим понятие вывода на общий случай.