Формализация (НФЭ, 2010)

ФОРМАЛИЗАЦИЯ — отображение содержательного знания в формализованной теории (исчислении). Формализуемое знание должно представлять собой каким-то образом фиксированную совокупность утверждений. Для определенности уместно говорить о формализации некоторой содержательной теории Т. Под теорией в данном случае имеется в виду замкнутая относительно всех своих логических следствий совокупность утверждений, относящихся к соответствующей предметной области. Это означает, что все следствия, которые можно получить в Т в рамках корректных рассуждений, также относятся к теории Т. Возможности формализации теории Т за счет построения соответствующего исчисления (формализованной теории) ФТ, а также взаимоотношения между Т и ФТ, если такую возможность удается некоторым образом реализовать, зависят от ряда обстоятельств. Обычно принципиальную возможность формализации содержательной теории Т связывают с тем, насколько эта теория Т подготовлена к данной операции. Речь идет о ее развитости, достаточной степени эксплицированности ее понятийного аппарата. Возможность формализации существенно возрастает при разрешимости теории, т. е. при существовании процедуры, позволяющей относительно любого сформулированного в языке теории предложения решать, принадлежит оно к теории или нет. Все это важно, но главное, что открывает принципиальную возможность формализации содержательной теории Т,— это выразительные возможности символического языка, с помощью которого предполагается отобразить Т. Вообще говоря, язык исчисления предикатов позволяет записать в символической форме любое обычное или научное предложение. Для этого достаточно дополнить этот язык символами (константами) используемых в предложении предикатов и, может быть, еще так называемыми функциональными константами, о чем для простоты можно не говорить. Однако иметь возможность осуществить символическую запись любого предложения теории Г отнюдь не значит ее формализовать. Для признания того, что ФТ формализует Т, необходимыми являются, по крайней мере, следующие три условия:

(1) Язык L исчисления, используемого для формализации, должен давать возможность выразить любое предложение А теории Т с помощью некоторой формулы ФТ, которая при содержательной ее интерпретации порождает предложение, которое приемлемо трактовать как выражающее ту же мысль, что и А.

(2) Исходные постулаты (аксиомы) ФТ при получении из них теорем должны рассматриваться как цепочки бессодержатель-ных символов, из которых по фиксированным правилам вы-вода получаются новые цепочки символов (теоремы). Иначе говоря, процесс получения теорем не должен осуществляться на основании очевидности, подтверждаемости практикой ит. п.

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

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

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

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

Литература:

Клини С. К. Введение в метаматематику. М., 1957.

Е. А. Сидоренко

Новая философская энциклопедия. В четырех томах. / Ин-т философии РАН. Научно-ред. совет: В.С. Степин, А.А. Гусейнов, Г.Ю. Семигин. М., Мысль, 2010, т. IV, с. 266-267.