Математическая логика и теория алгоритмов

т.е. Т\А\-А,а затем правило введения импликации дает что и требовалось. Заметим, что при формальном аксиоматическом под­ ходе (в теории L) доказательство того, что [-11 А=:>А было получено, не столь просто. Рассмотрим еще один пример на доказательство в естественном выводе. Докажем, что имеет место (-(Av(B&C))=>(AvB)&(AvC). (4.27) Вид самой формулы для нас является подсказкой, как получить ее вы­ вод (если он существует). Нам известно, что вводится с помощью правила введения импликации. Следовательно, прежде чем получить (4.27), нужно доказать, что i A - v { B 8 c C ) ) l-(^v5)&(^vC). (4.28) Выражение (4.28) получим по правилу исключения дизъюнкции, если будет доказано А (- (AvB)&{AsyC) (4.29) и В&С 1" (AvB)&(AvQ (4.30) Высказывание (4.29) будет доказано правилом введения конъ­ юнкции, если будет доказано, что А }-(A V B) H A \-(A V C), (4.31) а (4.30) получим правилом введения конъюнкции из B&C\-(AvB) и В8сС\-(А\/С). (4.32) Ясно, что оба предложения в (4.31) доказуемы по правилу вве­ дения дизъюнкции. Предложения (4.32) можно получить введением дизъюнкции из предложений (В&С) j- В и (В&С) |- С, а последнее - по правилу исключения конъюнкции. 181