Теорема Зайденберга — Тарского — общее утверждение, которое в частности даёт алгоритм для решения любой задачи элементарной геометрии (точнее, в элементарной теории Евклидовой геометрии). Формально говоря, это утверждение о возможности элиминации кванторов в элементарной теории вещественных чисел, и как следствие, разрешимости этой теории.
Теорема доказана Альфредом Тарским в 1948 году в статье по разрешимости теорий элементарной алгебры и элементарной геометрии. В 1954 году найден более простой и естественный метод доказательства …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….
Формулировка
Для всякой формулы в сигнатуре, содержащей двуместные предикаты и , константы и и двуместные операции и , существует бескванторная формула , эквивалентная ей на множестве вещественных чисел .
Замечания
Эквивалентное утверждение: полуалгебраичность проекций полуалгебраического множества: так как проекция полуалгебраического множества вдоль одной из осей добавляет в определяющую систему квантор существования, который можно элиминировать, результатом её будет полуалгебраическое множество в ; с другой стороны, полуалгебраичность всякой проекции полуалгебраического множества обеспечивает устранимость квантора существования во всякой формуле, и это является единственным нетривиальным моментом в доказательстве теоремы об элиминации кванторов.
Теорема может рассматриваться как далеко идущее обобщение теоремы Штурма, в связи с чем фигурирует также как обобщённая теорема Штурма. При таком взгляде, теорема Штурма формулируется как наличие для любого многочлена бескванторной формулы такой, что из аксиом замкнутого вещественного поля следует эквивалентность: ; формулировка же теоремы Зайденберга — Тарского в этом случае — переход от произвольной бескванторной формулы , ограниченной квантором существования, к бескванторной формуле : . Притом если классическое доказательство теоремы Штурма существенно использует техники анализа (в частности, теорему об обращении в нуль непрерывной функции, меняющей знак), то математическая логика даёт сугубо алгебраическое доказательство факта.
Примечания
Литература
Зайденберга Зайденберга Категория:Вещественная алгебраическая геометрия Категория:Формальные теории арифметики