Формализо́ванный язы́к (формальный язык), искусственный (в отличие от естественных, например русского) язык, характеризующийся точными правилами построения выражений и их понимания. На протяжении всей истории развития математики в ней широко использовались символические обозначения для различных объектов и понятий. Однако, наряду с символическими обозначениями, математики свободно пользовались и обычным языком. Потребность в полной формализации математических теорий, т. е. в изложении этих теорий на формализованном языке, возникла в связи с задачей логического анализа математических суждений, уточнения понятия доказательства в математике. Формализованные языки, используемые для формализации математических теорий, обычно называют логико-математическими языками, т. к. в них сочетается использование математической и логической символик. Среди этих языков важное место занимают языки 1-го порядка, или элементарные языки.

Построение элементарного языка для формализации какой-либо математической теории начинается с того, что некоторым объектам из исследуемой области даются имена, называемые предметными константами. Затем некоторым операциям над объектами исследуемой области даются имена, называемые функциональными символами. Имена $𝑛$-местных операций называются $𝑛$-местными функциональными символами (иногда говорят, что такой символ имеет валентность $𝑛$). Наконец, даются имена некоторым свойствам объектов исследуемой области и отношениям между объектами. В математической логике для свойств объектов и отношений между ними используется общее понятие предиката, поэтому их имена называются предикатными символами. Каждый предикатный символ имеет определённую валентность $𝑛 ≥ 0$. Предметные константы, функциональные и предикатные символы составляют сигнатуру элементарного языка. Алфавит всякого элементарного языка наряду с сигнатурными символами содержит логические символы [обычно это логические связки $\&$ (конъюнкция), $∨$ (дизъюнкция), $→$ (импликация), $¬$ (отрицание), кванторные символы $∃$, $∀$], предметные переменные $𝑥_1, 𝑥_2, . . .,$ служебные символы $(,)$ (скобки) и « , » (запятая). Число констант, функциональных и предикатных символов может быть как конечным, так и бесконечным. Это, однако, не означает, что алфавит языка должен быть бесконечным, т. к. в качестве имён и переменных могут использоваться не только отдельные буквы, но и их сочетания.

Затем описывается синтаксис формализованного языка – правила построения осмысленных выражений. В элементарных логико-математических языках среди таких выражений различают термы и формулы. Термами называются выражения, которые являются аналогами имён объектов формализуемой теории и соответствующих именных форм. К термам прежде всего относятся предметные переменные и предметные константы. Из констант и переменных с помощью функциональных символов строятся более сложные термы: если $𝑓$ – имя $𝑛$-местной функции, а $𝑡_1, ..., 𝑡_𝑛$ – термы, то выражение $𝑓(𝑡_1, ..., 𝑡_𝑛)$ тоже считается термом. Терм, не содержащий переменных, называется замкнутым.

Из термов с помощью предикатных символов, логических связок и кванторов строятся формулы – выражения, соответствующие высказываниям и высказывательным формам обычного языка. Атомарной формулой называется любое выражение вида $𝑃(𝑡_1, ..., 𝑡_𝑚)$, где $𝑃$ – какой-либо $𝑚$-местный предикатный символ, а $𝑡_1, ..., 𝑡_𝑚$ – произвольные термы. Из атомарных формул следующим образом строятся предикатные формулы:

• все атомарные формулы суть формулы;

• если $𝐴$ и $𝐵$ – формулы, то выражения $(𝐴 \& 𝐵)$, $(𝐴 ∨ 𝐵)$, $(𝐴 → 𝐵)$, $¬𝐴$ считаются формулами;

• если $𝐴$ – формула, $𝑥$ – предметная переменная, то $∀𝑥 𝐴$ и $∃𝑥 𝐴$ суть формулы.

Выражения вида $∃𝑥$ и $∀𝑥$ называются соответственно квантором существования и квантором всеобщности по переменной $𝑥$. Часть формулы $𝐴$, которая сама является формулой, называется подформулой формулы $𝐴$. Областью действия кванторов $∀𝑥$ или $∃𝑥$ в формуле $𝐴$ называется такая её подформула $𝐵$, что $∀𝑥$ $𝐵$ или $∃𝑥$ $𝐵$ является подформулой формулы $𝐴$. Вхождение переменной $𝑥$ в формулу $𝐴$ называется связанным, если оно есть вхождение в квантор $∀𝑥$ или $∃𝑥$ либо в область действия одного из этих кванторов. Всякое вхождение переменной $𝑥$, не являющееся связанным, называется свободным. Формула без свободных переменных называется замкнутой. Иногда замкнутые формулы называют высказываниями.

Частным случаем элементарного языка является язык логики предикатов. Его сигнатура состоит из счётного множества предикатных символов каждой валентности. В этом случае предикатные символы называются предикатными переменными. Термами языка логики предикатов являются только предметные переменные. Формулы языка логики предикатов называются предикатными формулами. Синтаксические правила определяют класс осмысленных выражений формализованного языка. Понимание этих выражений, или семантика формализованного языка, обычно подразумевается при его построении. Интерпретация выражений формализованного языка, которая предполагалась при его построении, называется намеренной или стандартной интерпретацией. Наряду с ней возможны и другие интерпретации. Чтобы задать интерпретацию элементарного языка, нужно зафиксировать непустое множество $𝑀$, называемое предметной областью, каждой предметной константе сопоставить её значение – некоторый элемент из $𝑀$, каждому $𝑛$-местному функциональному символу $𝑓$ сопоставить функцию $\tilde{f} : 𝑀^𝑛 → 𝑀$, а каждому $𝑚$-местному предикатному символу $𝑃$ – некоторый $𝑚$-местный предикат на $𝑀$, т. е. функцию $\tilde{P} : 𝑀^𝑚 → \{ 0,1 \}$.

Когда выбрана интерпретация, можно расширить сигнатуру, включив в неё в качестве предметных констант имена всех элементов предметной области. Индукцией по построению замкнутого терма $𝑡$ в расширенной сигнатуре определяется его значение $|𝑡|$ в данной интерпретации: значения констант указаны при задании интерпретации, а значение терма $𝑓(𝑡_1, . . . , 𝑡_𝑛)$ есть $\tilde{f} (|𝑡_1|, . . . , |𝑡_𝑛|)$. Также индуктивно для каждой замкнутой формулы $𝐴$ в расширенной сигнатуре определяется её истинностное значение $|𝐴|$ в данной интерпретации. Если $𝐴$ имеет вид $𝑃(𝑡_1, ..., 𝑡_𝑚)$, то её значение есть $\tilde{P} (|𝑡_1|, . . . , |𝑡_𝑚|)$. Если $𝐴$ имеет вид $¬𝐵$, то $|𝐴| = 1$ («истина») тогда и только тогда, когда $|𝐵| = 0$ («ложь»). Аналогично, в соответствии с истинностными таблицами для логических операций $\&, ∨, →$, определяются значения формул вида $(𝐴 \& 𝐵)$, $(𝐴∨𝐵)$, $(𝐴 → 𝐵)$ через значения формул $𝐴$ и $𝐵$. Например, $[(𝐴 \& 𝐵)| = 1$ тогда и только тогда, когда $|𝐴| = 1$ и $|𝐵| = 1$. Значение формулы $∀𝑥$ $𝐴(𝑥)$ есть $0$ в том и только в том случае, когда $|𝐴(𝑚)| = 0$ для некоторого $𝑚 ∈ 𝑀$. Значение формулы $∃𝑥$ $𝐴(𝑥)$ есть $1$, если $|𝐴(𝑚)| = 1$ для некоторого $𝑚 ∈ 𝑀$. Если $|𝐴| = 1$, то говорят, что формула $𝐴$ истинна в данной интерпретации. Формула называется общезначимой, если она истинна в любой интерпретации. Каждая общезначимая предикатная формула выражает некоторый логический закон.

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

Описание синтаксиса и семантики формализованного языка обычно ведётся на каком-либо естественном языке, который таким образом выступает как метаязык по отношению к данному формализованному языку. Наряду с описанными выше языками 1-го порядка рассматриваются языки более высоких порядков. Так, в языках 2-го порядка наряду с предметными переменными используются функциональные и предикатные переменные и кванторы по ним. Логико-математические языки играют существенную роль в математической логике и исследованиях по основаниям математики. Наряду с ними широкое применение получили алгоритмические языки, или языки программирования, – формализованные языки, служащие для записи алгоритмов, подлежащих выполнению на вычислительных машинах.