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

2) G \-A^B - no теореме дедукции; 3) —A) - теорема согласно п. д) леммы 4.2; 4) (А^В) \- (—В^ -А) - из 3) по MP; 5) G I В^ —А - из 2) и 4) по третьему свойству выводимости (см. параграф 6 данной главы); 6) G, — L 8 - —iS - по определению вывода; 7)G, -^В \-^В^^-ш5); 8) —\В^^ —А, —В I—А - по MP; 9) G, —1S I—А - из 7) и 8) по третьему свойству выводимости. Что и требовалось доказать. 2. Правило удаления &: A8iB\-A. Доказательство. \) А, В \- ^ - по определению вывода; 2) А, —А I— \В - из 1) по правилу перевертывания; 3) -А \-А^ —iS - по теореме дедукции; 4) —:(А^ —iB) I — >—А - из 3) - по правилу перевертывания; 5) -п—А =^А - теорема согласно п. а) леммы 4.2; 6) —i-nA - из 5) по MP; 7) -п(А^ —\В) [• - из 4) и 6) по свойству (3 ) выводимости. Получили |- А. Что и требовалось. 3. Правило введения & : А,В \- А&В. Доказательство. \ ) А , А ^ ^ \ - 7в-поМР; 2) А, — 1— L 8 I—\(А^ —В) - из 1) по правилу перевертывания; 1)) А, В \- ^ - по определению вывода; 4) В^ —1— L 8 - теорема согласно п.б) леммы 4.2; 5) 5 I— L 8 - из 4) по MP; в) А, В - —1— L 8 - из 5); 7) А, В —\(А^ —В) - из 6) и 2) по третьему свойству выводимости. В результате получили А, В \- ASlB, ЧТО И требовалось. Аналогично доказывается, что А,в\- BSlA. Также можно доказать следующие правила. 4. Правила введения v. А \-AvB, B\-AvB. 5. Правило доказательства разбором случаев: Если А\-С И 5|- С, ТО^ vB \- С. 6. Правило сведения к нелепости (доказательство от противного): Если^ | -5 и А\ — \В,то I —А. 114