Sciweavers

Share
TYPES
2000
Springer

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

9 years 2 months ago
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'...
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where TYPES
Authors Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
Comments (0)
books