Упражнения. 1. Применяя правило подстановки, показать, что доказуемы формулы:

1. Применяя правило подстановки, показать, что доказуемы формулы:

2. Применяя правило подстановки и правило заключения, установить доказуемость формул:

1) ; 2) ; 3)

4) 5)

3. Применяя производные правила вывода, показать, что доказуема формула

4. Доказать производные правила вывода:

1) ; 2) ; 3) ; 4)

Примечание. Отметим некоторые общие соображения для получения доказуемых формул. Если задана “короткая” формула, для которой надо установить её доказуемость, то нужно мысленно представить, на какую из аксиом она похожа по форме. Затем надо представить, какие переменные и на какие формулы надо в ней заменить, чтобы получить заданную доказуемую формулу.

Если задана “длинная” формула, то нужно мысленно “охватить” одну, а лучше две её последние скобки, и представить, на какую из аксиом эти скобки “похожи” по форме. Затем надо представить, какие переменные в этой части формулы и на какие другие формулы надо заменить, чтобы получить заданную часть формулы. Замена в оставшейся начальной части заданной формулы уже будет практически очевидна.

Примерно по такому же сценарию устанавливается доказуемость формулы путем применения правил подстановки и замены. Сначала надо представить, на последнюю часть какой из “длинных” аксиом “похожа” по форме заданная формула, и подобрать соответствующую замену переменным. Далее смотрят, нельзя ли к полученной промежуточной доказуемой формуле применить ПЗ или ПСЗ, чтобы получить заданную формулу. Если этого сделать нельзя, то смотрят на оставшиеся части промежуточной доказуемой формулы и определяют, на какие из “коротких” аксиом они “похожи”, и устанавливают тем самым их доказуемость.

Затем, применяя ПСЗ, устанавливают доказуемость исходной формулы.

Иногда после первого и даже второго применения правила подстановки бывает необходимо применить правило контрпозиции или снятия двойного отрицания, а уж затем применять ПЗ или ПСЗ.