Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

' 9 А Т.е. —1^ - А, а затем правило введения импликации дает |— \—А^А, что и требовалось. Заметим, что при формальном аксиоматическом подходе (в теории L) доказательство того, что |— >—А^А было получено, не столь просто. Докажем, что из А,В доказывается А&В. Это сразу следует по правилу введения конъюнкции. Чтобы доказать, что из А,В,С доказывается (A&BJ&C придется дважды применить правило введения конъюнкции. Это доказательство строится в виде дерева (как и исчислении секвенций): & А&В С ^ (A&BJ&C Дерево вывода можно строить как сверху вниз, так и снизу вверх, записывая заключение снизу (как здесь) либо наоборот. Пусть требуется доказать: А&В, В&А^ С \- С. Имеем следующее дерево вывода: А&В ^ А&В ^ & & ^ ^ В & А ^ С В&А С Рассмотрим еще один пример на доказательство в естественном выводе, в котором дерево вывода построим так, чтобы заключение было наверху. Докажем, что имеет место |- (А v(B&C))^(A vB)&(A vC). (4.28) Вид самой формулы для нас является подсказкой, как получить ее вывод (если он существует). Нам известно, что ^ вводится с помощью правила введения импликации. Следовательно, прежде чем получить (4.28), нужно доказать, что (Av(B&C)) [ (AvB)&(AvC.) (4.29) Выражение (4.29) получим по правилу исключения дизъюнкции, если будет доказано следующие два утверждения: А \-(AvB)&(AvC) (4.30) В&с\- (AvB)&(AvC). (4.31)) Высказывание (4.30) будет доказано правилом введения конъюнкции, если будет доказано, что А \-{AwB)^A \-{AvC), (4.32) а (4.31) получим правилом введения конъюнкции из В&С \- (А vB) и В&С [ (А vC) (4.33) Ясно, что оба предложения в (4.32) доказуемы по правилу введения дизъюнкции. Предложения (4.33) можно получить введением дизъюнкции из предложений (В&С) |- S и (В&С) |- С, а последнее - по правилу исключения конъюнкции. 139