Hello,
Do we know if the axiom of choice is needed for Chevalley's valuation/place extension theorem (i.e. the theorem that states that for every valued field and a field extension, one can extend the valuation to the field extension)?
Hello, Do we know if the axiom of choice is needed for Chevalley's valuation/place extension theorem (i.e. the theorem that states that for every valued field and a field extension, one can extend the valuation to the field extension)? 


I think this more or less answers it? 


The MO question Artem points to is certainly relevant here, but I think it's also important to realize that the extensions of valuations studied somewhat narrowly by Krull were eventually subsumed in the much more general Chevalley extension theorem for homomorphisms. This is treated in a number of algebra books in the classical tradition, including Jacobson's Basic Algebra II (9.8) and Chapter 6 of Bourbaki's Algebre commutative. While field extensions of special types such as a simple transcendental extension might be handled more concretely, the most general extension principle formulated by Chevalley does seem to require the Axiom of Choice in the guise of Zorn's Lemma, much in the spirit of existence proofs for maximal ideals. By the way, I think it's helpful for those asking questions to provide at least some specific references (print or online) to focus the discussion. P.S. As Pete remarks, there is no proof offered that the Axiom of Choice is necessary here. I'm not sure how logicians view the question, but from a practical point of view I suspect most people would place the burden of proof on the other side: if you really believe AC is not needed, come up with a better proof than the existing ones. Most of us prefer constructive approaches when possible, but Chevalley's general extension theorem doesn't seem promising. The proofs I've seen all rely on Zorn's Lemma in a completely natural way, as do similar theorems in algebra. (One might even wonder whether Chevalley's theorem is equivalent to AC.) A small question of my own: Is it true that Chevalley was a coinventor of the label "Zorn's Lemma"? (I recall reading that somewhere, but you can't believe everything you read.) 


Choice is needed. For example, it is consistent with ZF that there exist an algebraic closure L of Q such that every absolute value on L is trivial (and Gal(L/Q) is trivial). See: Hodges, Wilfrid. Läuchli's algebraic closure of $Q$. Math. Proc. Cambridge Philos. Soc. 79 (1976), no. 2, 289297. MR0422022 As for the origin of "Zorn's Lemma", try Campbell, Paul J. The origin of "Zorn's lemma''. Historia Math. 5 (1978), no. 1, 7789. MR0462876 The following is quoted from Berrick and Keating, 2000, p26: The name of the statement [Zorn's Lemma], although widely used (allegedly first by Lefschetz), has attracted the attention of historians (Campbell 1978). As a 

