Математическая логика и теория алгоритмов. Для изучающих компьютерные науки
6. Пусть в исчислении высказываний примитивными связками являются —i, V и Формулы получены из пропозициональных букв с помощью этих примитивных связок. Каковы бы ни были формулы А, в я с, следующие формулы - суть аксиомы теории Lj: А1: А^(В^А); А2: (А^(В^>С))^((А^В)^(А^>С)); A3: А&В^А; А4: А&В^В; AJ: А^(В^(А&В)); А6: А^(А vB); А7: В^(А vB): А8: (А^)^((В^)^((А vB)^)); А9: (А^В)^((А^ -пВ)^^); А10: -п-пА^А. Правилом вывода теории Lj служит правило modus ponens (MP). Доказать для теорииLj что: 1) формула А^А является теоремой; 2) верна теорема дедукции: если Г - множество формул, А,В - формулы и Г/4 |-В,то:Г 1-А^В: 3)(А^В).(В^) 4) формула B^fA^fA vB)) является теоремой; 5) формула В^((А&В)^А) является теоремой; 6) формула A^ f —i ^ ^A J является теоремой; 7) формула В^(—1—А^А) является теоремой. 7. Пусть формула А теории первого порядка является частным случаем тавтологии. Доказать, что А является теоремой в теории первого порядка. 8. Доказать следующую теорему дедукции для теорий первого порядка: если Г - множество формул. А,В - формулы и \- В и при этом существует такой вывод В из { Г в котором ни при каком применении правила обобщения к формулам, зависящим в этом выводе от А, не связывается квантором никакая свободная переменная формулы ^4. Тогда: Г \-А^В. 9. Пусть А - формула теории первого порядка. Доказать, что в теории первого порядка имеем: |- Vxi Vx2A^ \/х2 VxjA. 10. Выяснить существуют ли контрпримеры к следующим секвенциям: \)(В^В): 2)А^(С^В); 3) (С^А)^(А^С); 4) (А^В)^(В^—А); 5) А^(В^ (А^В)); в) (А^В)^((А^В)^В). 11. Методом исчисления секвенций доказать, что для системы G' следующие формулы являются тавтологиями: \)(—В^—\В); 2)А^(—А^В); 3) ( —iB^—A)^(A^B); 4) ( А^В)^( —iB^ —А); 5) А^(—В^ —i(A^B)); 6) ( А^В)^(( —А^В)^В). 12. Методами натуральной дедукции доказать следующие соотношения: \)А&В \-В&А; 2) \-(А&В)^В; 144
Made with FlippingBook
RkJQdWJsaXNoZXIy MTY0OTYy