МОДЕЛЕЙ ТЕОРИЯ

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

Наиболее развитой является М. т. формул логики первого порядка. Эти формулы строятся из константных символов (констант), переменных, функциональных и предикатных символов определенной валентности (фиксированную для данной логики или теории совокупность констант, функциональных и предикатных символов называют сигнатурой и иногда языком) стандартным образом, но используются кванторы всеобщности 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'^ded. North-Holland, 1990; (Рус. пер. первого издания:Кейслер Г., Чэн Ч.Ч.Теория моделей. М., 1977);Ebbinghaus H.-D., Flum J.Finite Model Theory. Springer, 1999;Hodges W.Model theory. Cambridge, 1993.