[FOM] discussion about the connection between AC and Buchbergers algorithm
pollack at cims.nyu.edu
Tue Jun 10 11:48:21 EDT 2008
I think that the following letter from Henri Lombardi bears on the
discussion about the connection between AC and a proof that
Buchberger's algorithm terminates finitely which began in (fom) vol 66
#1. In the PS. MLQ is Math.Log. Quart. I am too lazy and too ignorant
to have checked the veracity of the letter or the papers.
Hervé Perdry and me have given a constructive proof of termination
for any Buchberger algorithm.
This appeared in
The Buchberger Algorithm as a Tool for Ideal Theory of Polynomials Rings in
Constructive Mathematics, in : Gr¨obner Bases and Applications (Proc.
of the Conference
33 Years of Gr¨obner Bases), Cambridge University Press, London
Lecture Notes Series, vol. 251, (1998), 393–407.
This is based on a constructive version of Dickson's lemma.
The proof is similar to noetherianity proof for A[x] in Richman.
Some unavoidable Ackerman's lower bound appears in
(this constructive version of) Dickson lemme.
I attach a version of our paper where some "horrors" are corrected:
e.g. Dickson instead of Dixon.
Also see the wonderful paper of Hervé just appeared in MLQ
Professor of Mathematics and Computer Science
Courant Institute of Mathematical Sciences/NYU
Office: Room 716, Warren Weaver Hall (Courant
Mailing Address: 251 Mercer Street,
New York, NY 10012, U.S.A.
Email: pollack at cims,nyu.edu
More information about the FOM