Теорема Зайденберга — Тарского

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

Формулировка

Для всякой формулы $\varphi$ в сигнатуре, содержащей двуместные предикаты $=$ и $<$, константы $0$ и $1$ и двуместные операции $+$ и $\times$, существует бескванторная формула $\psi$, эквивалентная ей на множестве вещественных чисел $\mathbb {R}$.

Замечания

• Эквивалентное утверждение: полуалгебраичность проекций полуалгебраического множества: так как проекция полуалгебраического множества $A\subset \mathbb {R} ^{n+1}$ вдоль одной из осей добавляет в определяющую систему квантор существования, который можно элиминировать, результатом её будет полуалгебраическое множество в $\mathbb {R} ^{n}$; с другой стороны, полуалгебраичность всякой проекции полуалгебраического множества обеспечивает устранимость квантора существования во всякой формуле, и это является единственным нетривиальным моментом в доказательстве теоремы об элиминации кванторов.

• Теорема может рассматриваться как далеко идущее обобщение теоремы Штурма, в связи с чем фигурирует также как обобщённая теорема Штурма. При таком взгляде, теорема Штурма формулируется как наличие для любого многочлена $p(x,x_{1},\dots ,x_{n})$ бескванторной формулы $\psi (x_{1},\dots ,x_{n},a,b)$ такой, что из аксиом замкнутого вещественного поля следует эквивалентность:

$a<b\Rightarrow \psi (x_{1},\dots ,x_{n},a,b)\equiv \exists x(a<x<b\land p(x,x_{1},\dots ,x_{n})=0)$;

формулировка же теоремы Зайденберга — Тарского в этом случае — переход от произвольной бескванторной формулы $\varphi (x,x_{1},\dots ,x_{n})$, ограниченной квантором существования, к бескванторной формуле $\psi (x_{1},\dots ,x_{n},a,b)$:

$a<b\Rightarrow \psi (x_{1},\dots ,x_{n},a,b)\equiv \exists x(a<x<b\land \varphi (x,x_{1},\dots ,x_{n}))$.

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

История

Доказана Тарским в 1948 году в статье по разрешимости теорий элементарной алгебры и элементарной геометрии. В 1954 году Абрахамом Зайденбергом найден более простой и естественный метод доказательства.

Литература

• Н. К. Верещагин, А. Х. Шень. 2. Языки и исчисления // Лекции по математической логике и теории алгоритмов. — М.: МЦНМО, 2012. — С. 101—111.