Кузнецов О.П., Адельсон-Вельский Г.М. - Дискретная математика для инженеров (1048837), страница 45
Текст из файла (страница 45)
ключением. Примеры аксиом и правил вывода будут приведены несколько позднее, Выводом формулы В из формул Аь ..., А называется последовательность формул Р„... Р, такая, что Р =В, а любая Р~(1=1, ..., лт) есть либо аксиома, либо одна из исходных формул А,, ..., А„либо непосредственно выводима из формул Р„..., Р; 1 (или какого-то их подмножества) по одному из правил вывода. Если существует вывод В из Аь ..., А„то говорят, что В выводима из Аь ..., А,. Этот факт обозначается так: Аь ..., А,';В. Формулы А„..., А, называются гипотезами или посылками вывода.
Переход в выводе от Р; ~ к Р; называется 1-м шагом вывода. 21В Доказательством формулы В в теории Т называется вывод В из пустого множества формул, т. е. вывод, в котором в качестве исходных формул используются только аксиомы. Формула В, для которой существует доказательство, называется формулой, доказуемой в теории Т, или теоремой теории Т; факт доказуемости В обозначается(-В. Очевидно, что присоединение формул к гипотезам не нарушает выводимости. Поэтому если ~ — В, то А~ — В, и если А» ..., А«)- В, то А„..., А„, А„+1( — В для любых А и А,+ь Порядок гипотез в списке несуществен. При изучении формальных теорий мы имеем дело с двумя типами высказываний: во-первых, с высказываниями самой теории (теоремами), которые рассматриваются как чисто формальные объекты, определенные ранее, а во-вторых, с высказываниями о теории (о свойствах ее теорем, доказательств и т.д.), которые формулируются на языке, внешнем по отношению к теории, — метаязыке и называ.
ются метатеоремами. Различие между теоремами и метатеоремами не всегда будет проводиться явно, но его обязательно надо иметь в виду, Например, если удалось построить вывод В из Аь ..., А„то высказывание «А„..., А„) — В» является метатеоремой; ее можно рассматривать как дополнительное («произвольное») правило вывода, которое можно присоединить к ис. ходным и использовать в дальнейшем. Ясно, что общезначимые (тождественно-истинные) высказывания типа А~/А или ухР(х)-ь-Р(у), имеющие силу общих логических законов, должны содержаться в любой теории, претендующей на логический смысл.
Поэтому изучение конкретных формальных теорий начнем с исчислений, порождающих все общезначимые формулы. Исчисление высказываний. Аксиомы и правила вывода. В исчислении высказываний мы вновь встречаемся с объектами, с которыми однажды уже имели дело, — с формулами алгебры логики. Однако здесь формулы рассматриваются не как способ представления функций, а как составные высказывания, образованные из элементарных высказываний (переменных) с помощью логических операций или, как говорят в логике, связок ~/, Ь, 1, -». При этом особое внимание уделяется тождественно-истинным высказываниям, поскольку, как уже отмечалось, они должны входить в любую теорию в качестве общелогических законов.
Их порождение и является основной задачей исчисления высказы- ваний. Исчисление высназываний определяется следующим образом. 1. А л ф а в и т исчисления высказываний состоит из переменных высказываний (пропозициональных букв): А, В, С..., знаков логических связок ~/, й, ~, — ~ и скобок (,). 2. Фор мулы: а) переменное высказывание есть формула; б) если ц и И вЂ” формулы, то (И ~/ Ч3), Фа З), (Ж— аз) и ~а — формулы; в) других формул нет.
Внешние скобки у формул обычно договариваются опускать; например, вместо (н ~/ аз) пишут н ~/'о. Вместо синтаксически более удобного знака ) часто употребляется черта пад формулой (она использовалась в гл. 3). 3. А к с но м ы. Приведем здесь две системы аксиом. Первая из них непосредственно использует все логические связки: Система аксиом ! П.
А-э.(В-~А); 12, (А-~В)-~((А-~(В-~-С))-~-(А- С)); 13. (А Ь В)- А; 14. (А Ь В) †«-В; 15. Л- (В-~(А Ь В)); 16, Л-э(А ~/ В); 17. В-+.(А ~,' В); 18, (А-~С)-з-(( — )-С) — э.((Л ~,' В)-~-С)); 19. (А- В)-~((А-~ ~В)-+- ! А); ПО. ) ) А-+-А. Другая система использует тольно две связки ) и -~; при этом сокращается алфавит исчисления (выбрасываются знаки '/, Ь) и соответственно определение формулы. Операции ~/, Ь рассматриваются не как связки исчисления высказываний, а как сокращения (употреблять которые удобно, но не обязательно) для некоторых его формул: А~/В заменяет )А — «В, АЬВ заменяет ) (А — ~- ) В).
В результате система аксиом становится намного компактнее. Система аксиом П .!11. А-+.(В-+А); П2. (А-э(В-эС)) — ~((А-эВ)- (А-~С)); 220 ПЗ. ( ) А-~- ~В)-~-(( ~А-+В)-~А). Приведенные системы аксиом равносильны в том смысле, что порождают одно и то же множество формул. Разу» меется, такое утверждение нуждается в доказательстве, которое заключается в том, что показывается выводимость всех аксиом системы П из аксиом системы ! и, наоборот, системы 1 из системы П ( с учетом замечаний относительно ~/ и 6).
Доказательство этих выводимостей.предоставляется читателю после того, как он познакомится с примерами вывода в исчислении высказываний (см. также при. мер 6.2, а). Возможны и другие системы аксиом, равносильные пер. вым двум системам. Какая из систем лучше? Это зависит от точки зрения. Система П компактнее и обозримее; соответственно более компактны н доказательства различных ее свойств. С другой стороны, в более богатой системе 1 короче выводы различных формул. 4. Пр а вил а вывода: 1) правило подстановки. Если Ж вЂ” выводимая формула, содержащая букву А (обозначим этот факт а (А) ), то выводима формула З (З), получающаяся из а заменой всех вхождений А на произвольную формулу З(— и (А) и (З, 2) правило заключения (Мо()пз Ропепз).
Если и и Ж-» -+З вЂ” выводимые формулы, то З выводима: и, и.+З З В этом описании исчисления высказываний аксиомы яв. ляются формулами исчисления (соответствующими определению формулы); формулы же, использованные в правилах вывода (а, а - З и т.д.), это «метаформулы», илн схемы формул. Схема формул, например и- з, обозначает множество всех тех формул исчисления, которые получаются, если ее метапеременные заменить формулами исчисления: скажем, если и заменить на А, а з — на А "хВ, то из схемы формул З -+ З получим формулу А-+АЬВ, Использование схем формул можно распространить и на аксиомы.
Например, если в системе П переменные (пропознциональные буквы) А, В, С заменить метапеременными 22( Н, зв, 6, то получаются трн схемы аксиом, задающие три бесконечных множества аксиом. В результате возникает другой способ построения исчисления высказываний: с бесконечным множеством аксиом (задаваемым конечным числом схем аксиом), нобез правила подстановки, поскольку опо неявно содержится в истолковании схем аксиом.
Первый способ более последовательно конструктивен: все его средства явно зафиксированы и конечны; при' вводе исчисления в ЭВМ (например, при автоматизации доказательства теорем) он выглядит более естественным. С другой стороны, второй способ больше соответствует математической традиции истолкования формул; например, алгебраическое тождество (а+Ь)'=а'+2аЬ+Ь' или тождества булевой алгебры истолковываются именно как схемы тождеств, а не конкретные тождества, верные лишь для конкретных букв.
Правило подстановки при этом подразумевается (см. гл. 3, 5 3.2). Впрочем, достаточно очевидно, что переход от одного способа построения исчислений к другому не представляет труда. Рассмотрим теперь примеры вывода в исчислении высказываний. Пример 3.1. а. Покажем, что формула Л вЂ” ~-А выводима из системы аксиом 11. ~-А-~-А.
1. (А-~-( (А — зА) — 1- 4) )-~ ( (А-э (А-~А) ) — э-(А-зА) ) (подстановка в аксиому П2 А-~-А вместо В и А вместо С). 2. А-~((А-+А)-+А (подстановка в 1П А-~А вместо В). 3. (А (А-~-А))-+(А-~А) (из шагов 2, 1 по правилу заключеная). 4. А-~-(А-~-А) (подстановка в П1 А вместо В). б. А-~-А (из шагов 4, 3 по правилу заключения). б. А) — В-+.Л. Пусть А выводима. Тогда из Л и аксиомы П 1 по пра- А, А-~.(В-~-А) нилу заключения получаем что и доказы-  — «А вает искомую выводимость. Как уже отмечалось ранее, всякую доказанную в исчислении выводимость вида Г)- И, где à — список формул, Ж вЂ форму, можно рассматривать как правило вывода à —, которое можно присоединить к уже имеющимся.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
