Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added some discussion to the comment box at the bottom of constructive mathematics. I'd like to work those quotes in to a section called "criticism" or "opposition". Half of the reason I want to do that is so those quotes are on that page. Does anyone oppose me doing this?
Let's create a section titled "History" where such quotes can go.
But let's also make very clear at this entry, that a main point of caring about excluded middle and other constructive math is that it arises in nature all the time and is hence not up to us humans to decide to be a good idea or not: the internal logic of almost every topos is of this sort.
I mean, that's why we care about constructive mathematics, not why, for example, Brouwer cared about constructive mathematics.
Edit: I misread your post slightly, but you can probably get the gist of what I meant.
I mean, that's why we care about constructive mathematics, not why, for example, Brouwer cared about constructive mathematics.
I am not an expert on the history of this, but I know it does happen that people care about the right things for slightly insufficient reasons. Then of course it is easy to attack their attitude, even if it is right.
And by the way: Hilbert is also famous for a major misconception about the foundations of math.
I agree in spirit with Urs's recommendation; it could also be titled Philosophical Arguments [or Viewpoints or something]. Something like this could also be given a page of its own. I have no real objection to any of that, provided that the page remains neutral on the question of rightness or wrongness of Constructivism, nothing beyond a milder claim that it's worthy of investigation.
As I say, I'm not strongly opposed, but I'm also not convinced it would be all that useful to record such debates from a bygone era. They seem a little quaint and antique to me. On the other hand, references to reputable histories of this would be welcome.
@Urs: I don't think any of Brouwer's work outside of topology is particularly notable. He wasn't the first person to come up with the idea of constructive mathematics, and most of the theory was developed by other people. It seems to me that he's famous specifically for the drama he was involved in (he did real work in topology just to get tenure).
The nLab's perspective on constructive mathematics seems to be the right one (study it because it's interesting rather than making a silly philosophical stand), while Brouwer's perspective on constructive mathematics was that it was the only 'real' mathematics.
But is it obvious that Hilbert's dogmatism was markedly less silly or less strident than Brouwer's?
(Aside: am I the only one who sees a yellow line underneath each mention of the word 'perspective'? I've seen this in the Café too.)
I tend to agree with Todd #5; there's not much point in rehashing these debates here. Of course, if you do put those quotations in the text, Harry, I know the responses to them (^_^). (Or I could put them here for the record.)
@ Todd #7
Not to me; they were both quite silly, and manifestly wrong, both about each other and about their own mathematics. Perhaps it is possible to establish who was sillier, but I don't care to make the effort.
Good point, Ian: a browser highlighter turns on when I hover over 'perspective', and a box opens with Wikipedia's definition of the word. It's odd, though -- I don't know why it activates only with this word, or how it got activated. I use some version of Mozilla Firefox using an HP Pavilion Notebook running on Windows.
Yeah, I agree that there's not much point rehashing old dogmatism at the page on constructive mathematics, and it could be counterproductive. But there wouldn't be any harm in having a separate page about the history of the debate. One of the most fascinating things for me about the whole "foundational crisis" is that it took so long for people to realize that everyone was being foolishly dogmatic. I suppose not everyone has even realized it yet. (-:O
Once we got proper redirects, one of the things that I did throughought the Lab was to ensure that the links to constructive mathematics and constructivism all worked well; most links are to the former, while those few links that really refer to the philosophy rather than to the mathematics go to the latter. So while the latter currently redirects to the former, there is certainly room for it to be made into a separate page, on which one could put arguments both for and against.
@Toby: They were both silly with respect to foundations. My point is that Hilbert was otherwise a one of the greatest mathematicians of all time, while Brouwer (although it's clear from his topological work that he was quite bright) did his only significant work to trick someone into giving him tenure.
I also think that the way that Hilbert was "wrong" was much more interesting than the way Brouwer was "wrong".
@ Todd re yellow underlines:
Running Firefox 3.0 on Ubuntu 8.10, I don't know how to get a yellow underline on ‘perspective’, but I do know how to get a yellow highlight: Find in the page (Edit -> Find, or Ctrl-F), Highlight all (Alt-A), enter ‘perspective’ in the Find box, then hit Esc (just to remove the search box from view). Possibly you did something like this, in which case opening the Find box again will let you see what's going on.
But I'm not getting Wikipedia or anything like that. So my best guess is that you have some Addon that looks up words in Wikipedia (maybe this one?), and it has got ‘perspective’ stuck in it in a way somewhat similar to (and maybe even linked with, but maybe not) Firefox's Find feature.
@Toby #14: thanks for the advice -- I'll check it out.
@Harry "My point is that Hilbert was otherwise a one of the greatest mathematicians of all time, while Brouwer (although it's clear from his topological work that he was quite bright) did his only significant work to trick someone into giving him tenure."
If that's actually the point, then of course I would oppose its appearing on an nLab page -- that kind of disparaging assessment (of Brouwer in this case) has no place on the Lab. (Perhaps that's not actually your main point.)
Anyway... yeah, a page on the history of these debates would be of interest. Best would be to stick to supportable facts; other opinions (such as on the significance of Brouwer's intuitionist musings, or who was the more interesting, Brouwer or Hilbert) is probably not the way to go. That would be more of a blog discussion, should it ever come up.
While adding to constructive mathematics the reference
I removed the following ancient query box. If anyone insists this stuff should be there, please copy it back but remove my initial question. I no longer have this question, and I feel that meanwhile we could discuss that question in a better way.
+– {: .query}
Urs asks: Can you explicitly specify for me the topos which describes Sets as viewed by constructivists? Or is that the wrong question to ask?
Toby replies: It is the wrong question to ask. Constructivists believe that the category of sets is the category of sets; what more can they say? It is the classical mathematicians that go around making unjustifiable claims about this category, such as that it is boolean, or is a topos, or has choice.
Instead, the questions to ask are: What do constructivists believe about the category of sets? and What sort of category's internal logic serves as a model of constructivist reasoning? The first question asks what axioms to use as an ETCS-like foundation of mathematics if you are a constructivist; the second question asks how a classical mathematician can understand constructive mathematics by interpreting it as a discussion of internalisation. Note that these are different questions; even for classical mathematics, the answers to the questions are different. (In particular, everybody agrees that the category of sets is well-pointed, but classical mathematicians cannot understand constructive mathematics by doing it internal to a well-pointed topos, since they can prove that such a topos must be boolean!)
What's more, the answers to these questions depend on what constructivists you're talking about! A simple answer, good for many purposes, is that a constructivist believes that the category of sets is a well-pointed topos (whereas a classical mathematician believes that it's a well-pointed topos satisfying choice). This is actually a fairly strong statement that many constructivists would disagree with (and then again, it is too weak for some reasoning that some constructivists would accept), but at least it does not imply excluded middle. Correspondingly, a simple answer for what kind of category to internalise constructive mathematics in is that it should be done internal to an arbitrary topos; again, this allows one to produce proofs that many constructivists would dispute, but at least not any proof of excluded middle.
I know, I know, you want to know which topos! But do you see how unfair this question is? A constructivist might as well ask you which topos to interpret classical mathematics in, and you would reply ’Why, , of course!’. But this would tell the constructivist nothing, since the constructivist is also working with . What you need to tell the constructivist is that you assume that has choice; then the constructivist can follow your reasoning. To be sure, there are various specific toposes (the effective topos, the realisability topos, the category of sheaves on the real line, etc) that are useful for understanding some aspects of constructive reasoning, but you can't point to any of them and say ’There, that's the topos that constructive mathematics is done in.’, because none of those toposes is the category of sets.
Mike comments: While I agree with everything Toby has said, I think there is nevertheless a particular topos in which a classical mathematician could work internally to reproduce constructive mathematics: the free topos. Of course, this is something of a cheat, since the free topos is defined just so that the only statements true in it are those which are intuitionistically provable, so it’s not particularly helpful to the classical mathematician trying to understand the intuitionist. Neither do I mean that an intuitionist would claim that the free topos is the category of sets. But it nevertheless encapsulates everything the intuitionist can prove about the category of sets.
Toby replies: OK, that’s a good point, Mike. Similarly, one can understand the classical mathematician by working in the free boolean topos (or rather, the free topos-with-choice, although I’m not entirely certain that this exists). But classical mathematicians don’t believe that this topos is the category of sets either. (Indeed, to assume that it is probably amounts to something like the axiom of constructibility. insert standard disclaimer that ’constructible’ ’constructive’.).
Mike 2-replies: Actually, I don’t think that asserting that the free boolean topos is the category of sets has anything to do with the axiom of constructibility. On the one hand, since the axiom of constructibility is not provable from ZFC, there is no reason for it to be true in any free topos (except the “free topos satisfying the axiom of constructibility,” to whatever extent that exists). On the other hand, any free topos (on a countable theory) is countable, so there are many models of ZFC + constructibility that are not the free boolean topos.
I have been trying for some time to figure out the “categorical meaning” of the axiom of constructibility, but I have so far mostly failed. It seems to be very closely tied to membership-based set theory.
Toby: OK, forget I said anything about constructibilty.
[ continued in next comment ]
[ continuation from previous comment]
Harry: Could we work this quote:
“Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists. To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether.” - D. Hilbert
into the text somewhere? It’s too good a quote to pass up. I also love:
“No one will drive us from the paradise which Cantor created for us.” - D. Hilbert
=–
There is some formal version of a statement along the lines that if a proposition is false classically, then it cannot be true constructively. What’s the right technical term for this situation?
I’m not quite sure, but surely double negation translation is relevant.
Would you have: if is classically true, then is true constructively, and so is true constructively?
@Urs #19:
If by ‘constructively’ you mean in some formal system that admits only classically correct reasoning (but not all classically correct reasoning), then we can say something stronger: if something is valid1 constructively, then it is valid classically. Assuming that the system is consistent, your claim follows.
On the other hand, if ‘constructively’ can mean something like intuitionistic mathematics or Russian constructivism that accepts some classically false axioms, then your claim fails; any one of these classically false axioms is itself a counterexample.
Validity is more appropriate than truth if we're talking about proof systems rather than models. ↩
Thanks. I mean simply that if something is not provable with excluded middle, then it is not provable without. This is evident, I hope. But what i am after is the technical term for this situation. Something involving the word “proof strength” or the like?
David #21: yes, that’s what I had in mind.
So put more directly, #21 says that if is true classically, then is true constructively. This is not exactly what I was after, but if this is what double negation translation is about, then we should add a line there in the Idea section that makes this simple statement transparent.
OK. It now opens:
Double negation translation is a method for converting propositions valid in classical logic into propositions valid in intuitionistic logic. In particular, if is a proposition, then is derivable in classical logic if and only if is derivable in intuitionistic logic.
I guess we should link from ’valid’ in the first sentence. But then validity starts off talking about modal logic. So I’ve added a couple of sentences to make that more general.
Thanks, David. This should also be linked to from other relevant entries. I have added a line at classical logic and created a stubby sub-section at constructive logic – Double negation.
David, I have added some more hyperlinks to the sentence that you added:
In particular, if is a proposition, then is derivable in classical logic if and only if its double negation is derivable in constructive logic.
In particular notice that we do have an entry double negation (previously not linked to from double negation transform)
is derivable in classical logic if and only if is derivable in intuitionistic logic.
That’s not true exactly. Glivenko’s theorem is only about tautologies; for general propositions you have to do the double-negation translation by inserting double-negations recursively throughout the formula wherever there is a or an .
Oh yes, damn. Now that’s gone into several places.
But now if modified to
In particular, if is a classical tautology, then is derivable in classical logic if and only if its double negation is derivable in constructive logic
is that important enough to appear in the Idea section?
My apologies for having sent us down that path, esp. my response in #24. But to address Urs #19: if in a consistent theory a closed formula is provable classically, then cannot be provable intuitionistically, because if it were, then since all intuitionistic proofs are classically valid, we would have (classical) proofs of both and . Is that what you’re after? I don’t know the official technical term for that, but the principle just seems to be “intuitionistic proofs are classically valid”.
In particular, if is a classical tautology, then is derivable in classical logic if and only if its double negation is derivable in constructive logic
I’d hold off on that as well. A formula of type is a classical tautology, but is not an intuitionistic tautology. One can prove only the weaker formula .
Right, Glivenko’s theorem is actually only about propositional tautologies. I would be more inclined to put in the idea section something about the correct -translation; the fact that you can deal with a propositional tautology by simply double-negating it on the outside seems like little more than an accident to me.
Now that’s gone into several places.
I’ll fix that, don’t worry about it. (Sorry, I didn’t take the time to really look into this.)
As soon as we have some decent informal statement in the Idea-section at double negation translation, I’ll adjust the (three, I think) entries that refer to this.
I suggest we just leave out that sentence.
To atone for my error, I’ve put in the translation for the first-order case.
I suggest we just leave out that sentence.
No, wait, it must be possible to give a decent informal idea of what is roughly going on in the entry.
Maybe, but not starting out from there. I should think we ought to explain what people were looking for in such translations.
This article looks interesting:
According to the authors, people wanted to know whether classical reasoning was stronger that intuitionistic reasoning, and used double negation translation to show, e.g., that
the consistency of arithmetic based on intuitionistic logic (Heyting arithmetic) is equivalent to the consistency of arithmetic based on classical logic (Peano arithmetic).
I’ve added:
It can be used to establish relative consistency results. For example, it may be possible to show that the proof of a contradiction in a classical theory could be translated to the proof of a contradiction in a constructive theory. Kurt Gödel used this technique to show that Peano arithmetic and Heyting arithmetic are equiconsistent.
Preliminary note
This is only to drop a morsel of— mostly decorative yet relevant —material into a relevant thread, for—possible—use by someone else in the future, if they go about extending constructive mathematics for some reason or the other; no change was made by me on account of that, nor do I plan to incorporate this anytime soon. No response is expected on this one. If currently you are working in a mode which permits reading only important messages in the nForm, this is not an important message and you may safely skip the rest.
Explanations
In expository/pedagogical material on constructive mathematics I have repeatedly encountered discussions of the well known and discussed for decades, of course) aspect that large swathes of existing mathematical practice are in fact constructive (or readily strippable of spurious non-constructive usages), and that, by and large, most mathematicians will discover that they have been doing constructive mathematics all along. Sometimes, jokes like “Have you ever seen a category theorist write ’We now prove that the diagram is commutative. Suppose it were not commutative. Then […]’ ? “
A common literary reference, almost a cliché, relevant to this issue is Molière’s 1670 play “Le Bourgeois gentilhomme”, and a line of the character “Monsieur Jourdain”, in Scene IV of Act 2:
Monsieur Jourdain: Par ma foi ! il y a plus de quarante ans que je dis de la prose sans que j’en susse rien, et je vous suis le plus obligé du monde de m’avoir appris cela.
This is explicitly cited, or at least alluded to, over and over in the literature, even by S. Shelah on p. 205 of the Bulletin of the American Mathematical Society, Vol. 40, No. 2, p. 203–228, though there, somewhat ironically, to give support to ZFC.
Since citations of philosophers (if relevant of course) are sometimes used in the encyclopedic part of the nLab), Fichte for example, it seems that this material of Molière’s might fittingly be used in constructive mathematics (by someone else, at some time in the future).
I fully recognize that Molière is quite a different kind of philosopher from e.g. Fichte or Leibniz, and that the citations of the latter two can be seen to express some original ideas, while Molière passage is a rather trivial psychological observation, and need not be told that. This is one of the many reasons why I will not incorporate this Molière-reference. But it may help someone else.
I add this to this thread, because decorative paraphernalia can have a technical value, e.g. to get into a work flow. Moreover, I am writing an exposition of an article on unique interpretability of pasting schemes, and, in doing so, I make some (mild, pseudo-)constructive innovations, taking, as an exercise, the stance that “acylic digraph” is a meaningless concept constructively, and rather work with a constructive replacement (which is equivalent to “acyclic digraph” classically, of course). This reminded me once again of all this and I decided to add this to the thread, for further use by someone else.
Some of the below material could be used relevantly at some point of constructive mathematics, or in related articles or talks on the subject. Working with the metaphorical correspondences
classical : poetry
constructive : prose
can help give structure to articles or talks.
Re #38, in a separate comment:
Material
Again, just to provide something of a quarry for someone else, should they set to work on constructive mathematics again (such trivialities can help you to get going, and therefore are something of a work-tool), here is some material on this:
Signification : Réussir dans une activité sans le savoir, par hasard et sans dessein.
Origine : Locution proverbiale devenue expression française qui puiserait ses origines dans une célèbre pièce de Molière de la fin du XVIIIème siècle à savoir « Le Bourgeois gentilhomme » où selon une scène célèbre de l’Acte II, scène IV, M. Jourdain venait de savoir que tout langage serait classé selon la façon de le dire, en poésie ou en prose et fut réjoui de constater qu’il faisait de la prose à tout moment sans le savoir. De par cette constatation, Molière veut montrer sous un angle plaisant que les mots poésie et prose sont mis au même plan et que le terme prose soit défini d’une façon négative par rapport à la poésie.
Exemple d’utilisation : Par ma foi ! il y a plus de quarante ans que je dis de la prose sans que j’en susse rien, et je vous suis le plus obligé du monde de m’avoir appris cela. (Molière : Le Bourgeois gentilhomme)
Maître de philosophie: […] Sont-ce des vers que vous lui voulez écrire ?
Monsieur Jourdain: Non, non, point de vers.
Maître de philosophie: Vous ne voulez que de la prose ?
Monsieur Jourdain: Non, je ne veux ni prose ni vers.
Maître de philosophie: Il faut bien que ce soit l’un, ou l’autre.
Monsieur Jourdain: Pourquoi ?
Maître de philosophie: Par la raison, Monsieur, qu’il n’y a pour s’exprimer que la prose, ou les vers.
Monsieur Jourdain: Il n’y a que la prose ou les vers ?
Maître de philosophie: Non, Monsieur : tout ce qui n’est point prose est vers ; et tout ce qui n’est point vers est prose.
Monsieur Jourdain: Et comme l’on parle qu’est-ce que c’est donc que cela ?
Maître de philosophie: De la prose.
My translation of the above:
Philosophy instructor: […] Is it poetry that you want to write?
Monsieur Jourdain: No, no, not poetry.
Philosophy instructor: You want to write nothing but prose?
Monsieur Jourdain: No, I want neither prose nor poetry.
Philosophy instructor: It has to be either one, or the other.
Monsieur Jourdain: Why?
Philosophy instructor: For the reason, Sir, that to express oneself there is nothing other than either prose, or poetry.
Monsieur Jourdain: There does not exist anything other than either prose or poetry?
Philosophy instructor: No, Sir: all which is not prose is poetry; and all which is not poetry, is prose.
Monsieur Jourdain: And when one talks, what is this?
Philosophy instructor: Prose.
large swathes of existing mathematical practice are in fact constructive (or readily strippable of spurious non-constructive usages), and that, by and large, most mathematicians will discover that they have been doing constructive mathematics all along.
That seems not to be the case to me. On the contrary. Just take the basics of topology. EM is absolutely everywhere. AC is used repeatedly at crucial steps. Constructive topology is something quite differnt from what is commonly known. And that’s just basic topology, on which a major part of the rest of mathematics is based
Re #40. Many thanks for this point of view. While I am not asking for it, I would be happy to read more of this (somewhere).
This of course depends on the interpretation of “large swathe”. I did not say “the majority of” or “most of”.
The estimate given is of course hard to make precise. It is surely also biased by me having been trained in combinatorics, working mainly with combinatorial structures which are often formalizable in something much more constructive and weaker than ZF + AC + EM.
And, well, graph theory, to me at least, is one of the “large swathes of existing mathematical practice”.
It is also biased by the subjective experience that many negative definitions I was so accustomed too can easily and usefully be replanced with more (pseudo-)constructive ones, and also biased by the very particular thing I am currently constructing, a proof which uses a sort-of-novel definition of directed acyclic digraph (DAG for short), namely
(constructive DAG) (digraph in which for each weakly-connected finite circuit there exist at least one vertex on said circuit with in-degree-zero-on-that-circuit and at least one vertex on said circuit out-degree-zero-on-that-circuit)
It is sort-of-ironic that computer scientists tend to work with the traditional negative there-does-not-exist-any-directed-circuit definition of “DAG”.
Remarks.
The above is evidently classically-equivalent to “there does not exist any finite directed circuit”, but it is at least “pseudo-constructive” in that it avoids a negation in the definition of DAG. And it is just what Power (cf. this thread) uses of the property “acyclic” in JAlg129, so one can just as well take this as the definition from the get-go, at least as an exercise. I seems to work beautifully, but I am not done yet.
It is clear what I mean by “weakly-connected circuit” and I will not detail this unless requested, to make some progress on how essential planarity is for Power’s theorem.
Re 41: I accidentally said a construable-as-uneducatedness thing in
and weaker than ZF + AC + EM.
I am aware of what Diaconesu, Goodman, Myhill proved (roughly, AC => EM; hence ZF + AC + EM approx ZF+AC = ZFC).
It might be worth adding a brief mention of the bourgeouis gentleman to constructive mathematics as relevant to the experience of at least some mathematicians, but I think it would be at most one sentence.
Also, “ZF” generally refers to a theory that already includes EM. If you want to refer to an analogous theory in constructive mathematics there are IZF and CZF.
re 43:
Also, “ZF” generally refers to a theory that already includes EM.
Thanks for pointing out. But how does it include EM ? ZF, to my way of thinking at least, is just an (untyped) first-order theory with a single binary relation symbol, and in particular does not contain any symbol for truth, nor does it make any prescriptions for how to reason with it.
The nLab page ZFC does not (formally) include EM into the list of axioms of ZF. My copy of Jech, Set Theory apparently never mentions “excluded middle”, nor does your very useful “Set Theory for Category Theory”. Did you mean it in the sense that ZF is usually reasoned about using EM, or in a more formal sense of “includes”? Or did you mean to write that ” “ZFC” generally refers to a theory that already includes EM. ” The “C” was left out in your comment.
That’s a good question. I did mean ZF. (As you say, of course ZFC includes EM, since AC implies EM.) In general, the way that a first-order theory includes EM is by including it as an axiom (or axiom schema). There is no need for a “symbol for truth”; EM is the axiom schema that for any statement . (However, any first-order theory does contain a symbol for truth: the true proposition is one of the logical connectives.)
However, since most mathematicians use classical logic by default, they do not bother to mention it as an axiom. (This includes Jech, as well as my “Set theory for category theory” which was written for classical mathematicians. But my stack semantics paper does treat EM as an axiom schema – p.9.) This is why EM is not usually listed in the axioms of ZF. (Equivalently, one can formulate ZF — or any other first-order theory — inside a notion of “first-order logic” that contains or proves EM “at the level of logic” rather than at the level of the theory.)
Now it’s true that in general constructive mathematicians don’t rename things when they remove EM as an assumption. For instance, even though topological spaces (say) are usually studied in the context of EM (since, as noted, most mathematicians use classical logic by default), a constructive mathematician doesn’t start talking about “constructive topological spaces” when they use the same word-for-word definition of topological space but in the absence of EM. So one might argue that a constructive mathematician should simply say “ZF” to refer to the axioms of ZF (without EM) in constructive logic, since to them the default logic is constructive.
However, in practice, ZF is very closely associated with classical mathematics, so it is less confusing overall to adopt the convention that “ZF” includes EM and speak of “intuitionistic ZF” or “constructive ZF” for theories that don’t. This is partly because while set theory (such as ZF) has overwhelmingly become the “default” foundation for classical mathematics, this is less true for constructive mathematics; constructive mathematicians often prefer type theory, or weaker frameworks like Heyting arithmetic, or not to formalize their foundations at all. It’s also because a large fraction of ZF-theory depends on EM, relative to many other branches of mathematics; even the basic theory of ordinal numbers and so on looks very different constructively. Furthermore, it doesn’t really work very well to literally write down the “same” axioms of ZF and use them constructively; in particular, Replacement as usually formulated is not very useful without EM/AC and should be replaced by the classically-equivalent Collection and Separation axioms.
1 to 45 of 45