отождествление определенного фрагмента научного языка, фактически используемого научным сообществом, для ведения дискуссий на определенную тему с некой математической моделью этого языка, позволяющей представить важные с точки зрения данной дискуссии фрагменты научного знания и когнитивные операции с ними таким образом, чтобы представления этих фрагментов знания и операций не несли никакой дополнительной смысловой нагрузки, т. е . не выполняли никаких информационных функций, кроме заранее и явным образом оговоренных. Чаще всего понятие формализации вводится как неформальное понятие, поскольку оно должно быть значимо для всех используемых или только возможных формализованных языков. Вместе с тем представляется, что универсальность понятия о формализации вряд ли пострадала бы при формализации самого этого понятия в одном из универсальных языков современной науки, напр. языке второпорядковой логики или одной из сильных версий первопорядковой теории множеств. Такой перевод даже если и не добавил бы ясности к пониманию сути формализации теми, кто фактически осуществляет такую деятельность, во всяком случае, имел бы то положительное следствие, что он позволил бы отсечь некомпетентную критику невежественных в точных науках мыслителей, а также популярные в определенных кругах спекуляции по поводу «пределов формализуемости». Поскольку формализация предполагает замену научного языка некоторой его математической моделью, она является одной из форм математизации науки. При этом формализация, очевидно, является ядром этого процесса, поскольку большинство лежащих за ее пределами математизирующих операций могут быть представлены в качестве разновидностей косвенной формализации. Например, когда мы от качественной оценки степеней достоверности утверждения переходим к количественной, мы уже получаем возможность применить к неформальным рассуждениям о степенях достоверности стандартные процедуры перевода в язык формализованной арифметики (или анализа).
Поэтому, несмотря на то, что количественное рассуждение о степенях достоверности в целом может оставаться неформальным, в любой момент может быть осуществлена точечная проверка вызывающих сомнение аргументов в соответствующем формализованном языке. Некоторое время в определенных областях науки и философии доминировало представление о том, что перевод научной теории в определенные разновидности формальных языков позволяет «обосновать» содержание этих теорий. Данное воззрение, восходящее к формалистической программе Д. Гильберта, следует признать неадекватным. Даже если формализация некоторых теорий в ряде случаев действительно позволяет повысить степень приемлемости этих теорий с точки зрения научного сообщества, этот эффект остается более или менее случайным и не связан напрямую с сутью формализации как таковой. Другой важной особенностью формализации является ее творческий характер. Формализация может быть успешной или неуспешной, и построение успешной формализации едва ли может быть алгоритмизировано. Творческий характер формализации обусловлен тем, что формализация есть операция, позволяющая сделать определенный вид научных рассуждений «чисто формальным», в то время как никакой «чистой формы вообще», с которой можно было бы соотнести формализуемые в данном конкретном случае научные рассуждения, не существует. Таким образом, осуществляющий формализацию агент должен сам выделить и упорядочить те составные части содержания формализуемой теории, учет которых в качестве компонентов формы высказывания позволит повысить качество научного исследования и привести к его дальнейшему развитию. Поэтому способность удачно формализовать связную совокупность знаний о некоторой предметной области говорит о более глубоком проникновении в содержание этих знаний, нежели способность оперировать ими, оставаясь лишь на «содержательном» уровне. На первый взгляд, творческий характер формализации порой ограничен рамками того семейства логических формализмов с их стандартными семантиками, которое признается наиболее общей концептуальной рамкой такой формализации. Например, в 1920–1980-е гг. такой рамкой оставалась классическая первопорядковая логика, возможно, с отдельными выходами на уровень первопорядковой теории множеств либо второпорядковой логики. Однако такое признание было вызвано не какой-то узостью мышления специалистов в области формальных языков, а спецификой решаемых ими задач, значительная часть которых сводилась к выражению свойств полноты бесконечных структур (таких, как «для любого числа существует большее число» и «между любыми двумя различными числами находится третье число»).
Именно эти свойства выражаются с помощью стандартных кванторов наиболее естественным образом. Однако после того как компьютерная революция сделала актуальным изучение конечных структур (таких как вычисления и базы данных), все больше роль стандартного набора выразительных средств приобретают иерархия обобщенных кванторов, различные версии лямбда-исчисления, линейной логики и т. д. Таким образом, универсализация на каждом данном этапе развития науки определенного семейства формальных языков является естественным отражением фундаментальных сходств решаемых этой наукой задач. К общепризнанным позитивным эффектам формализации относят возможность яснее сформулировать те допущения, от которых зависят достигнутые наукой результаты, решить некоторые старые вопросы, дискуссия по которым на содержательном уровне, казалось бы, зашла в безнадежный тупик, а также лучше оценить осмысленность этих вопросов и поставить новые. Эта оценка не является, конечно, окончательной, поскольку принятая формализация научных знаний в любой момент может быть заменена на новую, в рамках которой взгляд на состояние формализуемых знаний может кардинально измениться. Кроме того, продвижение в решении вопросов, вызывающих содержательный интерес, как правило, «покупается» ценой траты усилий на решение собственно «внутренних», не интересных с неформальной точки зрения мелких и крупных затруднений, на которые неизбежно наталкивается развитие каждого конкретного формализма. Так что степень полезности каждой конкретной формализации в развитии науки может быть очень приблизительно представлена как соотношение суммы решенных затруднений, ранее возникших на неформальном уровне и вновь найденных интуитивно интересных проблем с возникшими в результате формализации новыми интуитивно маловразумительными затруднениями, возникающими при практическом использовании полученного формализма. Г. К . Ольховиков