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

МОДЕЛЕЙ ТЕОРИЯ — раздел математической логики, в котором изучаются фундаментальные связи между синтаксическими свойствами предложений формального языка и семантическими свойствами их моделей.

Наиболее развитой является М. т. формул логики первого порядка. Эти формулы строятся из константных символов (констант), переменных, функциональных и предикатных символов определенной валентности (фиксированную для данной логики или теории совокупность констант, функциональных и предикатных символов называют сигнатурой и иногда языком) стандартным образом, но используются кванторы всеобщности Vx, Vj,... и существования Зх, Зу,... только по предметным переменными,..., т.е. х,у,... —переменные, областью изменения которых является предметная область подразумеваемой модели. Термом называют выражение, построенное из переменных и констант с помощью функциональных символов; понятие терма соответствует понятию математического выражения, пример терма — выражение 2х³+Зху-4. Моделью для этих формул (моделью языка, алгебраической системой для данной сигнатуры, в последнем случае моделью называют алгебраическую систему без функций, а алгебраическую систему без предикатов, за исключением предиката равенства, т.е. совпадения, называют (универсальной) алгеброй) называется непустое множество М (носитель модели; сама модель часто обозначается той же буквой М), в котором каждому константному символу сопоставлен некоторый элемент, каждому функциональному символу валентности п — и-местная функция, каждому предикатному символу валентности и — и-местный предикат (как функция, действующая из Мх...хМ (п сомножителей) во множество {истина, ложь} или {1, 0} в иных обозначениях); обозначения предикатов и функций в модели часто такие же, как и символов, которым они сопоставляются. Истинность формулы в (на) модели (на алгебраической системе) определяется с помощью введения интерпретации свободных переменных, т.е. функции, сопоставляющей всякой переменной некоторый элемент носителя, а далее — индукция по построению формулы: значение элементарной формулы Р(г_р...,tj (здесь Р — предикатный символ валентности и, t_p...,t_n термы) получается вычислением значений аргументов в соответствии со значениями констант в М, значениями переменных в соответствии с их интерпретацией и функциями, сопоставленными функциональным символам, а затем вычислением значением предиката, сопоставленного в М предикатному символу Р, от получившихся значений £,>•".£,,; в индукционном шаге используются классические таблицы истинности для булевых пропозициональных связок и следующие правила для формул, начинающихся с кванторов: формула Ухф считается истинной в М при данной интерпретации переменных, если ф истинна в М при любой интерпретации переменных, отличающейся от данной разве что значением х; формула Зхф считается истинной в М при данной интерпретации переменных, если ф истинна в М при некоторой интерпретации переменных, отличающейся от данной разве что значением х. Формула считается истинной в модели, если она истинная в ней при любой интерпретации переменных. Модель называется моделью множества формул Ф, если в этой модели истинны все формулы из Ф. По всякому множеству моделей X определяется совокупность формул Т(Х), истинных во всех этих моделях, которая называется (элементарной, первопорядковой) теорией этого множества; по всякому множеству формул Ф определяется совокупность моделей Е(Ф), в которых истинны все формулы из Ф. В соответствии с теоремой Геделя о полноте для всякой совокупности моделей X справедливо Т(Е(Т(Х))) = Г(Х) и для всякого множества формул Ф справедливо Е(Т(Е(Ф))) = Е(Ф). Истинность формулы в модели эквивалентна истинности ее универсального замыкания (результата приписывания к формуле кванторов всеобщности по всем свободным переменным), поэтому во многих случаях достаточно рассматривать предложения, т.е. замкнутые формулы (формулы без свободных переменных). Фундаментальными достижениями М. т. логики первого порядка являются: теорема Левенгейма—Сколема (усиленный вариант известен как теорема Левенгейма—Скулема—Тарского) — всякое счетное или конечное множество предложений, имеющих модель, имеет и счетную модель; теорема Мальцева о компактности — если всякое конечное подмножество данного множества предложений имеет модель, то и все множество имеет модель; теорема Геделя о полноте — всякое непротиворечивое множество предложений имеет модель. М. т. логики первого порядка, помимо своих внутренних проблем, помогла решить и/или упростить известные решения многих математических проблем. Примеры: многочисленные локальные теоремы в алгебре, единообразно доказанные А.И. Мальцевым и до этого либо имевшие (порой довольно громоздкие) доказательства, учитывающие специфику конкретных видов алгебраических систем, либо являвшиеся открытыми проблемами; построение А. Робинсоном так называемого нестандартного анализа, являющегося, по сути, строгим обоснованием анализа бесконечно малых, предложенного Г. Лейбницем, причем нестандартный анализ явился не только удобным способом изложения обычного математического анализа и родственных ему дисциплин, но и инструментом доказательства новых теорем. Несмотря на большую применимость формул логики первого порядка и наличие мощного теоретико-модельного инструментария, многие свойства, привычные для применения, оказываются невыразимыми с помощью этих формул. Таковы, напр., свойство конечности произвольной модели для данной сигнатуры, свойство счетности, свойство континуальности модели. Средствами логики первого порядка невозможно описать с точностью до изоморфизма натуральный ряд (совокупность натуральных чисел с обычным порядком). Невозможными для описания оказываются и многие конструкции, широко применяемые в теоретических исследованиях в компьютерных науках; пример: невозможно в виде каких-либо формул первого порядка или их совокупностей записать, что бинарное отношение R₁ является транзитивным замыканием бинарного отношения R_r

В формулах второго порядка кроме кванторов по предметным переменным допускаются кванторы по предикатам и функциям. Модели формул второго и более высоких порядков определяются аналогично сказанному выше, но в случае использования, допустим, переменных по предикатам, соответствующие предикатные буквы в модели не имеют фиксированной интерпретации, а при определении истинности формул в модели используется интерпретация не только предметных переменных, но и по предикатным и функциональным переменным. Соответственно, дополняется определение истинности формул таким, напр., индукционным пунктом: формула /Рф считается истинной в модели М при данной интерпретации (всех!) переменных, если ф истинна в М при любой интерпретации переменных, отличающейся от данной разве что значением предикатной переменной Р. Все перечисленные свойства, не выразимые в логике первого порядка, выразимы в логике второго порядка. Такая большая выразительность имеет и отрицательные черты: фактически М. т. логики второго порядка является вариантом теории множеств со всеми привнесенными ее проблемами; в частности, эта теория не имеет эффективной аксиоматизации.

С 60-х гг. 20 в. развиваются различные направления М. т., целью которых является учет требований повышения выразительных возможностей используемого языка, снижения неэффективности, а также возникшей в те годы и активно прогрессирующей компьютерно-информационной реальности. Так возникла абстрактная М. т. и доказано, что она, по существу, является М. т. логики первого порядка в точности тогда, когда в ней справедливы теорема Левенгейма—Сколема и теорема компактности. Наиболее важными из новых направлений являются: а) теория рекурсивных (алгоритмически описываемых) моделей и родственная ей теория конструктивных моделей, теория конечных моделей как теория с дополнительными условиями, накладываемыми на модели; б) теория моделей логических языков с обобщенными кванторами и бесконечными конъюнкциями и дизъюнкциями, теория моделей ограниченных языков второго порядка, напр. слабых языков второго порядка (квантификация по конечным множествам), пропозициональных языков с неклассическими логическими операторами (неклассические, в частности — модальные, логики) и кванторами по пропозициональным переменным, и многих др.

А.В. Чагров

Лит.: Булос Дж., Джеффри Р. Вычислимость и логика. М., 1994; Гончаров С.С., Ершов Ю.Л. Конструктивные модели. Новосибирск, 1999; Мальцев AM. Алгебраические системы. М., 1970; Робинсон А. Введение в теорию моделей и метаматематику алгебры. М., 1967; Справочная книга по математической логике.Ч. I. Теория моделей. М., 1982; Chang С.С, KeislerH.J. Model Theory. 3'^d ed. North-Holland, 1990; (Рус. пер. первого издания: Кейслер Г., Чэн Ч.Ч. Теория моделей. М., 1977); Ebbinghaus H.-D., Flum J. Finite Model Theory. Springer, 1999; Hodges W. Model theory. Cambridge, 1993.