# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTodd_Trimble
• CommentTimeNov 27th 2010

I wrote out a proof which uses very little machinery at fundamental theorem of algebra. It is just about at the point where it is not only short and rigorous, but could be understood by an eighteenth-century mathematician. (Nothing important, just fun!)

• CommentRowNumber2.
• CommentAuthorTobyBartels
• CommentTimeNov 28th 2010

Thanks, I added a bit about the theorem’s status in constructive mathematics.

• CommentRowNumber3.
• CommentAuthorTobyBartels
• CommentTimeNov 29th 2010

This led me to write square root, which is where the constructive difficulties in both the FTA and the quadratic formula lie.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeNov 29th 2010

Added link to root to fundamental theorem of algebra and added a stub. But Toby will want to go over it.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeNov 29th 2010

How do you define the absolute value constructively? I guess I can see how to do it for real numbers as constructed in terms of rational numbers, since we know what the absolute value of a rational number is, but did you have anything more general in mind?

• CommentRowNumber6.
• CommentAuthorTobyBartels
• CommentTimeNov 30th 2010

In general, there’s no constructive way to define absolute value in a linearly ordered field. (At least, I don’t see how to do it, although I don’t actually know any counterexamples.) That why at one point I include the existence of an absolute value in the hypothesis of a statement on square root. (Perhaps the existence of an absolute value should be an extra hypothesis in the constructive definition of a linearly ordered field? I haven’t thought about this very much.)

However, in a real-closed field (which is what matters for the FTA), you can define absolute value as ${|x|} \coloneqq \sqrt{x^2}$ and prove the usual properties. At one point I had the existence of an absolute value as a redundant condition on a real-closed field somewhere on one of these pages, but I think I removed this quickly enough that it doesn’t even show up in the history.

• CommentRowNumber7.
• CommentAuthorHarry Gindi
• CommentTimeNov 30th 2010

There is something wrong with constructive mathematics if it can’t prove the quadratic formula =.

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeNov 30th 2010

Harry, as I understand it, the problem is choosing a square root. Paul Taylor puts it well in his Practical Foundations of Mathematics: in for example the topos of sheaves over $S^1$, there is a $\mathbb{Z}_2$ torsor given by the squaring map $S^1 \to S^1$. This is epi, so that in the internal logic the proposition “each element of $S^1$ has a square root” is true, but insofar as there is no global section of the squaring map, you can’t “choose a square root” (in the sheaf context the choosing is continuous choice). Taylor refers to Buridan’s ass here, saying here are two square roots that look equally inviting to the donkey, and he cannot choose between them.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeNov 30th 2010

Let’s put that example somewhere into an $n$Lab entry.

I think with the comparatively huge amount of remarks on constructive math that we do have on the $n$Lab, it would be very good to have a page or two that spells out plenty of examples of for what this is good for . Lots of examples where one wants to work in a topos by ordinary reasoning but has to stick to constructive arguments. I think such a list of examples will add considerable value to what we already have (thanks mostly to Toby).

• CommentRowNumber10.
• CommentAuthorTobyBartels
• CommentTimeDec 1st 2010
• (edited Dec 4th 2010)

Let’s put that example somewhere into an $n$Lab entry.

There’s already an example at square root, which is the topos of sheaves on the real line, although without any of Taylor’s poetic language about Buridan’s ass.

However, I’m afraid that I’ve never understood Taylor’s example (crappy online version). Taylor seems to argue that because there is no function $\sqrt{}\colon S^1 \to S^1$ in constructive mathematics (which is true), there is no proof of $\forall y\colon S^1,\; \exists x\colon S^1,\; y = x^2$ in constructive, and this I cannot accept (since it can be proved in the language of the free pretopos with NNO, which is the basic non-finitist variety of constructive mathematics). What is true is that there is no proof of $\forall y\colon \mathbb{C},\; \exists x\colon \mathbb{C},\; y = x^2$ in constructive mathematics (and in particular in the internal language of the sheaf topos over the real line), but this is evidently not what he’s talking about, since he mentions only $S^1$ and not $\mathbb{C}$. His main point seems to be a philosophical one about the difference between mathematical objects and their codings (which can be resolved by passing from a category of presets to a pretopos of sets).

That you cannot prove $\sqrt{x^2} = x \;\vee\; \sqrt{x^2} = -x$ (without the LLPO) seems more like Buridan’s ass to me. That you cannot prove $\forall y\colon \mathbb{C},\; \exists x\colon \mathbb{C},\; y = x^2$, on the other hand, seems unlike Buridan’s ass; it is inherently $2$-dimensional. (Recall that you can prove $\forall y\colon \mathbb{R},\; \exists x\colon \mathbb{C},\; y = x^2$; in fact, you can even prove the existence of a function $\sqrt{}\colon \mathbb{R} \to \mathbb{C}$.) The failure is not that you are being pulled in two directions, but rather that you are always spinning in circles.

As far as the relevance of continuous functions goes, it’s immaterial that there is no continuous section of the squaring map $S^1 \to S^1$ or $\mathbb{C} \to \mathbb{C}$; what matters is whether there is a continuous partial section on any sufficiently small open set. (After all, we’re talking about sheaves here!) For $S^1 \to S^1$, there is one on any proper open subset; for $\mathbb{C} \to \mathbb{C}$, there is none on any neighbourhood of $0$, and that is where the problem lies.

• CommentRowNumber11.
• CommentAuthorTodd_Trimble
• CommentTimeDec 1st 2010
• (edited Dec 1st 2010)

The failure is not that you are being pulled in two directions, but rather that you are always spinning in circles.

Yes, I agree with you now that the Buridan’s ass metaphor is not very apt.

For $S^1 \to S^1$, there is one on any proper open subset; for $\mathbb{C} \to \mathbb{C}$, there is none on any neighbourhood of 0, and that is where the problem lies.

Ah! Thanks for clarifying that; the issue is that the squaring map on the complex numbers is ramified at $0$.

• CommentRowNumber12.
• CommentAuthorTobyBartels
• CommentTimeDec 3rd 2010

the issue is that the squaring map on the complex numbers is ramified at $0$

Yes, exactly, although I’m not fluent in algebraic geometry, so I don’t think to say it that way.

• CommentRowNumber13.
• CommentAuthorTobyBartels
• CommentTimeDec 4th 2010

I’ve edited #10 to better reflect what Taylor wrote, although it mostly affects the bits in parentheses.

• CommentRowNumber14.
• CommentAuthorTobyBartels
• CommentTimeDec 4th 2010

@ Harry

There is something wrong with constructive mathematics if it can’t prove the quadratic formula =.

It can prove the quadratic formula; the question is whether one can prove that it always applies, that is whether one can prove that every complex number has a complex square root. Most schools of constructive mathematics can prove this, but Fred Richman’s school cannot; there is something wrong with it.

And there is something wrong with classical mathematics too, since it can’t prove that every subset of the real line is measurable, that every function from the unit interval to the real line is uniformly continuous, etc etc etc. You can’t have everything.

• CommentRowNumber15.
• CommentAuthorHarry Gindi
• CommentTimeDec 5th 2010
• (edited Dec 5th 2010)

@Toby:

Every function from the unit interval to the real line is uniformly continuous

That isn’t even intuitively true. (Heaviside step function)

Every subset of the real line is measurable

Why should this be true? It seems pretty unintuitive to me, but I also have some harsh opinions of measure theory in general (i.e. that it’s not the canonical “right” notion).

• CommentRowNumber16.
• CommentAuthorTodd_Trimble
• CommentTimeDec 5th 2010

Harry, I hope you’re not doubting that Toby knows what he’s talking about with regard to constructive mathematics! “Every function from the unit interval to the real line is uniformly continuous” is meant to be interpreted in certain constructive frameworks, such as a suitable world for doing synthetic differential geometry.

• CommentRowNumber17.
• CommentAuthorHarry Gindi
• CommentTimeDec 5th 2010
• (edited Dec 5th 2010)

@Todd: Sure, but I’m saying that such a conclusion is not at all intuitive, while the quadratic formula is intuitively true as a result of plane geometry as related to completing the square.

What I was talking about in my original post was that if there is some proposed system of axioms for doing mathematics in general, it should at least be able to prove results that are intuitively true (wasn’t this Brouwer’s original reason for coming up with it?).

I was using “should be true” to mean “should be true in any reasonably useful system of axioms”.

• CommentRowNumber18.
• CommentAuthorMike Shulman
• CommentTimeDec 5th 2010

Brouwer found the facts cited by Toby (at least, the first one; I don’t know whether he knew any measure theory) to be intuitively true. The problem with the Heaviside step function $H$ is that it is not defined on the whole real line. Consider the real number $x$ with decimal expansion $0.x_1 x_2 x_3 x_4 \dots$, where $x_n$ is $0$ if $2n+2$ is a sum of two primes, and $1$ otherwise. What is $H(x)$? (Or, if your convention for $H(0)$ makes that an easy question, what is $H(-x)$?) I’ll be very impressed if you can give a definite answer.

For the other, the existence of nonmeasurable sets has many consequences that many people find unintuitive, such as the Banach-Tarski paradox and the behavior of probability on infinite domains.

(That said, I personally still do think the most convincing argument for using constructive reasoning is that it stays valid when you move into an arbitrary topos. I’m just saying that different people might have different “intuitions” from you.)

• CommentRowNumber19.
• CommentAuthorTodd_Trimble
• CommentTimeDec 5th 2010

I’ll let Toby respond. “Intuitively true” depends on the intuitions one has.

• CommentRowNumber20.
• CommentAuthorHarry Gindi
• CommentTimeDec 5th 2010
• (edited Dec 5th 2010)

@Mike: Are we thinking of the same Heaviside step function? I don’t understand what you’re getting at.

• CommentRowNumber21.
• CommentAuthorTodd_Trimble
• CommentTimeDec 5th 2010

Harry, a more basic point that should be borne in mind is that $x \geq 0 \vee x \lt 0$ is not constructively true, since we do not assume excluded middle. So the Heaviside function is not definable in a typical constructive context such as the internal logic of a topos.

This relates to Mike’s example because in intuitionism or constructive mathematics, existence is established by exhibiting a witness or witnessing proof. There is not (as yet) a witnessing proof of Goldbach’s conjecture.

• CommentRowNumber22.
• CommentAuthorHarry Gindi
• CommentTimeDec 5th 2010
• (edited Dec 5th 2010)

So the constructive reals don’t satisfy trichotomy (and are therefore not an ordered field)?

• CommentRowNumber23.
• CommentAuthorDavidRoberts
• CommentTimeDec 5th 2010

@Harry: field

• CommentRowNumber24.
• CommentAuthorHarry Gindi
• CommentTimeDec 5th 2010
• (edited Dec 5th 2010)

If you look at the category of (pre?)sheaves on a category with a terminal object, aren’t all fields discrete?

Doesn’t that cover basically every interesting case?

For instance, in simplicial rings, every simplicial ideal is contained in a maximal ideal (every SCR surjects onto a simplicial field), and all simplicial fields are discrete.

• CommentRowNumber25.
• CommentAuthorDavidRoberts
• CommentTimeDec 6th 2010
• (edited Dec 6th 2010)

But the reals as usually realised (Dedekind or Cauchy, say) are not discrete. For me, Heyting fields (if I was pushed to make a stab at a useful internalised concept) are the most useful concept. To quote from field,

A residue field is a Heyting field if and only if it is a local ring. Furthermore, the quotient ring (or ‘residue ring’) of any local ring by its ideal of noninvertible elements is a Heyting field; in particular, it is a residue field (hence that name). On the other hand, not every residue field is even a local ring (the MacNeille reals are not), so not every residue field is the residue ring of any local ring.

Since local rings are such a useful concept, I would like my fields to be local rings. Note that the Dedekind reals form a Heyting field.

At field there is also the statement

another disadvantage is that this is not a coherent axiom and so cannot be internalized in as many categories.

but it doesn’t say what is needed of a category to internalise the definition of Heyting field. Presumably one needs an internal apartness relation

• CommentRowNumber26.
• CommentAuthorHarry Gindi
• CommentTimeDec 6th 2010
• (edited Dec 6th 2010)

A field is an injective ring or something (a ring $k$ such that every morphism $k\to R$ is injective). Recall that the rings of a topos are classified by geometric morphisms into $\mathfrak{S}$, the topos of presheaves on affine schemes of finite type over spec Z.

Surely the correct way to define algebraic notions is to resort to descriptions of objects by their morphisms, rather than by their elements, no?

• CommentRowNumber27.
• CommentAuthorTodd_Trimble
• CommentTimeDec 6th 2010
• (edited Dec 6th 2010)

If you look at the category of (pre?)sheaves on a category with a terminal object, aren’t all fields discrete?

Definitely not. Look at the category of sheaves on say $[0, 1]$, and take the sheaf $R$ of Dedekind reals (= sheaf of continuous sections of the projection $\mathbb{R} \times [0, 1] \to [0, 1]$). If $R$ broke up as a coproduct consisting of a zero part and a nonzero part, then the pullback of this coproduct along any global section $1 \to R$ would give a coproduct decomposition of $1$. Now there is no nontrivial coproduct decomposition of the terminal 1 since nontrivial subobjects of 1 are open subobjects and the space $[0, 1]$ is connected. We would thus infer that any continuous section is either nonzero everywhere or zero everywhere, but that’s obviously false.

• CommentRowNumber28.
• CommentAuthorHarry Gindi
• CommentTimeDec 6th 2010

Oh, then why do simplicial sets work?

• CommentRowNumber29.
• CommentAuthorTodd_Trimble
• CommentTimeDec 6th 2010

I believe the object of Dedekind reals $R$ in presheaf toposes $Set^{C^{op}}$ are indeed discrete in the sense we are talking about, because they are given by the constant presheaf $\Delta(\mathbb{R})$, where $\Delta: Set \to Set^{C^{op}}$ is the diagonal map. Since the classical reals in $Set$ admit the coproduct decomposition into a zero and invertible part, and since $\Delta$ preserves coproducts, we get a coproduct decomposition for $R$ in $Set^{C^{op}}$.

• CommentRowNumber30.
• CommentAuthorTobyBartels
• CommentTimeDec 6th 2010

Every function from the unit interval to the real line is uniformly continuous

That isn’t even intuitively true. (Heaviside step function)

Well, that depends on your intuition! There are certainly people who would find it intuitively true, possibly including such non-idiots as Richard Feynman. (I’m having trouble finding this anecdote online, so I can’t tell you just how convoluted a function it was that violated Feynman’s intuition.) In the 19th century, there was a lot of debate over what constitutes a function, with even some uniformly continuous ones coming under fire. While the modern notion of function is obviously the correct notion of something, it’s not clear that it really captures the original intuition (of Leibniz et al) of what a function is.

In any case, constructive mathematicians today would agree that $H(x) \coloneqq \left\{\array{0 & x \lt 0 \\ 1 & x \gt 0}\right.$ defines a dandy partial function; the question is whether it extends to a total function.

A more interesting question is whether the Heaviside step function (which is certainly an important mathematical object, regardless of whether it is technically a function) is best understood as an almost-everywhere-defined measurable function or as a distribution (one whose derivative is the Dirac delta function, which is not technically a function). Both can be done constructively; even classically, there is no need to worry about exactly how to define $H(0)$, which irrelevant to the point of the thing.

Every subset of the real line is measurable

Why should this be true? It seems pretty unintuitive to me, but I also have some harsh opinions of measure theory in general (i.e. that it’s not the canonical “right” notion).

The main reason why it should be true is that it makes the theory of the Lebesgue integral much nicer. Classical mathematics is almost as bad as constructive mathematics, insisting on piddling details like checking whether a set is measurable. Much as you need to know about metric spaces to understand Fred Richman’s version of the fundamental theorem of algebra, so you have to know about $\sigma$-algebras to understand classical measure theory on the real line. It’s so much easier not to bother with such complications.

It also is intuitive to a lot of people, certainly all those people who find the Banach–Tarski paradox paradoxical. There was even an article in the American Mathematical Monthly about 10 years ago advocating that an undergraduate course be taught in dream mathematics, a style of mathematics that makes this assumption.

Note that dream mathematics is not constructive; although I think that its two big nonclassical axioms (this one and a similar one about the Borel property) can be phrased in such a way as to make it compatible with constructive mathematics, they are still in themselves rather nonconstructive axioms. The reasons to prefer classical analysis over constructive analysis are also reasons to prefer dream analysis over classical analysis: things that 19th-century analysts expected to be true (and which many students today expect until, if ever, they learn otherwise) can in fact be proved.

• CommentRowNumber31.
• CommentAuthorDavidRoberts
• CommentTimeDec 6th 2010

@Toby - what exactly do you need for an internal Heyting field object?

• CommentRowNumber32.
• CommentAuthorTobyBartels
• CommentTimeDec 6th 2010
• (edited Dec 6th 2010)

@ David

I believe that the answer is that you really shouldn’t bother with them; you should just use internal local ring objects. (So you need only coherent logic.)

Every local ring comes with an apartness relation: $x \# y$ iff $x - y$ is invertible (which can be stated in coherent logic); we simply don’t have that $x = y$ if this fails (assuming that our logic is strong enough even to say this). But if we define a ‘field’ to be a local ring and a ‘field homomorphism’ to be ring homomorphism that reflects $\#$ (which can also be stated in coherent logic), then the resulting category is equivalent (in any Heyting pretopos, say) to the category of Heyting fields. So if our logic is too weak to define a field directly, then we can just use this category of local rings and $\#$-reflecting homomorphisms.

Or something like that; having written this, I now see some problems with it, but I think that they can be overcome.

• CommentRowNumber33.
• CommentAuthorTobyBartels
• CommentTimeDec 6th 2010
• (edited Dec 6th 2010)

A field is an injective ring or something (a ring $k$ such that every morphism $k\to R$ is injective).

I’m not sure what theorem you really mean here, since neither of what you say above is quite correct and I can’t figure out quite how to fix them, but I wouldn’t be surprised if it’s constructively valid.

I know this theorem: If $K$ is a field and $R$ is a nontrivial ring, then every ring homomorphism from $K$ to $R$ is an injection. The proof that immediately comes to me is constructive (although that may be because I’m used to thinking constructively first), if by ‘field’ we mean a Heyting field and by ‘nontrivial’ we mean that it is false that $0 = 1$ (which the weakest way of saying this, constructively, so the strongest possible theorem).

• CommentRowNumber34.
• CommentAuthorTobyBartels
• CommentTimeDec 6th 2010

So the constructive reals don’t satisfy trichotomy (and are therefore not an ordered field)?

@Harry: field

And more specifically: ordered field (which references also linear order).

• CommentRowNumber35.
• CommentAuthorHarry Gindi
• CommentTimeDec 6th 2010

@Toby: I’m saying that regardless of how you want to state the definition of a field object internally, we can define a field object externally to be a nontrivial ring object $k$ such that given any other nontrivial ring object $R$, any map $k\to R$ is injective. At least in a Grothendieck topos (which appears to be the only case that non-constructivists/non-logicians really have any interest), what’s wrong with this definition?

• CommentRowNumber36.
• CommentAuthorTobyBartels
• CommentTimeDec 6th 2010

I was using “should be true” to mean “should be true in any reasonably useful system of axioms”.

And what does that mean!?

In my opinion, both of these statements should be true:

• Any partial function from the unit interval to the real line (indeed, from any set to any inhabited set) can be extended to a function.
• Any function from the unit interval to the real line (indeed, from any compact space to any complete space) is uniformly continuous.

Unfortunately, they cannot both be true, on pain of contradiction. That is why there are different varieties of mathematics (even though most mathematicians are still taught that only one variety is true, as if that meant anything).

• CommentRowNumber37.
• CommentAuthorTobyBartels
• CommentTimeDec 6th 2010

what’s wrong with this definition?

It’s not quite anything that you said before.

It looks like a fine definition to me, although there may be some subtleties about what ‘nontrivial’ means. However, I haven’t yet checked the converse condition (that any ring with this property must be a field). The field of real numbers certainly satisfies it (constructively, in particular in any Grothendieck topos).

At least in a Grothendieck topos (which appears to be the only case that non-constructivists/non-logicians really have any interest)

If you mean that Grothendieck toposes are the only context where anybody other than a constructivist or a logician uses intuitionistic logic, then that’s definitely not true! What about synthetic differential geometry? What about David Roberts’s (and my) work on gerbe theory as doing things internal to a category such as $Diff$ (although fields don’t seem to come up there)? There’s a lot more to internalization than Grothendieck toposes.

• CommentRowNumber38.
• CommentAuthorDavidRoberts
• CommentTimeDec 6th 2010

…we can define a field object externally to be a nontrivial ring object $k$ such that given any other nontrivial ring object $R$, any map $k\to R$ is injective. At least in a Grothendieck topos (which appears to be the only case that non-constructivists/non-logicians really have any interest), what’s wrong with this definition?

What do you mean when you say a map is injective in an general category (say with finite limits)? Do you mean something like the opposite of projective, or a monomorphism?

• CommentRowNumber39.
• CommentAuthorTobyBartels
• CommentTimeDec 6th 2010

Monomorphism should work here; it corresponds to set-theoretically injective in $Ring$.

• CommentRowNumber40.
• CommentAuthorDavidRoberts
• CommentTimeDec 6th 2010

Yes, that would make sense given the ’external’ point of view.

• CommentRowNumber41.
• CommentAuthorMike Shulman
• CommentTimeDec 6th 2010

I thought synthetic differential geometry was usually done in a Grothendieck topos of sheaves on a site of smooth loci. In fact, I don’t think I’ve ever seen any other model for it. Of course you can write down a list of axioms and not bother about models, but if you are someone like Harry, then you may always want to think in terms of models.

I agree with the general point that there’s more to internalization that Grothendieck toposes, though. As another example, computer scientists are interested in “realizability” toposes like the effective topos, which are not Grothendieck. And (at least some of) nonstandard analysis can be viewed as taking place in a filterquotient topos, also not Grothendieck. The constructible universe can be regarded as another non-Grothendieck topos that at least set-theorists are interested in. And what about FinSet, where certainly much of combinatorics takes place?

• CommentRowNumber42.
• CommentAuthorDavidRoberts
• CommentTimeDec 7th 2010

Toby may have meant Diff in the sense of manifolds (long shot, I know) - I’ve always kept in mind non-finitely complete ambient categories for this very reason, to connect with classical theory.

• CommentRowNumber43.
• CommentAuthorTobyBartels
• CommentTimeDec 7th 2010

@ Mike:

Yes, I was just thinking of the axioms, but you’re right that the models are usually Grothendieck toposes, so that’s not a counterexample to Harry’s claim.

@ David:

Yes, by $Diff$ I meant what the Lab calls Diff, the category of manifolds that one learns about in undergraduate courses. I like that building internal groupoid theory even within that ill behaved category recreates all of the generality of differentiable stacks.

• CommentRowNumber44.
• CommentAuthorColin Tan
• CommentTimeDec 19th 2013
I like the proof that the extension of a real closed field by i is algebraically closed. Is there a converse to this statement? Such as, if K/L is a Galois field extension of degree 2 and K is algebraically closed of characteristic 0, then L is real closed?
• CommentRowNumber45.
• CommentAuthorTodd_Trimble
• CommentTimeDec 19th 2013

Colin: yes, this is part of the general threory of real closed fields. In fact, it doesn’t even have to be degree 2; that’s a bonus result even if we assume the a priori weaker hypothesis of finite degree. A good search term is “Artin-Schreier theorem”. There’s an exposition in Lang’s Algebra.

1. @Toby: I am late to the discussion :-), but what problems do you see with your #32? I didn’t know it before, but it looks perfectly fine to me.

A small remark: Homomorphisms between local rings which reflect the apartness relation defined by $x # y$ iff $x-y$ is invertible also go by the name “local homomorphism”, of course.

• CommentRowNumber47.
• CommentAuthorColin Tan
• CommentTimeDec 21st 2013
I'm reading the section which gives an algebraic proof via real closed fields. I'm wondering: is Lemma 1 used to prove the Theorem?
• CommentRowNumber48.
• CommentAuthorTobyBartels
• CommentTimeDec 21st 2013

@Ingo: I no longer remember the problems, and I can no longer find them! Perhaps they don't exist after all.

• CommentRowNumber49.
• CommentAuthorTobyBartels
• CommentTimeDec 21st 2013

@Colin: In the last line of the proof of the Theorem, we have ‘But $K$ has no nontrivial quadratic extensions by the lemma that follows’, so it's used there.

2. @Toby: As I was just about to add the observation to local ring, I noticed where the problem might hide: Apparently, some people require that the apartness relation of a Heyting field is tight (for instance Richman et at. in their book, and you when you created the entry :-), but not the nLab at field); but the natural apartness relation on a local ring is not tight in general (it is if and only if the local ring is even a residue field). I don’t know what the consensus is.

• CommentRowNumber51.
• CommentAuthorTobyBartels
• CommentTimeDec 24th 2013

The definition of Heyting field is supposed to require it to be tight (so I just edited it). But that's in a context where we have full (intuitionistic) logic at our disposal. If we only have coherent logic, then we can stick to local rings, but we have to count two local rings as equivalent if their residue fields are the same (which can be expressed using only coherent logic without explicit reference to these residue fields).

Now I think that I found the problem: it's tricky to define properly what a morphism of fields is when using local rings. We have to specify the information that would define a ring homomorphism between the local rings' residue fields without direct reference to these residue fields (or otherwise using non-coherent logic). Probably I should try to write that up at local ring.

• CommentRowNumber52.
• CommentAuthorUrs
• CommentTimeMay 5th 2014
• (edited May 5th 2014)

added a history section and some historical references, by copying-and-slightly-editing what David Roberts compiled here but is too shy to add to the $n$Lab himself.

• CommentRowNumber53.
• CommentAuthorDavidRoberts
• CommentTimeMay 5th 2014

Urs - I was going to add it tomorrow (I should be offline now, in any case). That said, as a history it is hopelessly biased and incomplete, centered purely on the elementariness of Gauss’ second proof.

• CommentRowNumber54.
• CommentAuthorTodd_Trimble
• CommentTimeJun 29th 2015
• (edited Jun 29th 2015)

I’ve been adding a few glosses to the proof via advanced calculus. From reading around a little, it looks like this may be close to the proof given by Argand in 1814 (which apparently is often considered the first rigorous proof, pace Gauss – I may add to the history section at some point). I have my doubts I can make the proof much more elementary than it is currently. Meanwhile, David Roberts is asking about the reverse mathematics of FTA at MO, which I don’t know about.

• CommentRowNumber55.
• CommentAuthorDavidRoberts
• CommentTimeJun 29th 2015
• (edited Jun 29th 2015)
• CommentRowNumber56.
• CommentAuthorTodd_Trimble
• CommentTimeJun 30th 2015

Great! Thanks for looking into this.