О том, как строить дерево доказательства.

• Если выводимая секвенция имеет вид 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.

При построении доказательств (чтобы не пойти по пути, который ни к чему не приведёт) надо постоянно иметь в виду можно ли вообще вывести те секвенции, к которым мы переходим, т.е. надо проверять тождественную истинность секвенций.