Теорема Фефермана–Воота

Теорема Фефермана–Воота ^[1] в теории моделей — теорема Соломона Фефермана и Роберта Лоусона Воота , показывающая , как алгоритмическим способом свести теорию первого порядка произведения структур к теории первого порядка элементов структуры.

Теорема считается одним из стандартных результатов в теории моделей. ^{[2] [3] [4]} Теорема расширяет предыдущий результат Анджея Мостовского о прямых произведениях теорий. ^[5] Она обобщает (на формулы с произвольными кванторами) свойство универсальной алгебры, согласно которому равенства (тождества) переносятся на прямые произведения алгебраических структур (что является следствием одного из направлений теоремы Биркгофа ).

Рассмотрим логическую сигнатуру первого порядка L. Определение структур произведений берет семейство L -структур для некоторого набора индексов I и определяет структуру произведений , которая также является L -структурой, со всеми функциями и отношениями, определенными поточечно.${\displaystyle \mathbf {A} _{i}}$${\displaystyle я\в я}$${\displaystyle \mathbf {A} =\prod _{i\in I}\mathbf {A} _{i}}$

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

Если — символ отношения с аргументами в L и — элементы декартова произведения , то мы определяем интерпретацию в следующим образом:${\displaystyle r(a_{1},\ldots ,a_{p})}$${\displaystyle p}$${\displaystyle a_{1},\ldots ,a_{n}\in \Pi _{i\in I}\mathbf {A} _{i}}$${\displaystyle r}$${\displaystyle \mathbf {A} }$

${\displaystyle \mathbf {A} \models r(a_{1},\ldots ,a_{p})\ifl \forall i\in I,\ \mathbf {A} _{i}\models r(a_{1}(i),\ldots ,a_{p}(i))}$

Когда — функциональное отношение, это определение сводится к определению прямого произведения в универсальной алгебре .${\displaystyle r}$

Для формулы первого порядка в сигнатуре L со свободными переменными и для интерпретации переменных мы определяем множество индексов, для которых выполняется в${\displaystyle \phi ({\bar {x}})}$${\displaystyle {\bar {a}}}$${\displaystyle {\bar {x}}}$${\displaystyle я}$${\displaystyle \phi ({\bar {a}})}$${\displaystyle \mathbf {A} _{i}}$

${\displaystyle ||\phi ({\bar {a}})||=\{i\mid \mathbf {A} _{i}\models \phi ({\bar {a}}(i))\}}$

Для данной формулы первого порядка со свободными переменными существует алгоритм для вычисления ее эквивалентной игровой нормальной формы, которая представляет собой конечную дизъюнкцию взаимно противоречащих формул.${\displaystyle \phi ({\bar {x}})}$${\displaystyle \bigvee _{i=0}^{k-1}\theta ({\bar {x}})}$

Теорема Фефермана–Воота дает алгоритм , который берет формулу первого порядка и строит формулу , которая сводит условие, которое выполняется в произведении, к условию, которое выполняется в интерпретации наборов индексов:${\displaystyle \phi ({\bar {x}})}$${\displaystyle \фи ^{*}}$${\displaystyle \phi ({\bar {a}})}$${\displaystyle \фи ^{*}}$${\displaystyle к+1}$

${\displaystyle I,||\theta _{0}({\bar {a}})||,\ldots,||\theta _{k-1}({\bar {a}})||}$

Таким образом, формула представляет собой формулу со свободным множеством переменных, например, в теории первого порядка булевой алгебры множеств.${\displaystyle \фи ^{*}}$${\displaystyle к+1}$

Формула может быть построена по структуре исходной формулы . Когда квантор свободен, то по определению прямого произведения выше следует${\displaystyle \фи ^{*}}$${\displaystyle \фи ^{*}}$${\displaystyle \фи}$

${\displaystyle {\begin{array}{rl}\mathbf {A} \models \phi ({\bar {a}})&\ifl \forall i\in I.\ \mathbf {A} _{i}\models \phi ({\bar {a}}(i))\\&\ifl \{i\mid \mathbf {A} _{i}\models \phi ({\bar {a}}(i))\}=I\\&\ifl ||\phi ({\bar {a}})||=I\end{array}}}$

Следовательно, мы можем принять за равенство на языке булевой алгебры множеств (эквивалентно, поля множеств ).${\displaystyle \phi ^{*}(U,X_{1})}$${\displaystyle U=X_{1}}$

Распространение условия на квантифицированные формулы можно рассматривать как форму исключения квантификаторов , где квантификация по элементам произведения сводится к квантификации по подмножествам .${\displaystyle {\bar {a}}}$${\displaystyle \фи}$${\displaystyle Я}$

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

Примером может служить подструктура элементов продукта, которые являются постоянными во всех, кроме конечного числа индексов. Предположим, что язык L содержит постоянный символ , и рассмотрим подструктуру, содержащую только те элементы продукта, для которых множество${\displaystyle с}$${\displaystyle а}$

${\displaystyle \{i\mid {\textbf {A}}_{i}\models a(i)\neq c\}}$

конечна. Теорема затем сводит истинностное значение в такой подструктуре к формуле в булевой алгебре множеств, где некоторые множества ограничены быть конечными.${\displaystyle \фи ^{*}}$

Один из способов определения обобщенных произведений — рассмотреть те подструктуры, в которых множества принадлежат некоторой булевой алгебре множеств индексов (подмножеству алгебры множеств powerset ), и где подструктура произведения допускает склеивание. ^[6] Здесь допускающее склеивание относится к следующему условию замыкания: если — два элемента произведения и — элемент булевой алгебры, то таковым является и элемент, определяемый «склеиванием» и согласно :${\displaystyle ||\фи (а)||}$${\displaystyle Б}$${\displaystyle X\subseteq I}$${\displaystyle 2^{Я}}$${\displaystyle а,б}$${\displaystyle X\in B}$${\displaystyle с}$${\displaystyle а}$${\displaystyle б}$${\displaystyle X}$

${\displaystyle c(i)=\left\{{\begin{array}{rl}a(i),&{\mbox{ if }}i\in X\\b(i),&{\mbox{ if }}i\in (I\setminus X)\end{array}}\right.}$

Теорема Фефермана–Воота подразумевает разрешимость арифметики Скулема , рассматривая, посредством основной теоремы арифметики , структуру натуральных чисел с умножением как обобщенное произведение (степень) арифметических структур Пресбургера.

Имея ультрафильтр на множестве индексов , мы можем определить структуру факторизации на элементах произведения, что приводит к теореме Ежи Лося , которую можно использовать для построения гипердействительных чисел .${\displaystyle I}$