WikiSort.ru - Не сортированное

Теорема Зайденберга — Тарского — утверждение о возможности элиминации кванторов в элементарной теории^[en] вещественных чисел со сложением и умножением (замкнутых вещественных полей^[en]), и как следствие, разрешимости этой теории. Формально: для всякой формулы ${\displaystyle \varphi }$ в сигнатуре, содержащей двуместные предикаты ${\displaystyle =}$ и ${\displaystyle <}$ , константы ${\displaystyle 0}$ и ${\displaystyle 1}$ и двуместные операции ${\displaystyle +}$ и ${\displaystyle \times }$ , существует бескванторная формула ${\displaystyle \psi }$ , эквивалентная ей на множестве вещественных чисел ${\displaystyle \mathbb {R} }$ . Впервые была доказана Тарским в 1948 году в труде по разрешимости теорий элементарной алгебры и элементарной геометрии^[1], в 1954 году Зайденбергом^[en] найден более простой и естественный метод доказательства^[2][3].

Эквивалентное утверждение теоремы — полуалгебраичность проекций полуалгебраического множества: так как проекция полуалгебраического множества ${\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].

Примечания

Литература

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