Теория моделей — раздел математической логики, который занимается изучением связи между формальными языками и их интерпретациями или моделями. Название теория моделей было впервые предложено Альфредом Тарским в 1954 году. Основное развитие теория моделей получила в работах Тарского, Мальцева и Робинсона.
Теория моделей посвящена изучению фундаментальной взаимосвязи между синтаксисом и семантикой. При этом, первому в ней отвечает формальный язык, а второму — модель — математическая структура, допускающая некоторое описание этим языком. Теория моделей возникла как обобщение существующих подходов решения метаматематических проблем, связанных с алгеброй и математической логикой. Сами эти подходы существовали давно, но при этом долгое время не рассматривались во всей своей общности, в рамках единой логико-философской парадигмы. Естественным примером в этом контексте является проблема, связанная с пятым постулатом Евклида о параллельности линий. Веками математикам не удавалось доказать его истинность, пока в XIX веке Бойяи и Лобачевский не построили неевклидову геометрию, показав тем самым, что постулат параллельности не может быть ни доказан, ни опровергнут. С точки зрения теории моделей, это означает, что система аксиом без пятого постулата допускает несколько различных моделей, то есть в этом случае — несколько вариантов реализации геометрии.
Таким образом, первоначальная теория моделей выросла из таких разделов математики как логика, универсальная алгебра, теория множеств в качестве обобщения и укрупнения существующих знаний. Поэтому первые результаты теории моделей появились задолго до её «официального» возникновения. Первым таким результатом принято считать[1] теорему Лёвенгейма — Сколема (1915). Другим крупным результатом стала теорема компактности, доказанная Гёделем (1930) и Мальцевым (1936).
Теория моделей для классической логики первого порядка является исторически первым и наиболее развитым примером теоретико-модельного подхода. В роли моделей здесь выступают множества, представляющие область возможных значений переменных. Функциональные символы интерпретируются как операции соответствующей арности над ними, а предикаты — как отношения (более подробно, см. Логика первого порядка, интерпретация).
Одним из важнейших инструментов теории моделей является теорема компактности, доказанная Мальцевым, которая утверждает, что множество формул первого порядка имеет модель тогда и только тогда, когда модель имеет каждое конечное подмножество этого множества формул.
Название теоремы связано с тем, что она может быть сформулирована как утверждение о компактности стоуновского пространства.