2. Правило сложного заключения.

Правило сложного заключения также допускает обобщение.

Второе производное правило, получаемое в результате такого обобщения, применяется к формулам вида

и формулируется так :

если формулы и доказуемы, то и формула L доказуема.

Правило сложного заключения схематично записывается так:

├А₁, ├А₂, …,├А_n, ├A₁→(A₂→(A₃→(...(A_n→L) …)))

├ L

Следующие правила знакомы по тождественно истинным формулам алгебры логики, носящим те же наименования.

3. Правило силлогизма.

Если доказуемы формулы А→В и В→С, то доказуема формула А→С , т. е.

├А→В,├В→С

├А→С

4. Правило контр позиции.

Если доказуема формула А→В, то доказуема формула , т. е.

├ А →В

├

На примере этого правила покажем, как доказываются такие утверждения в исчислении высказываний. Сделаем одновременную подстановку , получим доказуемую формулу ├(А→В)→├( ). (1)

Но по условию доказуема формула ├А→В. (2)

Из формул (2) и (1) по правилу заключения имеем ├ .

5. Правило снятия двойного отрицания.

а) Если доказуема формула , то доказуема формула .

б) Если доказуема формула , то доказуема формула .

Схематичная запись : ├ А → и ├ →В

├ ├ .

§4.Понятие выводимости формул из совокупности формул.

Будем рассматривать конечную совокупность формул Н={А₁,А₂,…,А_n}.

Определение формулы, выводимой из совокупности Н.

1)Всякая формула А_i ,является формулой, выводимой из Н.

2) Всякая доказуемая формула выводима из Н.

3) Если формулы С и С→В выводимы из совокупности Н, то формула В также выводима из Н.

Если некоторая формула В выводима из совокупности Н, то это записывают так: Н├В.

Нетрудно видеть, что класс формул, выводимых из совокупности Н, совпадает с классом доказуемых формул в случае, когда совокупность Н содержит только доказуемые формулы, и в случае, когда Н пуста.

Если же совокупность формул Н содержит хотя бы одну не доказуемую формулу, то класс формул, выводимых из Н, шире класса доказуемых формул.

Пример.

Доказать, что из совокупности формул Н={А ,В} выводима формула .

Так как А и В , то по определению выводимой формулы

Н├А, (1)

Н├В. (2)

Возьмемксиомы и , и выполним подстановки и .

В результате получим доказуемые формулы, которые выводимы из Н по определению выводимой формулы, т. е.

Н├(А→А)→((А→В)→(А )), (3)

Н├В→(А→В), (4)

Так как формула А→А доказуема, то Н├А→А. (5)

Из формул (5) и (3) по правилу заключения получаем: Н├(А→В)→(А )). (6)

Из формулы (2) и (4) по правилу заключения получаем: Н├А→В. (7)

Из формул (7) и (6) по правилу заключения получаем: Н├А . (8)

И, наконец, из формул (1) и (8) получаем:

Н├ (9)

Ясно, что при доказательстве выводимости формулы из совокупности формул можно пользоваться не только основным правилом заключения, но и правилом сложного заключения. Тогда, пользуясь этим правилом , предложение (9) можно получить из предложений (5), (7), (1) и (3).