Теория моделей — раздел математической логики, который занимается изучением связи между формальными языками и их интерпретациями или моделями. Название теория моделей было впервые предложено Альфредом Тарским в 1954 году. Основное развитие теория моделей получила в работах Тарского, Мальцева и Робинсона.

История возникновения

править

Теория моделей посвящена изучению фундаментальной взаимосвязи между синтаксисом и семантикой. При этом, первому в ней отвечает формальный язык, а второму — модель — математическая структура, допускающая некоторое описание этим языком. Теория моделей возникла как обобщение существующих подходов решения метаматематических проблем, связанных с алгеброй и математической логикой. Сами эти подходы существовали давно, но при этом долгое время не рассматривались во всей своей общности, в рамках единой логико-философской парадигмы. Естественным примером в этом контексте является проблема, связанная с пятым постулатом Евклида о параллельности линий. Веками математикам не удавалось доказать его истинность, пока в XIX веке Бойяи и Лобачевский не построили неевклидову геометрию, показав тем самым, что постулат параллельности не может быть ни доказан, ни опровергнут. С точки зрения теории моделей, это означает, что система аксиом без пятого постулата допускает несколько различных моделей, то есть в этом случае — несколько вариантов реализации геометрии.

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

Классическая теория моделей первого порядка

править

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

Теорема компактности

править

Одним из важнейших инструментов теории моделей является теорема компактности, доказанная Мальцевым, которая утверждает, что множество формул первого порядка имеет модель тогда и только тогда, когда модель имеет каждое конечное подмножество этого множества формул.

Название теоремы связано с тем, что она может быть сформулирована как утверждение о компактности стоуновского пространства[англ.].

Из теоремы компактности следует, что некоторые понятия не являются выразимыми в логике первого порядка. Например, понятия конечности или счётности не могут быть выражены никакими формулами первого порядка и даже их множествами: если множество формул имеет сколь угодно большие конечные модели, то оно имеет и бесконечную модель. Аналогично, теория, имеющая бесконечную модель, мощность которой не меньше мощности сигнатуры, имеет модели и любой большей мощности.

Теорема компактности находит применение для конструирования нестандартных моделей[англ.] классических теорий, например, арифметики[англ.] или математического анализа.

Теории и элементарная эквивалентность

править

Теория   — это замкнутое относительно выводимости (сокращённо, замкнутое) множество формул, то есть, такое множество  , что если формула   следует из  , то   принадлежит  .

Теория, имеющая хотя бы одну модель, называется непротиворечивой, остальные теории — противоречивыми.

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

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

Если полная теория   имеет конечную модель  , то все модели теории   изоморфны  , в частности, все они содержат такое же количество элементов. Следовательно, для конечных алгебраических систем понятия элементарной эквивалентности и изоморфизма совпадают.

Подсистемы и теоремы Лёвенгейма — Скулема

править

Алгебраическая система   называется подсистемой алгебраической системы  , если   и интерпретация каждого сигнатурного символа в   является ограничением его же интерпретации в   на множество  . Подсистема называется элементарной, если для любой формулы   и для любых   выполнено:   тогда и только тогда, когда  . Система   называется в этих случаях (элементарным) расширением системы  .

Элементарная подсистема   элементарно эквивалентна  . Теории, для моделей которых верно и обратное — каждая элементарно эквивалентная подсистема является элементарной — называются модельно полными. Модельная полнота теории   эквивалентна каждому из следующих свойств:

  • любая формула в   эквивалентна экзистенциальной формуле,
  • любая формула в   эквивалентна универсальной формуле,
  • объединение   с диаграммой любой модели порождает полную теорию.

Если   — непустое множество, то среди всех подсистем  , включающих  , существует наименьшая, которая называется порождённой множеством  . Для элементарных подсистем в общем случае такое утверждение неверно.

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

Теорема Лёвенгейма — Скулема «вверх» утверждает, что если   — алгебраическая система мощности не меньше  , то   имеет элементарные расширения любой мощности больше или равной  .

Теорема Лёвенгейма — Скулема «вниз»: если   — алгебраическая система мощности   и  , то   имеет элементарные подсистемы любой мощности между   и  .

Аксиоматизируемость и устойчивость

править

Множество формул   называется множеством аксиом для теории  , если   является множеством следствий  . В частности, сама   является множеством аксиом для себя. Если для теории   существует конечное множество аксиом, то она называется конечно аксиоматизируемой.

Совокупности алгебраических систем называют классами. Класс алгебраических систем   называется аксиоматизируемым, если он является совокупностью моделей некоторой теории  . В этом случае множество аксиом для   называется также множеством аксиом для  . Класс   конечно аксиоматизируем тогда и только тогда, когда аксиоматизируемы сам   и его дополнение.

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

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

Цепью называется множество алгебраических систем, линейно упорядоченное отношением «быть подсистемой». Если для элементов цепи выполняется свойство «быть элементарной подсистемой», то цепь также называется элементарной.

Объединение цепи алгебраических систем даёт новую систему той же сигнатуры, которая будет надсистемой для всех элементов цепи. При объединении элементарной цепи это объединение будет элементарной надсистемой и, следовательно, в нём будет сохраняться истинность всех формул.

При объединении любых цепей (в том числе неэлементарных) сохраняется истинность  -формул, верно и обратное — если формула сохраняет свою истинность при объединении любых цепей, то она эквивалентна некоторой  -формуле.

Теории, которые могут быть аксиоматизируемы посредством  -формул называются индуктивными. Согласно теореме Ченя — Лося — Сушко теория   является индуктивной тогда и только тогда, когда она устойчива относительно объединения цепей. Важный пример индуктивной теории — теория полей фиксированной характеристики.

Метод цепей является одним из важнейших инструментов построения алгебраических систем с нужными свойствами.

Ультрапроизведения

править

Пусть   — язык.   — семейство алгебраических систем,  . Прямым произведением алгебраических систем  ,  , называется алгебраическая система  , где для каждого предикатного символа  

  для каждого  ;

для каждого функционального символа  

 

и для каждого константного символа  

 

Пусть   — фильтр над  . Определим на   отношение  . Введём обозначения:

 ,  

Определим алгебраическую систему   следующим образом.

Положим для предикатного символа  

 

для каждого функционального символа  

 

и для константных символов  

 

Определённая таким образом алгебраическая система   называется фильтрованным произведением систем   по фильтру   и обозначается  . Если   — ультрафильтр, то   называется ультрапроизведением, если все   совпадают и равны  , то   называется ультрастепенью   и обозначается  .

Основное свойство ультрапроизведений состоит в том, что они сохраняют все предложения:

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

 

Также теорему компактности можно сформулировать следующим образом.

Теорема компактности. Если множество формул локально выполнимо в некотором классе  , то оно выполнимо в некотором ультрапроизведении систем из  .[2]

Категоричность

править

Теория   с равенством, имеющая конечную или счётную сигнатуру, называется категоричной в счётной мощности, если все её счётные нормальные модели изоморфны. Категоричность в данной несчётной мощности определяется аналогично.

Теория моделей высших порядков

править

Теория конечных моделей

править

Примечания

править
  1. Кейслер Г., Чен Ч. Теория моделей. — М.: Мир, 1977. — с. 14.
  2. Ершов, 1987, с. 117.

Литература

править
  • Ершов Ю. Л., Палютин Е. А. Математическая логика. — М.: Наука, 1987. — 336 с.
  • Справочная книга по математической логике. Часть 1. Теория моделей / под ред. Дж. Барвайса. — М.: Наука, 1982. — 392 с.
  • Кейслер, Г.Дж.; Чень-Чунь, Чэн. Теория непрерывных моделей. — М.: Мир, 1971. — 184 с.
  • Кейслер, Г.Дж.; Чень-Чунь, Чэн. Теория моделей. — М.: Мир, 1977. — 616 с.