Формализация

Формализация — это совокупность познавательных операций, обеспечивающая отвлечение от значения понятий и смысла выражений формализованной теории с целью исследования её логических особенностей, дедуктивных и выразительных возможностей. В символической логике и математике, где формализация наиболее развита, под ней понимают реконструкцию содержательной научной теории в виде формализованного языка — искусственной знаковой системы (см. Язык формализованный), предназначенной для представления некоторой научной теории (см. Теория) в процессе научного поиска (см. Наука, Методы научного познания).

Формализация подразумевает, что формализуемое знание должно представлять собой каким-то образом фиксированную совокупность утверждений и взаимосвязей между положениями теории, осуществляемое [чаще всего] с помощью аксиоматического метода. Она предполагает, что выявлены и чётко сформулированы все те логические средства, которые используются при выводе из исходных положений теории других её утверждений. Если же, наряду с аксиоматизацией и точным установлением логических средств, понятия и выражения научной теории заменяются некоторыми символическими обозначениями, она превращается в формальную систему.

Формализованная теория может рассматриваться как система объектов определённого рода (символов), с которыми можно обращаться, как с конкретными физическими объектами, а развёртывание теории свести к манипулированию этими объектами в соответствии с некоторой совокупностью правил, принимающих во внимание только вид и порядок символов. Это позволяет абстрагироваться от того познавательного содержания, которое выражается научной теорией, подвергшейся формализации. Различают два типа формализованных теорий: полностью формализованные, в полном объёме реализующие перечисленные требования, и частично формализованные, когда логические средства, используемые при развёртывании данной теории, явным образом не фиксируются.

Для определённости уместно говорить о формализации некоторой содержательной теории Т. Под теорией в данном случае имеется в виду замкнутая относительно всех своих логических следствий совокупность утверждений, относящихся к соответствующей предметной области. Это означает, что все следствия, которые можно получить в Т в рамках корректных рассуждений, также относятся к теории Т. Возможности формализации теории Т за счёт построения соответствующего исчисления (формализованной теории) ФТ, а также взаимоотношения между Т и ФТ, если такую возможность удаётся некоторым образом реализовать, зависят от ряда обстоятельств. Обычно принципиальную возможность формализации содержательной теории Т связывают с тем, насколько эта теория Т подготовлена к данной операции. Речь идёт о её развитости, достаточной степени эксплицированности её понятийного аппарата. Возможность формализации существенно возрастает при разрешимости теории, то есть при существовании процедуры, позволяющей относительно любого сформулированного в языке теории предложения решать, принадлежит оно к теории или нет.

Наиболее важным средством, которое открывает принципиальную возможность формализации содержательной теории Т, служат выразительные возможности символического языка, с помощью которого предполагается отобразить Т. Следует отметить, что язык исчисления предикатов позволяет записать в символической форме любое обычное или научное предложение. Для этого достаточно дополнить этот язык символами (константами) используемых в предложении предикатов и, может быть, ещё так называемыми функциональными константами, о чём для простоты можно не говорить. Однако иметь возможность осуществить символическую запись любого предложения теории Т отнюдь не значит её формализовать. Для признания того, что ФТ формализует Т, необходимыми являются, по крайней мере, следующие три условия:

1. Язык L исчисления, используемого для формализации, должен давать возможность выразить любое предложение A теории Т с помощью некоторой формулы ФТ, которая при содержательной её интерпретации порождает предложение, которое приемлемо трактовать как выражающее ту же мысль, что и A.
2. Исходные постулаты (аксиомы) ФТ при получении из них теорем должны рассматриваться как цепочки бессодержательных символов, из которых по фиксированным правилам вывода получаются новые цепочки символов (теоремы). Иначе говоря, процесс получения теорем не должен осуществляться на основании очевидности, подтверждаемости практикой и так далее.
3. Между классом теорем ФТ и классом содержательно истинных утверждений теории Т должно быть определённое оговорённое отношение, позволяющее ФТ считать формализацией Т (точнее об этом ниже).

Пункт [2] существенным образом отличает ФТ от Т. В Τ не обязательно есть фиксированные правила вывода, и для получения новых утверждений можно опираться на содержательный смысл терминов и имеющийся контекст. Если, например, в Т содержится утверждение, что событие α произошло раньше события β, то мы обязаны по содержательным основаниям относить к верным утверждениям теории Т также и то, что β произошло позже α. Вместе с тем мы не обязаны фиксировать это. Иначе в ФТ. Здесь логические связи между отношениями раньше и позже должны быть явным образом отображены. И если указанные отношения обозначаются как «и» соответственно, то ФТ должна содержать правило, позволяющее переходить от (α < β) к (β > α). Очевидно, в ФТ придётся указать также на транзитивность указанных отношений. Кратко говоря, в ФТ придётся отобразить логику данных отношений, необходимую для описания соответствующей предметной области. При этом сама эта логика может зависеть от того, например, будет ли считаться время непрерывным или дискретным, бесконечно или конечно делимым, даже если в Т эти вопросы не обсуждаются.

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

В связи с пунктом [3] следует иметь в виду, что ФТ в явном виде содержит всю необходимую для формализаций теории Т логику и математику и соответствующий им класс правил или содержательно интерпретируемых теорем, например, закон контрапозиции импликации: (A → B) → (¬ B → ¬ A) и так далее, которым фактически нет соответствия в Т. Кроме того, Τ обычно не детерминирует всех логических взаимоотношений высказываний, содержащих используемую в Т терминологию. Поэтому ФТ практически всегда задаёт ту или иную экспликацию этой терминологии. Если даже отвлечься от возможности использования в ФТ различных базовых логик и математик, то уже только оправданные содержанием Т логические различия в экспликациях терминологии позволяют построить для одной и той же содержательной теории Т множество альтернативных формализаций. При этом теория Т в зависимости от того, какая конкретная формализация будет сочтена адекватной, будет в той или иной степени менять свой смысл. Логическая операция должна только указать, чем отличаются возможные альтернативы, но не указывать какую-то из них в качестве более предпочтительной, не говоря уже более верной. Чтобы иметь возможность содержательного обсуждения теории ФТ, в частности, говорить о её непротиворечивости, полноте, доказуемости или недоказуемости в ней теорем определённого рода, используется так называемый метаязык (в отличие от языка, на котором сформулирована ФТ), и все верные утверждения такого рода относят к метатеории МФТ.

Проблему формализации содержательной теории Т в ФТ можно считать решённой, если в рамках метатеории МФТ удаётся показать, что каждому истинному в принятой интерпретации предложению Т соответствует доказуемое утверждение ФТ (теорема полноты), и наоборот (теорема адекватности). В силу разных причин такого положения не всегда удаётся добиться. Об этом говорит, в частности, известная теорема К. Гёделя (1931) о неполноте непротиворечивой формализованной арифметики. Дело в том, что некоторая формализуемая теория Т может содержать столь богатый выразительными возможностями язык, что в её рамках могут строится утверждения о формализующей её системе ФТ и, значит, отображаться в последней. Происходит так называемые замыкание языка и метаязыка. Любая непротиворечивая формализация теории Τ оказывается принципиально неполной, так как любое изменение ФТ порождает класс новых содержательно истинных в МФТ и в самой Т предложений. Именно такого рода теорией доказывается содержательная арифметика. В объектном языке формализующей эту арифметику теории ФТ можно строить утверждения о самой этой теории, которые при содержательной интерпретации становятся истинными предложениями теории Т. В ФТ воспроизводится, в частности, некоторая форма парадокса лжеца, так как всегда находится формула, утверждающая свою собственную недоказуемость в ФТ. Такая формула содержательно истинна именно потому, что в ФТ недоказуема. Её истинность в Т и при этом недоказуемость в ФТ говорит о неполноте последней. В то же время теорема Гёделя о неполноте не исключает возможности полной формализации более узких фрагментов математики. Теорема Гёделя и ряд других (например, теорема А. Тарского о неформализуемости понятия истины для таких теорий) выявили ограниченность дедуктивных и выразительных возможностей формализмов. Во всех тех случаях, когда мы имеем дело с достаточно развитыми научными теориями, процесс формализации не может быть завершён. Формализация не может исчерпать всего богатства содержания таких теорий. Развитие научного знания, в особенности на его наиболее высокотеоретизированных уровнях, осуществляется посредством взаимодействия содержательных и формальных методов исследования при определяющей роли первых.

В целом, несмотря на ряд ограничений, формализация является эффективным средством выявления и уточнения содержания научной теории. Вся совокупность познавательных приёмов и средств, лежащих в основе формализации, ориентирована на то, чтобы обеспечить необходимое соответствие между содержательной научной теорией, подвергаемой формализации, и формальной системой, возникающей в результате её формализации: класс выводимых в формализованной теории формул должен совпадать с классом содержательно-истинных положений подвергшейся формализации теории (но обратное утверждение, как правило, неверно). В этом смысле можно утверждать, что содержательная научная теория служит своеобразным «эталоном», от степени соответствия которому зависят в значительной мере достоинства формализованной теории. Поскольку для построения формальной системы необходимо использовать (хотя и весьма в ограниченном объёме) естественный язык и в терминах этого языка проанализировать её структуру, описать логические особенности формализма (непротиворечивость, разрешимость), то это означает, что формализация предполагает содержательное мышление также и в качестве средства построения и исследования своих собственных дедуктивных и выразительных возможностей.

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