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

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

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