Введение

Об аксиоматическом методе. Современные представления. Исчисления. Теоремы и вывод. Теория и метатеория. Цели формализации в математике. Логика высказываний и ее формализация — теория K.

В основе современной математики лежит аксиоматический метод. Суть его в том, что математическая теория строится путем вывода всех утверждений (теорем) из относительно небольшого числа утверждений, которые заранее считаются истинными (это аксиомы).

Именно в таком ключе аксиоматический метод был введен в математику в Древней Греции. В современной математике аксиоматический метод получил дальнейшее развитие. Детальному анализу подверглись не только сами выводы конкретных математических теорий, но и способы доказательств. Однако, чтобы проанализировать приемы математических рассуждений и их обоснованность формализации нужно подвергнуть не только предметную область, т.е. содержательные понятия конкретной математической теории, но и приемы логических умозаключений.

В свете этого полностью формализованная математическая теория выглядит так. Имеется некоторый язык, позволяющий составлять правильные слова-формулы, которые отражают возможные утверждения теории. Есть некоторый набор формул, изначально объявленных истинными (это аксиомы). Кроме того, задан некоторый набор правил преобразования формул, кото- рые позволяют из истинных формул получать новые истинные формулы. Все истинные утвер- ждения теории получаются путем формальных преобразований формул в рамках узаконенных правил преобразований. Цепочка последовательных преобразований называется выводом.

В полностью формализованной теории утрачивается содержательный смысл формул, а все построение теории превращается в манипуляции заданными символами. В силу этого такие теории называют исчислениями.

Построение исчислений не является высшей целью развития математики. На это указывает положение дел в таких классических областях математики, как дифференциальное и интеграль- ное исчисления, геометрия. Эти разделы, несмотря на их многолетнюю историю, по-прежнему излагаются на содержательном, а не формальном, уровне. Дело в том, что формализация — это определенный метод математического исследования, который используется при исследовании теорий на непротиворечивость, наличие зависимых понятий и т.п.

Отметим, что при изложении формальной теории приходится выходить за ее рамки, чтобы проводить содержательный анализ ее результатов. Поэтому вокруг формальной теории возникает другая теория: ”учение о формальной теории“, которую называют метатеорией. Метатеория формирует свой язык, расширяющий язык формальной теории, который называется метаязыком. На это было обращено внимание при изложении логики высказываний.

Логика высказываний не является формальной теорией, хотя и имеет собственный язык. Все суждения в логике высказываний оказываются за пределами ее языка и устанавливаются на базе истинностных функций, которые никак не отражаются в языке логики высказываний.

Реально все необходимые выводы логики высказываний можно было бы сделать, не прибе- гая к ее полной формализации. Но тогда теряется связь получения тех или иных утверждений с реальный процессом умозаключений, который и представляет собой подлинное математическое доказательство. Кроме того, логика высказываний в основном сводится к теории булевых функций, т.е. к исследованию конечных объектов. Поэтому формальная теория логики высказываний — одна из самых простых и в этом смысле удобна как иллюстрация современного подхода к формализации в математике.

Любая теория имеет множество вариантов формализации. В рамках логики высказываний мы остановимся на одном из этих вариантов, который назовем теорией K.