- Если выводимая секвенция имеет вид G |– F & G
(и F & G нет в G), то
нужно применить правило введения конъюнкции и отдельно вывести
G |– F и G |– G.
- Если выводимая секвенция имеет вид G |– F Й G
(и F Й G нет в G), то
нужно применить правило введения импликации и вывести
G И {F} |– G.
- Если выводимая секвенция имеет вид G |– F Ъ G
(и F Ъ G нет в G), то правило введения дизъюнкции
нужно применять только если можно вывести либо G |– F,
либо G |– G.
- Если формула вида F & G входит в множество G посылок
выводимой секвенции (а в правой части F и G употребляются без конъюнкции),
то, можно попытаться дойти до секвенций, в которой в правой части в
"чистом виде" F или G и, применив правило удаления конъюнкции,
получить аксиому.
- Если формула вида F Й G входит в множество G посылок
выводимой секвенции (а в правой части G употребляются без импликации),
то, можно попытаться дойти до секвенций, в которой в правой части в
"чистом виде" G и, применив правило удаления импликации,
перейти к доказательству секвенции с правой частью F.
- Если формула вида F Ъ G входит в множество G посылок
выводимой секвенции (а в правой части F и G употребляются без дизъюнкции),
то, можно применив правило удаления дизъюнкции, перейти к доказательству
двух секвенций, в одной из которых вместо F Ъ G – F, а в другой G.
- Если вышеперечисленные приёмы не приводят к доказательству, надо
попытаться "доказать от противного", т.е. применить правило удаления отрицания
(или введения отрицания) и, потом, – правило сведения к противоречию.
Применяя правило сведения к противоречию важно правильно подобрать
формулу F.
Как видим, правила введения при доказательстве "от корней к аксиомам"
позволяют "разбирать" формулы в правой части секвенций, а правила удаления
– в левой.
При построении доказательств (чтобы не пойти по пути, который ни к чему не
приведёт) надо постоянно иметь в виду можно ли вообще вывести те секвенции,
к которым мы переходим, т.е. надо проверять тождественную истинность секвенций.
Назад
|