Русская Википедия:Теорема Зайденберга — Тарского
Теорема Зайденберга — Тарского — утверждение о возможности элиминации кванторов в Шаблон:Iw вещественных чисел со сложением и умножением (Шаблон:Iw), и как следствие, разрешимости этой теории.
Формулировка
Для всякой формулы <math>\varphi</math> в сигнатуре, содержащей двуместные предикаты <math>=</math> и <math><</math>, константы <math>0</math> и <math>1</math> и двуместные операции <math>+</math> и <math>\times</math>, существует бескванторная формула <math>\psi</math>, эквивалентная ей на множестве вещественных чисел <math>\R</math>.
Замечания
- Эквивалентное утверждение: полуалгебраичность проекций полуалгебраического множества: так как проекция полуалгебраического множества <math>A\subset \R^{n+1}</math> вдоль одной из осей добавляет в определяющую систему квантор существования, который можно элиминировать, результатом её будет полуалгебраическое множество в <math>\R^n</math>; с другой стороны, полуалгебраичность всякой проекции полуалгебраического множества обеспечивает устранимость квантора существования во всякой формуле, и это является единственным нетривиальным моментом в доказательстве теоремы об элиминации кванторов.
- Теорема может рассматриваться как далеко идущее обобщение теоремы Штурма[1], в связи с чем фигурирует также как обобщённая теорема Штурма. При таком взгляде, теорема Штурма формулируется[2] как наличие для любого многочлена <math>p (x, x_1, \dots, x_n)</math> бескванторной формулы <math>\psi(x_1, \dots, x_n, a, b)</math> такой, что из аксиом замкнутого вещественного поля следует эквивалентность:
- <math>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)</math>;
- формулировка же теоремы Зайденберга — Тарского в этом случае — переход от произвольной бескванторной формулы <math>\varphi(x, x_1, \dots, x_n)</math>, ограниченной квантором существования, к бескванторной формуле <math>\psi(x_1, \dots, x_n, a, b)</math>:
- <math>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))</math>.
- Притом если классическое доказательство теоремы Штурма существенно использует техники анализа (в частности, теорему об обращении в нуль непрерывной функции, меняющей знак), то математическая логика даёт сугубо алгебраическое доказательство факта[2].
История
Доказана Тарским в 1948 году в статье по разрешимости теорий элементарной алгебры и элементарной геометрии.[3] В 1954 году Шаблон:Iw найден более простой и естественный метод доказательства[4][5].
Примечания
Литература
- ↑ Шаблон:Статья
- ↑ 2,0 2,1 Шаблон:Книга
- ↑ Шаблон:Cite web
- ↑ Шаблон:Статья
- ↑ Шаблон:Статья …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…
