PROFILPELAJAR.COM

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

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

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

Замечания

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

Теорема может рассматриваться как далеко идущее обобщение теоремы Штурма^[1], в связи с чем фигурирует также как обобщённая теорема Штурма. При таком взгляде, теорема Штурма формулируется^[2] как наличие для любого многочлена $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}))

.

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

История

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

Примечания

↑ Е. А. Горин. Об асимптотических свойствах многочленов и алгебраических функций от нескольких переменных // УМН. — 1961. — Т. 16, № 1(97). — С. 91—118. Архивировано 13 мая 2013 года.
↑ ¹ ² Э. Энгелер. Метаматематика элементарной математики. — М.: Мир, 1987. — С. 23—24. — 128 с.
↑ A. Tarski. A Decision Method for Elementary Algebra and Geometry (неопр.). R-109. RAND Corporation (1 августа 1948). Дата обращения: 27 декабря 2018. Архивировано 11 августа 2017 года.
↑ A. Seidenberg. New decision method for elementary algebra (англ.) // Ann. of Math., Ser. 2. — 1954. — Vol. 60. — P. 365—374.
↑ 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…