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

Исторически первым формализованным языком была силлогистика Аристотеля (см. Силлогистика), реализованная с помощью стандартизованного фрагмента естественного (греческого) языка. Общую идею формализованного языка сформулировал Г. В. Лейбниц (characteristicauniversalis), предусматривавший его расширение до «исчисления умозаключений» — calculusratiocinator. В Новое время различные варианты формализованных языков разрабатывались на основе аналогии между логикой (см. Логика) и алгеброй. Решающее значение здесь имели труды О. де Моргана, Дж. Буля и их последователей, в особенности Э. Шрёдера и П. С. Порецкого. Современные формализованные языки — в их наиболее распространённых формах — восходят к труду Г. Фреге «Begriffsschrift» — «Запись в понятиях» (1879), от которого идёт главная линия развития языка логики высказываний (см. Логика высказываний) и [объемлющей её] логики [многоместных] предикатов (см. Логика предикатов), а также применение этих логических языковых средств к задачам обоснования математики.

Характерная структура формализованных языков включает следующее:

· задание алфавита исходных знаков;

· индуктивное определение (правильно построенной) формулы языка;

· задание правил образования;

· задание правил вывода;

· задание правил преобразования, которые сохраняют выделенную логическую характеристику формул (истинность, доказуемость и другие).

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

Формализованные языки различаются по своей логической силе, начиная с «классических» языков (в которых в полной мере действуют аристотелевские законы тождества, противоречия и исключённого третьего, а также принцип логической двузначности — см. Законы логики) и заканчивая многочисленными языками неклассических логик (см. Логики неклассические), позволяющих ослаблять те или иные принципы, вводить многозначность оценок формул либо их модальности. Разработаны языки, в которых логические средства в том или ином смысле минимизируются. Таковы языки минимальной и положительной логик или язык логики высказываний, использующий единственную логическую операцию, например штрих Шеффера.

Формализованные языки обычно характеризуют в терминах синтактики (см. Синтактика) и семантики (см. Семантика). Но самым существенным является та логическая характеристика его формул, которая сохраняется правилами вывода (истинность, доказуемость, подтверждаемость, вероятность и прочие). Для любого формализованного языка фундаментальными являются проблемы полноты выражаемой в нём логики, её разрешимости и непротиворечивости; например, язык классической логики высказываний полон, разрешим и непротиворечив, а классической логики предикатов (многоместных) хотя и полон, но неразрешим; язык же расширенного исчисления предикатов — с кванторами по предикатам и неограниченным применением принципа абстракции — противоречив (такой была логико-арифметическая система Г. Фреге, в которой Б. Рассел обнаружил антиномию, названную его именем).

Формализованный язык может быть «чистой формой», то есть не нести никакой внелогической информации; если же он её несёт, то становится прикладным формализованным языком, специфика которого — наличие постоянных предикатов и термов (дескрипций) — например арифметических, — отражающих свойства прикладной области. Для формализации теорий высокого уровня абстракции формализованный язык может по-разному видоизменяться, расширяться либо «надстраиваться»; пример: формализация классического математического анализа как арифметики второго порядка (то есть с кванторами по предикатным переменным). В ряде случаев формализованный язык содержит логические структуры многих — даже бесконечно многих — порядков (такова, например, «башня языков» А. А. Маркова, служащая формализации конструктивной математики, или интерпретация модальностей в виде иерархии «возможных миров»). Семантическая база формализованного языка логики может быть теоретико-множественной, алгебраической, вероятностной, теоретико-игровой и другой. Возможны и такие её «ослабления», которые лишь родственны вероятностной семантике — так возникает, например, формализованный язык «нечёткой логики» (в смысле Л. Заде). Тогда язык приобретает специфическую прагматику, принимающую во внимание фактор носителя языка (дающего оценку «функции принадлежности» предмета объёму данного понятия). Здесь проявляется укрепляющаяся ныне тенденция учёта в формализованных языках «человеческого фактора» — в том или ином его виде, что явно проявляется, например, в некоторых формализованных языках логики квантовой механики. В другом направлении идёт разработка формализованных языков, семантика которых предполагает отказ от экзистенциальных допущений либо те или иные онтологические предпосылки — о допустимости правил с бесконечным числом посылок, «многосортности» предметных областей, даже противоречивых, и так далее.

Непременной особенностью формализованного языка является «возможностное» истолкование правил вывода; например, на определённом шаге мы вольны использовать либо не использовать, скажем, правило modusponens. Этой черты лишены алгоритмические языки, носящие «предписывающий» характер. Но по мере развития компьютерной логики и разработки программ «описывающего» типа это различие начинает сглаживаться. В этом же направлении действует и разработка формализованных языков, ориентированных на решения задач эвристики.