Россия
В статье анализируется содержание, функции и возможности такого метода научного познания, как формализация научных теорий. Разработка этого метода произошла в 30-х годах XX в. для решения проблем обоснования математических теорий. Наиболее эффективно этот метод был использован в таком направлении обоснования математики как формализм, основателем которого был выдающийся немецкий математик Д. Гильберт. В статье рассмотрены те принципиальные трудности и ограничения, с которыми столкнулась реализация этой программы (результаты К. Геделя и А.Черча). Это, однако, не умаляет особой природы и важности метода формализации как эффективного способа уточнения объективного содержания научных теорий.
наука, метод, математика, метаматематика, формализация.
Метод формализации научных теорий является одним из основных методов метатеоретического уровня научного знания [1; 3; 5; 9]. Предметом последнего являются реальные научные теории и их анализ с точки зрения соответствия принятым в той или иной области науки критериям состоятельности и обоснованности научных теорий. В математике такими критериями являются логическая непротиворечивость, полнота аксиом, разрешимость, то есть существование способа определения относительно любого ее высказывания возможности его выведения из принятой системы аксиом, истинность теории. Для решения этих по своей сути методологических проблем в математике в 30-х годах XX в. был создан специальный раздел – метаматематика, специально занимающийся решением проблем обоснования математического знания, анализом оснований математических теорий. Одним из создателей метаматематики явился выдающийся немецкий математик XX в. Д. Гильберт.
Он выдвинул и разработал вместе со своими учениками программу решения проблем обоснования математических теорий, которая получила название «формализм» или формалистская программа обоснования математики. Одним из главных методов реализации этой программы был выдвинут метод формализации реальных математических теорий с тем, чтобы относительно каждой из этих формализованных систем строго конструктивно, то есть на уровне работы только с символами (знаками) системы решить вопросы об их непротиворечивости, полноте, разрешимости и истинности. Любое, как положительное, так и отрицательное решение этих проблем для формализованной модели той или иной математической теории можно смело переносить на саму теорию. Установление формально-логической непротиворечивости некоторой теории означает доказательство того, что в ней никогда не появится логическое противоречие между любыми ее высказываниями, доказательство того, что в этой теории в принципе невозможно получить высказывание вида «А&-А». Поскольку математические теории, как правило, строятся аксиоматически, постольку метаматематика ставит перед собой в качестве одной из главных задач определить, является ли множество аксиом некоторой математической теории действительно достаточным, а точнее – необходимым и достаточным для чисто логического выведения всех остальных истинных высказываний теории только из ее аксиом. Эта проблема получила название проблемы полноты. Одной из задач проблемы полноты системы аксиом является установление независимости аксиом друг от друга, то есть их не выводимости друг из друга. Проблема разрешимости для математической теории заключается в установлении того, что любое из ее высказываний действительно может быть получено из ее аксиом в конечное число шагов и с помощью конечного числа операций. И, наконец, решение проблемы истинности для математической теории состоит в нахождении для нее модели или области ее интерпретации. Эти проблемы: установление логической непротиворечивости реальных математических теорий, полноты и независимости их аксиом, разрешимости и истинности доказательств и являются главными задачами метаматематического исследования [10].
В чем состоит основная трудность в решении этих проблем для реальных математических теорий? Дело в том, что все реальные математические теории хотя и имеют дело не с эмпирическими объектами, а с идеальными математическими объектами (точки, прямые, числа, множества, структуры и др.), являются, тем не менее, содержательным знанием. Содержательное знание это такое знание, термины и высказывания которого имеют некоторое значение и смысл, то есть определенную интерпретацию. Быть содержательным и означает не что иное, как иметь интерпретацию. Однако, работа с содержательным знанием необходимо предполагает опору на интуицию и интуитивное знание, значительная часть которого является неявным и трудно контролируемым знанием. Субъективность научного знания помогает творчеству, но мешает решению проблем объективности и обоснованности научного знания. Формализация содержательной теории имеет в качестве одной из своих главных целей сведение к минимуму ее опоры на интуицию и интуитивное знание и тем самым уточнение ее объективного содержания.
Формализация некоторой содержательной теории означает построение для нее формальной модели, то есть отображение теории в некоторую чисто синтаксическую языковую конструкцию, состоящую только из терминов и символов, не имеющих никакой интерпретации, никакого внешнего значения. Все собственные термины, а также логические и не логические символы формальной системы обозначают только самих себя и ничего более. Как известно, первым идею формализации всех математических теорий для установления их реальной логической структуры и решения проблем их непротиворечивости, полноты и эффективности выдвинул Д. Гильберт [2]. Для решения этих задач он сформулировал программу обоснования математики, которая получила название «формалистская программа обоснования» или просто «формализм». Гильбертовская программа обоснования математики была альтернативой другим программам обоснования математики, выдвинутым в начале двадцатого века, и прежде всего логицизму (Б. Рассел, А. Уайтхед и др.) и интуиционизму (Л.Э. Брауэр, А. Гейтинг, А. Пуанкаре, Г. Вейль и др.) [6; 8]. Выше, рассматривая дедуктивно-аксиоматический метод построения научных теорий, мы уже частично раскрыли подход Гильберта к формализации эвклидовой геометрии. Неожиданным результатом этого процесса стало установление того факта, что всем известная в течение многих веков система аксиом геометрии Эвклида оказалась явно неполной. Гильберт доказал, что для строго аксиоматического построения геометрии Эвклида требуется не пять аксиом, как это было у Эвклида и что считалось чем-то очевидным для всех математиков в течение многих столетий, а двадцать независимых аксиом. Тем самым Гильбертом была одновременно доказана и неполнота систем аксиом неевклидовых геометрий, построенных Н.И. Лобачевским, Я. Бойаи и Б. Риманом. В построенной Гильбертом формализованной системе эвклидовой геометрии термины «точка», «прямая», «плоскость» обозначали только самих себя, и с ними не нужно было связывать никаких других значений. Правда, логические правила вывода не были формализованы Гильбертом в его системе эвклидовой геометрии, поэтому его построение в целом носило полуформализованный характер. Затем, при построении формализованной системы арифметики Гильберту уже удалось устранить этот недостаток и формализовать не только аксиомы арифметики, но и правила вывода, то есть логику, используемую при доказательстве теорем арифметики. Прежде чем описать систему формализованной арифметики Гильберта, вернемся еще раз к понятию формальной теоретической системы или просто формальной системы. Как строится такая система? Для ее построения необходимо осуществить следующие действия. Сначала вводится набор знаков формальной системы. Это – некоторое множество символов, как правило, множество букв некоторого алфавита, например, заглавных и прописных букв латинского алфавита (А, B, С, …а,b,c …); запятые, разделяющие отдельные символы или строчки символов друг от друга; логические символы: → («если, то»), &,·(«и»), Ú («или»), -,ù («не»), (х) («все»), (Ех) («существует x»); и, наконец, скобки для отделения одних групп символов от других ( ). Затем вводится понятие формулы. Под формулой данного языка понимается любая строчка или последовательность исходных символов данного языка. Затем вводится понятие правильно построенной формулы для данного формального языка. Как правило, это делается индуктивным способом, путем демонстрации отдельных случаев как правильно построенных формул, так и неправильно построенных. Например, правильно построенными формулами являются такие формулы, как: a&b; (a&b)&c «a&(b&c); aÚb; (x) A(x) → B(x); Еx A(x).
Примерами неправильно построенных формул являются: A, B, Е; (x) A; (a),b; →x; b→; b, →. и т.д.
Далее. Из всего множества правильно построенных формул выбирается некоторое небольшое подмножество, которое должно стать основанием, фундаментом формальной теории. Это подмножество исходных формул формальной теории называется ее аксиомами. Следующий шаг в построении формализованной теории – это введение правил преобразования одних правильно построенных формул (строчек символов) в другие. Эти правила называются также правилами формального вывода. Введем вслед за Гильбертом такие правила. В принципе число таких правил может быть бесконечным, поэтому среди них выбирают небольшое множество так называемых «основных», к которым должны быть сводимы все остальные правила преобразования, разрешенные в данной формальной системе или «законные» правила вывода. Пусть заглавные буквы латинского алфавита (A, B, C….) обозначают любые правильно построенные формулы нашего формального языка. Разобьем вслед за Гильбертом все основные правила преобразования одних правильно построенных формул в другие на следующие группы [2, стр. 367–369]:
I 1-4. Логические аксиомы следования
1. А→(В→А)
2. (А→(А→B))→(A→B)
3. (A→(B→C))→(B→(A→C))
4. (B→C)→((A→B)→(A→C))
II 5-10. Логические аксиомы, касающиеся конъюнкции и дизъюнкции.
5. A·B→A
6. A·B→B
7. A→(B→(A·B))
8. A→AVB
9. B→ AVB
10. ((A→C)·(B→C))→((AVB→C))
III 11-12. Логические аксиомы отрицания
11. 
(закон противоречия)
12. 
(закон двойного отрицания)
Эти двенадцать аксиом и образуют полную систему аксиом такой формально-логической теории как исчисление высказываний. Из этих аксиом можно вывести неосновные логические правила вывода (правила преобразования одних правильно построенных формул исчисления высказываний в другие). Например, из аксиом 11 и 12 исчисления высказываний следуют в качестве теорем следующие правила преобразования: 
а также логический принцип: ((A→B)·(
→B))→B. Далее к 12 аксиомам исчисления высказываний Гильберт добавляет ещё одну аксиому, чтобы превратить (достроить) исчисление высказываний в более широкую формально-логическую систему – исчисление предикатов. Последнее позволяет формализовать любые высказывания (в том числе и высказывания арифметики) с кванторами (логическими функциями) такими как «все» («любой»), обозначаемый символом (х), «тот, который», обозначаемый символом A(a) (дословно «тот a, который имеет признак A») и «существует», обозначаемый символом E(x) (читается как «существует некоторый объект x»).
Эта 13-я аксиома выглядит так: 
или, более точно, 
,
(где ε – трансфинитная логическая функция выбора)
Она читается так: «высказывание A(a) верно, по крайней мере, для одной вещи x».
Аксиома 13 образует IV-ю группу аксиом. На основании аксиомы 13 вводятся такие формулы:
(x) A(x) →A(a) (аксиома Аристотеля)
A(x) → E(x)
(закон исключенного третьего).
Затем к логическим аксиомам исчисления предикатов Гильберт добавляет уже собственно арифметические аксиомы, образующие уже V-ю и VI-ю группу аксиом формализованной арифметики.
V 14-15 Аксиомы равенства, определяющие отношение «равно»
14. a = a
15. (a=b) → (A (a) →A(b))
VI 16-17 Аксиомы числа
16. a'≠0, где a' – «число, следующее за a»
17. (A(0)·(x)(A(x)→A(x'))→A(a) – принцип полной индукции для последовательностей.
Целые числа 1,2,3,… в системе формализованной арифметики натуральных чисел Гильберта записываются с помощью символов 0',0'',0''',…
Гильберт так подводит итог сущности построенной им системы формализованной арифметики натуральных чисел: «…В моей теории содержательные выводы заменены внешними действиями, подчиняющимися определенным правилам; тем самым аксиоматический метод получает ту надежность и законченность, которая для него доступна и в которой он нуждается для того, чтобы служить основным средством теоретических изысканий» [2, с. 369].
Что отличает формализованную научную теорию от неформализованной? Главное и принципиальное отличие состоит в том, что в формализованной (или формальной) теории доказательство является: а) предметом чувственного (наглядного) созерцания и б) оно полностью обозримо от начала до конца (или, как говорит Гильберт, оно является «полностью сообщаемым»). Таким образом, основным критерием надежности, строгости и эффективности того или иного доказательства в формализованной теории является его контролируемость чувственным созерцанием, его прозрачность и очевидность для последнего. В формализованных теориях правильность мышления и его результатов берется под контроль чувственного созерцания. И в этом отношении (формальная) математика сближается с естествознанием и его стандартами и критериями существования, истинности, обоснованности и определенности знания. Интуитивные же аспекты математического и естественнонаучного мышления рассматриваются при таком подходе как играющие лишь эвристическую функцию в научном познании, но отнюдь не критериальную, как, например, в эпистемологии Р. Декарта. Интеллектуальная интуиция попадает при этом под двойной контроль. С одной стороны, под контроль логики, а, с другой, под контроль чувственного созерцания и его разрешающей способности как средства познания.
В 30-е годы XX в. К. Геделем, одним из учеников Д. Гильберта, были получены принципиальные результаты, показавшие познавательные границы возможностей формализации содержательных теорий и лежащей в основе метода формализации предпосылки об исключительной надёжности метода чувственного созерцания знаков и символов как материальных объектов элементарного (простейшего) характера. С одной стороны, метод формализации оказался абсолютно надежным средством построения таких теорий формальной (математической) логики как исчисление высказываний и исчисление предикатов первого порядка. Полноту и абсолютную непротиворечивость исчисления высказываний впервые доказал Г. Фреге в конце XIX в. Затем этот результат был получен и другими известными логиками и математиками (Б. Расселом, А. Уайтхедом, Д. Гильбертом, П. Бернайсом, В. Аккерманом, Я. Лукасевичем) для различных систем исчислений высказываний, имеющих своим основанием разные системы аксиом. В 1939 г. К. Гедель доказал теорему о полноте исчисления предикатов, используемого в качестве формальной логической системы при формализации математики. Согласно этой теореме множество всех логических утверждений математики совпадает (равно) с множеством всех формул исчисления предикатов. Позже полноту и абсолютную непротиворечивость исчисления предикатов первого порядка доказали и другие выдающиеся логики XX в. (Р. Карнап, А. Черч, С. Клини и др.). Таким образом, полностью формализованные теории в науке возможны, но, к сожалению, таких теорий оказалось только две и притом чисто логических: исчисление высказываний и исчисление предикатов первого порядка (термины, обозначающие только свойства объектов, но не отношения между ними; термины, обозначающие отношения, это, как минимум, двухместные предикаты, или предикаты второго порядка). Любая же простейшая содержательная теория в науке, начиная с арифметики натуральных чисел, описывает не только свойства некоторых объектов, но и отношения между ними, то есть включает в свой язык двухместные (и более местные) предикаты или термины, обозначающие отношения между объектами. Могут ли быть полностью формализованы такие теории? А ведь таких теорий – подавляющее большинство даже в математике и логике, не говоря уже о естествознании и социально-гуманитарных науках. Занимаясь проблемами полноты формализованной арифметики натуральных чисел и её непротиворечивости, К. Гедель в 1931 г. получил результаты, радикально расходящиеся с первоначальным оптимизмом сторонников программы обоснования математики Д. Гильберта и достаточно драматичные по их философскому значению, но при этом абсолютно формально строгие в плане их доказательности. Первая теорема Геделя гласит, что нельзя полностью формализовать такую теорию как арифметика натуральных чисел, а значит и все другие научные теории, включающие эту теорию в качестве своей части. А это – практически все математические и физические теории (геометрия, алгебра, математический анализ, теория вероятностей, теория функций действительного и комплексного переменного, механика и все другие физические и социальные теории, где применяется количественное описание действительности). С чисто технической стороны теорема Геделя утверждала, что в любой формализованной системе арифметики всегда можно сформулировать на её языке некую правильно построенную формулу (и возможно имеющую содержательный исторический эквивалент), которую нельзя будет ни доказать, ни опровергнуть средствами этой системы. При этом данная теорема никак не запрещает сколь угодно полную формализацию любой содержательной теории. Она утверждает лишь принципиальную невозможность абсолютно полной формализации реальных содержательных теорий. Вторая теорема Геделя имела ещё более пессимистическое эпистемологическое звучание. Гедель доказал строгим, финитным образом, что непротиворечивость любой достаточно богатой формализованной системы (и, в частности, формализованной системы арифметики натуральных чисел) нельзя доказать средствами самой этой системы. А это означало, что для любой формализованной теории, например, арифметики натуральных чисел невозможно в принципе получить доказательство её абсолютной (или синтаксической) непротиворечивости (то есть доказать невозможность получения в ней в качестве одного из ее следствий формулы 
). А ведь вера в возможность доказательства абсолютной непротиворечивости формализованных математических теорий, и , прежде всего, наиболее простой из них – арифметики натуральных чисел, была главной целью программы обоснования математики Гильберта, как программы, альтернативной по отношению к другим программам обоснования математики – логицизму (Г. Фреге, Б. Рассел и др.) и интуиционизму (Л.Э. Брауэр, А. Гейтинг и др.) [7; 8]. Поскольку логицистская программа обоснования математики обнаружила трудности своей реализации уже в 20-х годах XX в. (после попытки ее реализации Б. Расселом и А. Уайтхедом в «Principia Mathematica»), постольку единственной серьезной альтернативой программе Гильберта была только программа интуиционизма (конструктивизма). Но это была уже другая метаматематика. Представители интуиционизма не отрицали огромной роли формального построения математических теорий, правда, уже на основе принципов конструктивизма и контроля со стороны элементарной интуиции. На этом пути А. Гейтинг в 30-х годах XX в. построил формальную систему интуиционистской логики, а С. Клини в 50-х годах – формальную систему интуиционистского математического анализа [4].
В связи с невозможностью чисто формального обоснования математических теорий законно возникает законный вопрос о необходимости формализации математики. Тем более, что с самого начала формализация рассматривалась только как средство решения определенных метаматематических проблем (полноты, непротиворечивости, разрешимости и истинности содержательных математических теорий). Однако, после результатов, полученных Геделем, стало ясно, что чисто формальное обоснование любой математической теории в принципе невозможно. Его можно осуществить только средствами другой формальной теории. Но отсюда с неизбежностью следует вывод, что любое такое доказательство будет всегда только относительным, а не абсолютным. Поскольку же непротиворечивость последней метатеории в этом ряду всегда будет только условной, предположительной, постольку и все остальные теории, которые использовали данную метатеорию для доказательства своей непротиворечивости, будут также непротиворечивыми лишь в условном смысле. И регресса в бесконечность (метаматематическую) при чисто формальном способе обоснования любой математической теории невозможно избежать в принципе.
Но если проблема обоснования математической теории не может быть решена с помощью формализации, тогда нужен ли вообще метод формализации в науке? Считаю, что ответ на этот вопрос должен быть положительным. Почему? Во-первых, потому, что только с помощью формализации теорий можно строго определить, достаточна ли аксиоматическая база тех или иных теорий как основание их логической доказательности. Только при формализации геометрии, арифметики, логических теорий, математического анализа, теории структур и др. впервые удалось выявить действительно необходимую аксиоматическую базу этих теорий. Как правило, оказывалось, что она должна быть значительно мощнее, чем это предполагалось ранее в конкретных содержательных теориях. А это значит, что практически все реальные математические теории были логически доказательными лишь частично, хотя при этом выдавали себя как строго доказательные. Яркий пример тому – традиционная геометрия Эвклида. Если мы хотим показать, что научные теории являются действительно строго логически доказательными, для этого существует только один путь – их формализация. Это, разумеется, не достаточное, но абсолютно необходимое условие обоснования логической доказательности теорий. С гносеологической точки зрения формализация научных теорий полезна также тем, что позволяет минимизировать решение проблемы их истинности. Эта минимизация заключается в том, что проблема истинности теории при её формально-аксиоматическом построении сводится только к проблеме доказательства истинности её аксиом. Формализация научных теорий имеет также ту пользу, что расширяет (практически неограниченно) область их применения, не ограничиваясь только первоначальной областью объектов, с которой было связано их историческое возникновение. А, безусловно, что максимально точное, строгое и доказательное описание как можно большего количества объектов является одним из идеалов и главных целей научного познания действительности. Далее. Формализация научных теорий позволяет существенным образом задействовать возможности чувственного познания при построении и обосновании научных теорий и тем самым осуществить гармоничное дополнение и взаимодействие в рамках теоретического моделирования действительности рационального, чувственного и интуитивного познания как одинаково необходимых компонентов при построении научных теорий. Далее. Только формализованное научное знание может быть передано вычислительным машинам и компьютерам, поскольку последние могут работать и совершать операции только с материальными объектами (в данном случае с символами, строчками символов и формулами). Конечно, вычислительная математика требует особых способов формализации эмпирического и теоретического научного знания, подчиняя их задачам составления соответствующих программ на языке, распознаваемом машиной и «понятном» для неё. В любом случае без формализации реального научного знания и реальных содержательных теорий здесь не обойтись. В этой связи важно подчеркнуть следующее немаловажное обстоятельство: известная теорема Геделя о неполноте, о которой говорилось выше, не налагает никаких принципиальных ограничений на возможность сколь угодно полной формализации научных теорий. Единственное, что она утверждает, так это только то, что невозможна абсолютно полная (стопроцентная) формализация содержания теории. Но она не запрещает возможность сколь угодно полной формализации любой теории, что абсолютно необходимо для любых компьютерных математических программ. Наконец, только при формализации научного знания удаётся максимально точно и однозначно определить многие понятия, что также является одним из идеалов научного познания. Например, именно на этом пути удалось получить строгое определение понятия алгоритма, которое на интуитивном уровне всегда широко использовалось не только в математике, но и в науке в целом. Так, А. Черч в 1936 г. доказал, что широко используемое в математике понятие рекурсивной функции может быть определено как функция, вычислимая с помощью некоторого алгоритма. И только после уточнения понятия алгоритма удалось обнаружить существование в реальной математике целого ряда реальных алгоритмически неразрешимых проблем. Разработка точного понятия алгоритма позволила в свою очередь уточнить понятие эффективной деятельности, в том числе и на уровне теоретического познания [3, с. 15]. Как известно, большинство современных метаматематических и металогических теорий строится сегодня именно конструктивистским образом, сознательно опираясь на понятие алгоритма на уровне построения метатеорий [10].
1. Вейль Г. Математическое мышление. М., 1989.
2. Гильберт Д. Основания геометрии. М.-Л., 1948.
3. Гильберт Д., Бернайс П. Основания математики. Издание второе. М., 1982.
4. Клини С., Весли Р. Основания интуиционистской математики. М., 1978.
5. Лебедев С.А. Методы научного познания. М.: Альфа-М. 2014. - 272 с.
6. Лебедев С.А. Философия научного познания: основные концепции. М.: Издательство Московского психолого-социального университета. 2014. - 272 с.
7. Лебедев С.А., Коськов С.Н. Эпистемология и философия науки: классическая и неклассическая. М.: Академический проект. 2014. -295с.
8. Философия математики и технических наук. Под общей ред. С.А. Лебедева. М.: Академический проект. 2006. - 779 с.
9. Lebedev S.A. Metatheoretic knowledge in science, its structure and functions// Journal of International Network Center for Fundamental and Applied Research. 2015. - № 2(4). - C. 97-104.
10. Lebedev S.A. Principles of mathematic theories//Вопросы философии и психологии. - 2015. - №2 (4). - С. 100-111.
