A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals

Abstract. In the FTA project in Nijmegen we have formalized a constructive proof of the Fundamental Theorem of Algebra. In the formalization, we have first defined the (constructive) algebraic hierarchy of groups, rings, fields, etcetera. For the reals we have then defined the notion of real number structure, which is basically a Cauchy complete Archimedean ordered field. This boils down to axiomatizing the constructive reals. The proof of FTA is then given from these axioms (so independent of a specific construction of the reals), where the complex numbers are defined as pairs of real numbers. The proof of FTA that we have chosen to formalize is the one in the seminal book by Troelstra and van Dalen [17], originally due to Manfred Kneser [12]. The proof by Troelstra and van Dalen makes heavy use of the rational numbers (as suitable approximations of reals), which is quite common in constructive analysis, because equality on the rationals is decidable and equality on the reals isn'...

• Type: Conference
• Year: 2000
• Where: TYPES
• Authors: Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
• Keywords: Constructive Proof, Constructive Reals, Formal Methods, Reals, TYPES 2000