代数基本定理证明方法研究外文翻译资料

A Constructive Proof of the Fundamental

Theorem of Algebra without Using the Rationals

Herman Geuvers, Freek Wiedijk, and Jan Zwanenburg

Department of Computer Science, University of Nijmegen, The Netherlands

{herman,freek,janz}@cs.kun.nl

Abstract：In the FTA project in Nijmegen we have formalised a constructive proof of the Fundamental Theorem of Algebra. In the formal isation, 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 axiomatising 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 formalise is the one in theseminal 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 isnrsquo;t. In our case, this is not so convenient, because the axiomatisation of the reals doesnrsquo;t lsquo;containrsquo; the rationals. Moreover, we found it rather unnatural to let a proof about the reals be mainly dealing with rationals. Therefore, our version of the FTA proof doesnrsquo;t refer to the rational numbers. The proof described here is a faithful presentation of a fully formalised proof in the Coq system.

1 Introduction

The Fundamental Theorem of Algebra states that the field of complex numbers

is algebraically closed. More explicitly, it says that

For every non-constant polynomial

With coefficients in , the equation has a solution.

This theorem has a long and illustrious history (see [6] or [11] for an overview). It was proved for the first time in Gaussrsquo;s Ph.D. thesis from 1799. Many proofs of the Fundamental Theorem of Algebra are known, most of which have a constructive version of the simple proof that derives a contradiction from the assumption that the (non-constant) polynomial is minimal at with . We briefly repeat the classical proof here. Let be a non-constant polynomial.

First note that must have a minimum somewhere, because if

. We may assume the minimum to be reached for . Now, assume the minimum of is not 0. The function has the form

with . Because of this, and we can take

with , and if is small enough, the part will be negligible compared to the rest, and we get a for which

So is not the minimum and we have and we have derived a contradiction.

By iterating this idea, one can try to construct a Cauchy sequence to a zero of the polynomial. The main difficulty with this approach is that we have two conflicting requirements for the choice of.

If is chosen too small each time, we may not reach the zero in countably many steps (we will go down, but might not go down all the way to zero).

If is not small enough, we are not allowed to ignore the part.

The solution to this is that, instead of using the above representation (in which the term is the smallest power with a non-zero coefficient), in the constructive proof one just takes some appropriate (not necessarily the smallest) and writes as

That way one can make sure that not only , but in fact for some fixed .

For every non-constant polynomial

With coefficients in , such that for some , the equation has a solution.

As the equality on (and therefore on ) is not decidable we canrsquo;t just write as with . Therefore, in constructive analysis, one works with the notion of apartness, usually denoted by #, which is a lsquo;positive inequalityrsquo;: if we positively know them to be distinct, i.e. we know a distance between them.

Now, one can constructively find a root of if we positively know some coefficient to be distinct from 0. The proof of constructive FTA proceeds by first proving it for monic polynomials (i.e. where ).

The original Kneser proof of FTA for monic polynomials makes use of an approximation of the polynomial with coefficients in Q, because it needs to compare the size of various expressions (which is not decidable in R). We found this unsatisfactory: the rational numbers donrsquo;t seem to have anything to do with the Fundamental Theorem of Algebra! Also, in our Coq formalisation of Kneserrsquo;s proof, we introduced the real numbers axiomatically (so a priori we didnrsquo;t have Q in our formalisation), and it seemed silly to reconstruct the rational numbers inside our real numbers just to be able to formalise this proof. Therefore, instead of constructing Q, we modified the proof so that it no longer referred to the rationals. The result is presented here.

The main idea behind the modification of the proof is that we introduce fuzziness in the comparisons. The proof will contains a lsquo;fuzziness parameterrsquo; . Instead of having to decide whether

all we need to establish is whether

Constructively we have cotransitivity of the order relation

from which it follows that the disjunction with the rsquo;s is decidable.

Apart from not needing Q, another difference between the proof presented here and the proof in [17] is that we have avoided using Vandermonde determinants. In the original proof, this is used to prove FTA from FTA for monic polynomials. We prove this implication directly, using some polynomial arithmetic. Therefore therersquo;s no use of linear algebra in the proof anymore.

We have formalised the proof presented here using the Coq system: this was

known as the FTA project [7]. In the formalisation, we treat the real numbers axiomatically. More precisely, the reals form a part of a constructiv

剩余内容已隐藏，支付完成后下载完整资料

A Constructive Proof of the Fundamental

Theorem of Algebra without Using the Rationals

Herman Geuvers, Freek Wiedijk, and Jan Zwanenburg

Department of Computer Science, University of Nijmegen, The Netherlands

{herman,freek,janz}@cs.kun.nl

Abstract：In the FTA project in Nijmegen we have formalised a constructive proof of the Fundamental Theorem of Algebra. In the formal isation, 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 axiomatising 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 formalise is the one in theseminal 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 isnrsquo;t. In our case, this is not so convenient, because the axiomatisation of the reals doesnrsquo;t lsquo;containrsquo; the rationals. Moreover, we found it rather unnatural to let a proof about the reals be mainly dealing with rationals. Therefore, our version of the FTA proof doesnrsquo;t refer to the rational numbers. The proof described here is a faithful presentation of a fully formalised proof in the Coq system.

1 Introduction

The Fundamental Theorem of Algebra states that the field of complex numbers

is algebraically closed. More explicitly, it says that

For every non-constant polynomial

With coefficients in , the equation has a solution.

This theorem has a long and illustrious history (see [6] or [11] for an overview). It was proved for the first time in Gaussrsquo;s Ph.D. thesis from 1799. Many proofs of the Fundamental Theorem of Algebra are known, most of which have a constructive version of the simple proof that derives a contradiction from the assumption that the (non-constant) polynomial is minimal at with . We briefly repeat the classical proof here. Let be a non-constant polynomial.

First note that must have a minimum somewhere, because if

. We may assume the minimum to be reached for . Now, assume the minimum of is not 0. The function has the form

with . Because of this, and we can take

with , and if is small enough, the part will be negligible compared to the rest, and we get a for which

So is not the minimum and we have and we have derived a contradiction.

By iterating this idea, one can try to construct a Cauchy sequence to a zero of the polynomial. The main difficulty with this approach is that we have two conflicting requirements for the choice of.

If is chosen too small each time, we may not reach the zero in countably many steps (we will go down, but might not go down all the way to zero).

If is not small enough, we are not allowed to ignore the part.

The solution to this is that, instead of using the above representation (in which the term is the smallest power with a non-zero coefficient), in the constructive proof one just takes some appropriate (not necessarily the smallest) and writes as

That way one can make sure that not only , but in fact for some fixed .

For every non-constant polynomial

With coefficients in , such that for some , the equation has a solution.

As the equality on (and therefore on ) is not decidable we canrsquo;t just write as with . Therefore, in constructive analysis, one works with the notion of apartness, usually denoted by #, which is a lsquo;positive inequalityrsquo;: if we positively know them to be distinct, i.e. we know a distance between them.

Now, one can constructively find a root of if we positively know some coefficient to be distinct from 0. The proof of constructive FTA proceeds by first proving it for monic polynomials (i.e. where ).

The original Kneser proof of FTA for monic polynomials makes use of an approximation of the polynomial with coefficients in Q, because it needs to compare the size of various expressions (which is not decidable in R). We found this unsatisfactory: the rational numbers donrsquo;t seem to have anything to do with the Fundamental Theorem of Algebra! Also, in our Coq formalisation of Kneserrsquo;s proof, we introduced the real numbers axiomatically (so a priori we didnrsquo;t have Q in our formalisation), and it seemed silly to reconstruct the rational numbers inside our real numbers just to be able to formalise this proof. Therefore, instead of constructing Q, we modified the proof so that it no longer referred to the rationals. The result is presented here.

The main idea behind the modification of the proof is that we introduce fuzziness in the comparisons. The proof will contains a lsquo;fuzziness parameterrsquo; . Instead of having to decide whether

all we need to establish is whether

Constructively we have cotransitivity of the order relation

from which it follows that the disjunction with the rsquo;s is decidable.

Apart from not needing Q, another difference between the proof presented here and the proof in [17] is that we have avoided using Vandermonde determinants. In the original proof, this is used to prove FTA from FTA for monic polynomials. We prove this implication directly, using some polynomial arithmetic. Therefore therersquo;s no use of linear algebra in the proof anymore.

We have formalised the proof presented here using the Coq system: this was

known as the FTA project [7]. In the formalisation, we treat the real numbers axiomatically. More precisely, the reals form a part of a constructiv

剩余内容已隐藏，支付完成后下载完整资料

资料编号：[273065]，资料为PDF文档或Word文档，PDF文档可免费转换为Word