Просмотр кода страницы Теорема Зайденберга — Тарского

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

Теорема доказана [[Тарский, Альфред|Альфредом Тарским]] в [[1948 год в науке|1948 году]] в статье по [[Разрешимость|разрешимости]] теорий элементарной алгебры и элементарной геометрии.<ref>{{cite web | url = https://www.rand.org/content/dam/rand/pubs/reports/2008/R109.pdf | author = A. Tarski | title = A Decision Method for Elementary Algebra and Geometry | work = R-109 | publisher = [[RAND Corporation]] | date = 1948-08-01 | access-date = 2018-12-27 | archive-date = 2017-08-11 | archive-url = https://web.archive.org/web/20170811135712/https://www.rand.org/content/dam/rand/pubs/reports/2008/R109.pdf | deadlink = no }}</ref>
В [[1954 год в науке|1954 году]] {{iw|Зайденберг, Абрахам|Абрахамом Зайденбергом|en|Abraham Seidenberg}} найден более простой и естественный метод доказательства<ref>{{статья | автор = A. Seidenberg | заглавие = New decision method for elementary algebra | издание = [[Ann. of Math.]], Ser. 2 | том =  60 | год = 1954 | страницы = 365—374 | lang = en}}</ref><ref>{{статья | автор = [[Робинсон, Абрахам|A. Robinson]] | заглавие = Review: A. Seidenberg. A new decision method for elementary algebra. Annals of mathematics, ser. 2 vol. 60 (1954), pp. 365-374. | издание = {{iw|J. Symb. Log}} | том = 22 | номер = 3 | год = 1957 | страница = 295}} <em>…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…</em></ref>.

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

Для всякой формулы <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>; с другой стороны, полуалгебраичность всякой проекции полуалгебраического множества обеспечивает устранимость квантора существования во всякой формуле, и это является единственным нетривиальным моментом в доказательстве теоремы об элиминации кванторов.

*{{Якорь|Обобщённая теорема Штурма}} Теорема может рассматриваться как далеко идущее обобщение [[Ряд Штурма|теоремы Штурма]]<ref>{{статья | автор = [[Горин, Евгений Алексеевич|Е. А. Горин]] | ссылка = http://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=rm&paperid=6566&option_lang=rus | заглавие = Об асимптотических свойствах многочленов и алгебраических функций от нескольких переменных | издание = [[УМН]] | год = 1961 | том = 16 | номер = 1(97) | страницы = 91—118 | archivedate = 2013-05-13 | archiveurl = https://web.archive.org/web/20130513090624/http://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=rm&paperid=6566&option_lang=rus }}</ref>, в связи с чем фигурирует также как '''''обобщённая теорема Штурма'''''. При таком взгляде, теорема Штурма формулируется<ref name="engeler">{{книга | автор = Э. Энгелер | заглавие = Метаматематика элементарной математики | место = М. | издательство = Мир | год = 1987 | страниц = 128 | страницы = 23—24}}</ref> как наличие для любого многочлена <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>.
:Притом если классическое доказательство теоремы Штурма существенно использует техники анализа (в частности, теорему об обращении в нуль непрерывной функции, меняющей знак), то [[математическая логика]] даёт сугубо алгебраическое доказательство факта<ref name="engeler"/>.

== Примечания ==
{{Примечания}}

== Литература ==
* {{книга | автор = [[Верещагин, Николай Константинович|Н. К. Верещагин]], [[Шень, Александр Ханиевич|А. Х. Шень]] | заглавие = Лекции по математической логике и теории алгоритмов | часть = 2. Языки и исчисления | место = М. | издательство = МЦНМО | год = 2012 | страницы = 101—111}}

[[Категория:Теоремы математической логики|Зайденберга]]
[[Категория:Теоремы алгебраической геометрии|Зайденберга]]
[[Категория:Вещественная алгебраическая геометрия]]
[[Категория:Формальные теории арифметики]]