3.1. Построение вывода в логике высказываний

Пример. Докажем, что выводима формула . Сокращенно это записывается так: ├.

По теореме, обратной теореме дедукции, посылку можно перенести в левую часть:

├.

Проделаем эту операцию еще раз:

, ├.

Таким образом, нам нужно доказать, что из формул и выводима формула . Составим вывод формулы . В каждой строке вывода записывается только одна формула. В правой части страницы удобно указывать комментарий, – что собой эта формула представляет. Возможны варианты:

· гипотеза,

· аксиома (может быть, с какими-то подстановками),

· ранее доказанная теорема,

· формула получена из предыдущих формул по правилу Modus ponens.

Вначале мы запишем гипотезы.

1. – гипотеза.

2. – гипотеза.

Формулу удобно получить из аксиомы А3. Поэтому запишем эту аксиому:

3. А3.

К формулам 1 и 3 можно применить правило вывода Modus ponens (что мы и отметим в комментарии). Порядок номеров формул существенен (первой указывается посылка).

4. . МР 1, 3.

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

5. . А1 с подстановкой вместо – .

Далее дважды применяем правило Modus ponens:

6. . МР 2, 5.

7. . МР 6, 4.

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

Отметим, что вывод может быть неединственным, в частности, формулы могут быть записаны в другом порядке. Решение данной задачи может быть оформлено следующим образом:

├.

По теореме, обратной теореме дедукции,

├.

, ├.

1. – гипотеза.

2. – гипотеза.

3. . А1, : .

4. . МР 2, 3.

5. . А3.

6. . МР 1, 5.

7. . МР 4, 6.

Пример. Данный пример более прост, но достаточно показателен. Обратите внимание, что здесь не используются ни аксиомы, ни теоремы. Доказательство теоремы ├ строится только на основании правила МР.

По теореме, обратной теореме дедукции,

├.

, ├.

, , ├.

1. – гипотеза.

2. – гипотеза.

3. – гипотеза.

4. . MP 3,2.

5. . MP 4,1.

< Предыдущая		Следующая >