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

14. Независимость схем аксиом исчисления высказываний. 15. Разрешимость исчисления высказываний. 16. Другие аксиоматизации исчисления высказываний. 17. Задание теорий первого порядка. 18. Исчисление предикатов первого порядка, его непротиворечивость. 19. Формальная арифметика. 20. Понятие о теоремах Геделя. 21. Значение аксиоматического метода. 22. Задание исчисления высказываний в виде исчисления секвенций. 23. Построение контрпримера для секвенций. 24. Какие преимущества вывода в исчислении секвенций по сравнению с исчислениями гильбертовского типа? 25. Теория естественного вывода. 26. Какие преимущества вывода в исчислении секвенций по сравнению с выводом в теории естественного вывода? Упражнения 1. Является ли выводом в исчислении высказываний следующая последовательность формул: 1) ( - ^^ ( (А^А) ^^А) ) ^ ( ( - ^^ (А^^А) ) ^ ( —A^—AJJ, 2) —A^f{A^—AJ^—AJ, 3) f—A^fA^—AJJ^f —A^—AJ, 4) —A^(A^—AJ, 5) —A^ —A. 2. Доказать, что для любых формул А, В исчисления высказываний следующие формулы являются теоремами исчисления высказываний: \)(—В^—\В); 2)А^(—А^В); 3) ( —iB^—A)^(A^B); 4) ( А^В)^( —iB^ —А); 5) А^(—В^ —i(A^B)); 6) ( А^В)^(( —А^В)^В). 3. Доказать, что в исчислении высказываний имеет место: \)A\-A v B; 2)A\-B v A; Ъ)А,В[А&В; А)А,В[В&А. 4. При доказательстве независимости А1 от А2 и A3 в исчислении высказываний введены выделенные формулы. Составить программу на одном из языков программирования для выяснения выделенности формулы полученной по А2. 5. При доказательстве независимости А2 от А1 и ^45 в исчислении высказываний введены гротескные формулы. Составить программу на одном из языков программирования для выяснения, что формулы (аксиомы), полученные по ^7 либо A3, являются гротескными. 143