2
$\begingroup$

The question Getting a bound on the coefficients of the factor polynomial got very nice answers on Gelfond's theorem. But for work on proof theory of arithmetic I want a proof in arithmetic. The published proofs use Mahler measure defined in complex analysis. Are there published proofs of Gelfond's theorem in arithmetic in the first place. I should say, proofs published in English or some Western European language. I cannot read Gelfond's paper in Russian.

In fact Mahler uses the sort of complex analysis which is probably conservative over Peano arithmetic along the lines of Takeuti's "A Conservative Extension of Peano Arithmetic." But I am not skilled at that yet. Can anyone here tell me if that will work for Mahler measure? or won't? Or point me to a better source?

Emil Jeřábek asks reasonably if I need Gelfond's theorem. In fact I do need something close to it. I want polynomial factorization over algebraic number fields. This is probably best approached in terms of two-variable integer polynomials where the first variable is really to be taken modulo an irreducible polynomial over $\mathbb{Z}$. This would be a pretty special case of Gelfond's theorem, but not obviously reducible to one-variable polynomials over $\mathbb{Z}$.

To be clear I am asking to know a proof, so I can check if it works in EFA. The project is to establish that EFA suffices for the classical Galois theory of number fields inclduing the Artin-Schreier theorem -- which is not obvious, since results in Reverse Math show even PRA does not suffice for the more general theory of algebraic extensions of $\mathbb{Q}$.

$\endgroup$
9
  • 1
    $\begingroup$ Why do you spell it as Gelfand rather than Gelfond? At least according to wikipedia, the name of Alexander Gelfond is spelt with an o, and Israel Gelfand with an a; not only in English, but also in Russian. $\endgroup$
    – Lucia
    Jan 17, 2014 at 16:50
  • 1
    $\begingroup$ Because Joe Silverman does in his answer to the cited question, and elsewhere. Both spellings exist on line. $\endgroup$ Jan 17, 2014 at 16:54
  • $\begingroup$ Do you really need Gelfond’s theorem? Pietro Majer gave a completely elementary answer that will formalize in PA (or a much weaker theory, for that matter) with no difficulty. $\endgroup$ Jan 17, 2014 at 17:17
  • 3
    $\begingroup$ Dear colleagues! Israil GelfAnd and Alexandr GelfOnd are two different people (as you can easily check with Mathscinet). The theorem in question is due to Alexandr Gelfond. Each of them has only one correct spelling. $\endgroup$ Jan 17, 2014 at 19:18
  • 1
    $\begingroup$ @ColinMcLarty I have a great talent for misspelling names (and other words, but spell-check helps with those), so even I wouldn't cite myself as a source for the correct spelling of someone's name. :) $\endgroup$ Jan 18, 2014 at 3:24

1 Answer 1

1
$\begingroup$

The Henselian strategy of Zassenhaus uses $p$-adic bounds rather than the integer exponential bounds of Gelfond's theorem. Weinberger and Rothschild develop this approach over algebraic number fields, by an algorithm explicit enough to be its own proof, in ``Factoring Polynomials Over Algebraic Number Fields,'' ACM Transactions on Mathematical Software,1976, 335--50.

http://www.math.ucsd.edu/~lrothsch/Reprints/Factoring%20polynomials%201976.pdf

This solves the problem behind my question.

The original question sought an explicitly arithmetic proof of Gelfond's theorem, or an explicit metatheoretic proof that it must be so provable. Gelfond's theorem is probably provable in EFA and likely in some even weaker fragment which could be explored if we had a PA proof to begin with. Emil Jeřábek's suggestion using Gaussian rationals might work but it depends on approximating integer polynomials by ones with rational roots -- and the current state of the art on that seems to be the Henselian strategy rather than Gelfond's theorem.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.