2016/07/19 by Grzegorz Pastuszak, Pastuszak, Grzegorz
Computer Science · Mathematics · #Advanced Topology and Set Theory #Algebraic Geometry and Number Theory #FOS: Mathematics #FOS: Physical sciences #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Mathematical Physics (math-ph) #Polynomial and algebraic computation
paper · pdf · doi:10.48550/arxiv.1607.05505
openalex publication_date 2016/07/19 · openalex created_date 2022/09/05 · openalex updated_date 2026/07/28
Assume that ACF denotes the theory of algebraically closed fields. The renowned theorem of A. Tarski states that ACF admits quantifier elimination. In this paper we give a constructive proof of Tarski's theorem on quantifier elimination in ACF. This means that for a given formula φ of the language of fields we construct a quantifier-free formula φ' such that ACF\vdashφ↔φ'. We devote the last section of the paper to show some applications of this constructive version in mathematics and physics.