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

Аксиоматизация теории позволяет: 1) систематизировать научный материал, 2) обеспечить определенную организацию научного знания, 3) исследовать структуру различных теорий и их взаимоотношение, 4) обеспечить необходимую строгость рассуждений. Формализация теории, опирающаяся на аксиоматический метод, имеет существенное значение для объяснения и уточнения понятий теории и выявления используемых в ней методов доказательств. С первого взгляда может показаться, что научная терминология, во многих случаях значительно отличающаяся от обычного словоупотребления, является менее ясной и более искусственной, чем повседневная речь. Однако именно благодаря известной искусственности достигается большая точность и определенность понятий, их ясность. В ряде случаев нельзя правильно поставить вопрос, ни тем более ответить на него, пока не уточним соответствующее понятие. Как и уточнение понятий, уточнение логических средств вывода, достигаемое посредством формализации, имеет, как видим, решающее значение для того, чтобы сделать доказательство необходимо строгим и свободным от ссылок на очевидность и интуицию. С проблемой формализации неразрывно связано создание различных научных или формализованных языков. Основная цель, которая при этом преследуется, состоит в том, чтобы построить язык, свободный от недостатков обычного языка. Благодаря точности и однозначности формализованные языки находят применение там, где предъявляются повышенные требования к строгости. Д. Гильберт писал: ''Под знаком аксиоматического метода математика проявляет свою руководящую роль е науке еообще^\ § 17. Исчисление секвенций и поиск контрпримера Рассмотренный в §§ 5-16 данной главы, формальный аксиоматический метод считается, как уже указано, исчислением гильбертовского типа. Новый метод - исчисление секвенций является более удобным подходом для построения доказательств, чем исчисления гильбертовского типа. Исчисление секвенций называют еще исчислениями генценовского типа по имени Генцена, который начал их изучать. Прежде чем строить исчисление секвенций рассмотрим следующую задачу, которую считаем задачей поиска контрпримера. Пусть дана некоторая формула W логики высказываний, которая возможно не является тавтологией, следовательно, может быть существуют значения переменных (означивание переменных), при которых она ложна. Как это выяснить? Естественно посмотреть на структуру формулы W. Например, если W имеет вид Л^В, то надо найти значения переменных, при которых формула А 130