A constructive proof of Tarski's theorem on quantifier elimination in   the theory of ACF

Grzegorz Pastuszak

arXiv:1607.05505·math.LO·July 20, 2016

A constructive proof of Tarski's theorem on quantifier elimination in the theory of ACF

Grzegorz Pastuszak

PDF

Open Access

TL;DR

This paper provides a constructive proof of Tarski's theorem on quantifier elimination in the theory of algebraically closed fields, enabling explicit construction of equivalent quantifier-free formulas.

Contribution

It offers a constructive method for quantifier elimination in ACF, unlike previous non-constructive proofs, with applications in mathematics and physics.

Findings

01

Constructive procedure for quantifier elimination in ACF

02

Explicit formulas for logical equivalences in algebraically closed fields

03

Applications demonstrated in mathematical and physical contexts

Abstract

Assume that $A C F$ denotes the theory of algebraically closed fields. The renowned theorem of A. Tarski states that $A C F$ admits quantifier elimination. In this paper we give a constructive proof of Tarski's theorem on quantifier elimination in $A C F$ . This means that for a given formula $φ$ of the language of fields we construct a quantifier-free formula $φ^{'}$ such that $A C F ⊢ φ \leftrightarrow φ^{'}$ . We devote the last section of the paper to show some applications of this constructive version in mathematics and physics.

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsAlgebraic Geometry and Number Theory · Polynomial and algebraic computation · Homotopy and Cohomology in Algebraic Topology