Формализация (Кузнецов, 2007)

ФОРМАЛИЗАЦИЯ - метод выявления и уточнения научного знания путем придания ему строго фиксированной формы. Одним из таких методов является аксиоматизация, т.е. построение аксиоматической теории. В этом случае исходному знанию, которое первоначально является интуитивным, носит содержательный характер и описывается на естественном языке, придается определенная структура — выделяются наиболее общие утверждения, которым придается статус аксиом, все остальные положения теории выводятся чисто логически из этих аксиом в качестве теорем; все термины, кроме исходных, входящих в аксиомы, вводятся по определению и их можно использовать только в смысле данных определений. Впервые метод Ф. был применен Аристотелем при построении первой логической теории — силлогистики. Несколько позже этот метод Аристотеля был использован Евклидом при построении классической геометрии.

Строго говоря, употребление естественного языка при Ф. является нежелательным. Именно по этой причине аксиоматика Евклида оказалась не полной. Ему не удалось в качестве аксиом задать все свойства геометрических объектов, которые реально использовались при доказательстве теорем. Ряд положений он применял интуитивно, неявным образом опираясь на термины, смысл которых не был формализован. Более совершенным методом Ф. является метод построения формальных теорий — исчислений. С этой целью предварительно осуществляется Ф. естественного языка, т.е. создается специальный язык символов. В этом языке задаются правила порождения осмысленных последовательностей символов (например, формул), которые становятся содержательными утверждениями благодаря их интерпрета-ции. Отдельные утверждения объявляются аксиомами. Вводятся правила преобразования одних последовательностей в другие, которые выступают в качестве логических правил дедукции. При этом сама дедукция превращается в формальный вывод, т.е. в такую последовательность шагов, осуществление которых не требует обращения к смыслу используемых понятий. Тем самым формализация — содержательное понятие доказательства. В настоящее время такой метод формализации широко применяется в математике и логике. Другим примером использования метода формализации является построение формального аналога интуитивного понятия алгоритма. Было предложено несколько способов такой формалиации, которые оказались эквивалентными друг другу. Последнее подтверждает тезис А. Чёрча, высказанный им в 1936 г., о том, что предложенные формальные аналоги полностью описывают смысл исходного интуитивного понятия алгоритма.

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

Д. Гильберт выдвинул программу обоснования математики посредством ее Ф. Однако последующие исследования показали ограниченность метода Ф. Так, в 1931 г. К. Гёделем была доказана теорема о том, что обычная арифметика натуральных чисел не может быть Ф., т.е. истинные предложения арифметики нельзя полностью аксиоматизировать. Это указывает на принципиальную неустранимость содержательных методов исследования даже в такой науке, как математика.

Словарь философских терминов. Научная редакция профессора В.Г. Кузнецова. М., ИНФРА-М, 2007, с. 642-643.