[FOM] discussion about the connection between AC and Buchbergers algorithm

[Richard Pollack]

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.

Dear Ricky
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
Mathematical Society
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.
Henri



PS:
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

-- 
Ricky Pollack
Professor of Mathematics and Computer Science
Courant Institute of Mathematical Sciences/NYU
 Office: Room 716, Warren Weaver Hall (Courant
 Institute).
Phone: 212-998-3167
Fax: 212-995-4121
Mailing Address: 251 Mercer Street,
	New York, NY 10012, U.S.A.
Email: pollack at cims,nyu.edu
homepage url:
 http://math.nyu.edu/faculty/pollack/index.html