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

секвенций к «нормальной форме», не содержащей применений правила сечения и тем самым представляющей в некотором смысле «прямой» вывод. Из многочисленных приложений этого результата особенно важны доказательства непуотиеоуечиеости арифметических формальных систем, использующие математическую технику, выходящую за рамки гильбертовского финитизма, и тем самым обходящие в известном смысле трудности, обусловленные теоремой К. Гёделя о неполноте формальной арифметики. Эта же основная теорема Генцена лежит в основе большинства алгоритмов выводимости для логических и логико-математических исчислений, чем и обусловлена исключительная важность исчисления секвенций для интенсивно развивающихся исследований в области машинного поиска логического вывода, являющихся важным примером моделирования интеллектуальной деятельности человека. 1. Эффективные и полуэффективные методы. 2. Дедуктивные теории, их классификация. 3. Свойства дедуктивных теорий: непротиворечивость, полнота, независимость аксиом, разрешимость. 4. Полуформальные аксиоматические теории. Пример такой теории - геометрия. В чем отличие геометрии Евклида от геометрии Лобачевского- Бойаи-Гаусса? 5. Формальные аксиоматические теории. Их задание, понятие вывода, теоремы, следствия. 6. Какие свойства выводимости знаете? 7. Исчисление высказываний. Задание. Конечно или бесконечно множество аксиом этой теории? 8. Является ли формула теоремой исчисления высказываний? 9. Укажите, какие из следующих формул являются теоремами исчисления высказываний: ж) ( А ^ В ) ^ ( з ) и) (А^В)^((—Л^В)^В); к)(А^В)^—\В. 10. Производные (доказуемые) правила вывода в исчислении высказываний. 11. Эквивалентность двух определений непротиворечивости для теорий, содержащих исчисление высказываний. 12. Непротиворечивость исчисления высказываний. 13. Полнота исчисления высказываний. Вопросы и темы для самопроверки а) —i—iB^B; б) В^^-пВ; г) -пВ^В; е) (—\В^—А)^(А^В); в) —A^>f—А^> —iBJ,' д) -А^(А^В); 142