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

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

Теорема доказана Альфредом Тарским в 1948 году в статье по разрешимости теорий элементарной алгебры и элементарной геометрии.[1] В 1954 году Абрахамом Зайденбергом^[англ.] найден более простой и естественный метод доказательства[2][3].

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

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

Замечания

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

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

${\displaystyle 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)}$;

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

${\displaystyle 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}))}$.

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

Примечания

1. A. Tarski. A Decision Method for Elementary Algebra and Geometry  (неопр.). R-109. RAND Corporation (1 августа 1948). Дата обращения: 27 декабря 2018. Архивировано 11 августа 2017 года.
2. A. Seidenberg. New decision method for elementary algebra (англ.) // Ann. of Math., Ser. 2. — 1954. — Vol. 60. — P. 365—374.
3. A. Robinson. Review: A. Seidenberg. A new decision method for elementary algebra. Annals of mathematics, ser. 2 vol. 60 (1954), pp. 365-374. // J. Symb. Log^[англ.]. — 1957. — Т. 22, № 3. …This elegantly written paper contains an alternative to Tarski’s decision method for “elementary algebra,” i.e., for sentences formulated in the lower predicate calculus with reference to a real-closed field (XIV 188). Like Tarski’s, the method described here depends on the elimination of quantifiers. In the present instance this amounts to a generalization of Sturm’s theorem as follows…
4. Е. А. Горин. Об асимптотических свойствах многочленов и алгебраических функций от нескольких переменных // УМН. — 1961. — Т. 16, № 1(97). — С. 91—118. Архивировано 13 мая 2013 года.
5. Э. Энгелер. Метаматематика элементарной математики. — М.: Мир, 1987. — С. 23—24. — 128 с.

Литература

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