Теория моделей

Теория моделей — это раздел математической логики (см. Логика математическая), изучающий модели формальных теорий, соотношения между моделями и теориями, а также преобразования моделей. Под моделями в математической логике понимаются интерпретации каких-либо логико-математических положений и их систем в контексте логической семантики. Теория моделей возникла как обобщение существующих подходов решения метаматематических проблем, связанных с алгеброй и математической логикой. Сами эти подходы существовали давно, но при этом длительное время не рассматривались во всей своей общности, в рамках единой логической системы. Предшественниками теории моделей были Б. Больцано и Э. Шрёдер, осознавшие понятие выполнимости формулы на интерпретации. Основное развитие теория моделей получила в работах А. Тарского, А. И. Мальцева и А. Робинсона. Название «теория моделей» было впервые предложено А. Тарским в 1954 году.

В настоящее время теория моделей делится на следующие разделы:

1. Классическая теория моделей, изучающая теоретико-множественные модели классических теорий.
2. Алгебраическая теория моделей, изучающая прежде всего модели неклассических логик (см. Логики неклассические), базирующиеся на обобщённой семантике истинностных значений.
3. Теория моделей С. Крипке, изучающая модели неклассических логик, базирующиеся на семантике возможных миров (см. Семантика возможных миров).
4. Интерпретации реализуемости, моделирующие логики и теории как исчисления задач.

Классическая теория моделей берёт своё начало от работ Л. Лёвенгейма (1915) и Т. Скулема (1920), установивших существование моделей любой бесконечной мощности для любой непротиворечивой теории, имеющей бесконечную модель. Этот результат вначале рассматривался как парадоксальный, потому что из него следовало существование счётных моделей несчётных множеств, а мощность множества в те времена содержательно интерпретировали как число элементов, по аналогии с конечными множествами, а не как сложность его задания, как сейчас делается по аналогии с теорией алгоритмов. Фундаментальным результатом классической теория моделей стала теорема К. Гёделя о полноте классической логики предикатов (первого порядка), из которой следует существование моделей у любых (основанных на этой логике) непротиворечивых теорий. В 1970-е годы выяснилось, что теорема Гёделя о полноте эквивалентна аксиоме выбора теории множеств.

Если задана некоторая сигнатура (перечисление констант, функциональных символов и предикатов вместе с числом аргументов у них), то (классической) интерпретацией данной сигнатуры является непустое множество объектов — универсум интерпретации, и функция вычисления значения ζ, сопоставляющая каждой константе — элемент универсума, n-местной функции f — функционал Uⁿ → U, n-местному предикату Ρ — функционал Uⁿ → {0, 1}. В интерпретации естественно определяется понятие значения любого терма и любой формулы теории (точное определение истинности формулы в интерпретации было впервые дано А. Тарским). Интерпретация называется моделью теории, если в ней истинны все аксиомы теории. Ещё одной формулировкой теоремы полноты Гёделя является совпадение множества теорем с множеством формул, истинных в любой модели теории.

Согласно теореме А. И. Мальцева о компактности, теория имеет модель тогда, и только тогда, когда любое конечное число её аксиом имеет модель. Эта теорема послужила основой для построения нестандартных моделей традиционных математических объектов, таких, как действительные и натуральные числа. В самом деле, взяв в качестве теории все истинные на стандартной модели формулы и добавив новое число ω и бесконечную совокупность аксиом ω> 0, ω> 1, ω > n, мы получаем, что любая конечная совокупность новых аксиом удовлетворяется на стандартной модели. Значит, есть и модель, где они все выполнены. Она сохраняет все выразимые на языке логики предикатов свойства стандартной модели, но пополнена новыми элементами.

Позитивно использовал существование нестандартных моделей А. Робинсон (1960). Он показал, что в нестандартной модели анализа можно на строгой основе возродить методы математиков XVII–XVIII веков, использовавших бесконечно малые и бесконечно большие величины. Основополагающим явился здесь результат, что любое конечное нестандартное число однозначно разлагается в сумму стандартного и бесконечно малого. Далее, сохранение всех выразимых свойств используется для установления принципов переноса, которые позволяют отбрасывать бесконечно малые либо доказывать общее утверждение о стандартных числах на основе рассмотрения одной бесконечно малой либо бесконечно большой величины. Но здесь приходится строго разделять формулы стандартного языка и формулы метаязыка, говорящего о нестандартной модели. В частности, утверждения, явно включающие предикат «быть [не] стандартным», уже могут нарушать все свойства стандартной модели. Дальнейшее развитие нестандартного анализа привело к теории полумножеств Г. Хаека и к альтернативной теории множеств С. Вопенки, где конечные нестандартные совокупности могут включать бесконечные подклассы.

Современная классическая теория моделей развивается во многих направлениях, большинство из которых в данный момент имеют дело со сложнейшими идеальными математическими понятиями (абстрактными объектами) без выхода на общенаучные либо методологические результаты. Определённым исключением здесь является совокупность теорем, характеризующих теории частного вида через их модели.

Алгебраическая теория моделей берёт своё начало от предложенной А. Линденбаумом и А. Тарским концепции, согласно которой любая теория может рассматриваться как алгебра, операциями которой являются логические связки, а объектами — классы формул, для которых доказуема эквивалентность. Такая алгебра называется алгеброй Линденбаума — Тарского (ЛТ-алгеброй) теории. ЛТ-алгебра классической теории — это булева алгебра. ЛТ-алгебра интуиционистской теории — это псевдобулева алгебра, теории в модальной логике S4 — это булева алгебра с замыканиями. Данный подход был вторым основанием и инструментом для построения альтернативной теории множеств. Для неклассических логик он математически эквивалентен семантике возможных миров и поэтому в последнее время употребляется менее интенсивно. Известной трудностью в алгебраической теории моделей является интерпретация кванторов. Для данной цели была развита теория цилиндрических алгебр.

Семантика возможных миров предлагалась уже Аристотелем, который рассматривал теорию модальных суждений. Её предшественником можно считать Г. В. Лейбница, который явно ввёл понятие возможного мира. В современном виде она впервые была предложена для частного случая интуиционистской логики Э. Бетом (1954) и последовательно развита для целого ряда логик С. Крипке, имя которого она и получила. При интерпретациях в семантике возможных миров имеется некоторая алгебраическая система классических (либо, в более тонких случаях, алгебраических) моделей, называемых мирами, связанных отношениями и порой функциями. Для модальных логик интерпретации в семантике возможных миров обычно используют единственное бинарное отношение достижимости. Логика L называется шкальной, если любая интерпретация с той же системой миров, что у модели L, также является моделью L. Таким образом, шкальные логики накладывают ограничения не на отдельные миры, а на их внешние взаимосвязи. Один из наиболее интересных результатов современной семантики возможных миров — перечисление всех суперинтуиционистских и модальных пропозициональных логик, обладающих интерполяционным свойством Крейга: для любой доказуемой импликации A ⇒ B найдётся формула C, содержащая лишь термины, общие для A и B, такая, что доказуемы A ⇒ C и C ⇒ B. В работах Л. Л. Максимовой показано, что логик, обладающих свойством Крейга, конечное число. Математическая структура вынуждения, использованная П. Дж. Коэном как промежуточный шаг для построения нестандартных классических моделей теоретико-множественных систем, позднее получила название моделей Крипке для интуиционистской логики. С их помощью решена проблема Гилберта: доказана независимость аксиомы выбора и континуум-гипотезы. Далее, теми же методами установлена невозможность явного построения, в частности, неизмеримого множества действительных чисел и нестандартной модели анализа. Исторически это было одно из первых применений семантики возможных миров.

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