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.
Not much there, but I created it: proper subset.
I have one objection: "In constructive mathematics, we..."
Which implies that the nLab has constructiveness (constructivism?) as part of the official nPOV. I think that when giving the constructive definition, you should actually make an effort to be NPOV in Wikipedia's sense.
It's not really up to me, but I'm just letting you know how I feel.
That is, the use of the mathematical "we" should be used as "You the reader and me the writer", not "me and other constructive mathematicians". I feel that the second usage violates the spirit of the mathematical "we".
By ‘In constructive mathematics, we …’, I mean ‘When (if ever) we do constructive mathematics, you the reader and I the writer …’. If you never do constructive mathematics, then the part of that referring to you is vacuously true, and you may ignore the whole thing if you like.
Although nobody has written about it on nPOV, one of the features on the Lab since its beginning is treatment of alternative foundations, which after all comes into category theory through internalisation. Once you admit its relevance (or notability, if you like), a discussion of what happens in constructive mathematics, without the claim that one should do such things, is NPOV (note spelling) in Wikipedia's sense.
Yeah, but we study things like constructive mathematics because it comes up in category theory and topos theory, not because we have philosophical issues with standard mathematics. If perhaps we could say "When we're working without the Law of the excluded middle...", that would make it clear that we're not part of the same intellectual tradition.
I dunno. It's not a huge deal in all honesty, but I think that many mathematicians will look askance at the nLab if it is seen to endorse constructive mathematics as a philosophy rather than a tool (even if we know that it doesn't).
So I am in favor of adding a section to nPOV that explains why constructive mathematics is inevitable and useful as soon as we like to study toposes.
The entry could also need more comments on why toposes are a GoodThing in the first place, how we can look at topological spaces as toposes etc.
With that deswcribed at nPOV we could then begin all sentences of the kind "In constructive mathematics we have" instead as "From the constructive internal nPOV, we have". Or the like. That would also serve as a continual reminder of what constructivbe mathematics is good for and hence serve eventually as a huge advertizement for it.
@Urs: Is your keyboard messed up?
Who's ‘we’ in #4, Harry? I have philosophical issues with standard mathematics, which I find often blurs meaningful distinctions. So does Mike Shulman, I believe, although not exactly the same ones. I do believe (unlike some constructive mathematicians) that classical mathematics is a worthwhile endeavour, but I study mathematics without the axiom of choice (including weak forms such as excluded middle) in part because I find it philosophically appealing to do so.
There has never been a single ‘intellectual tradition’ of constructive mathematics, but instead a broad range from knowing a few applications to wholesale rejection of nonconstructive reasoning. Nothing that I wrote on proper subset is supposed to endorse any philosophical claim, except the implicit claim that constructive mathematics is (contrary to what some classical mathematicians claim) also a worthwhile endeavour (because otherwise one would not mention it at all).
I really don't want to rephrase everything on the Lab that begins ‘In constructive mathematics’ into complicated phrasings like ‘When working without the Law of the excluded middle’ (which is wordy but at least precise) or ‘From the constructive internal nPOV’ (which will be meaningless to a casual reader who isn't already familiar with the Lab, and is also at the very least misleading). This is just how one does things in constructive mathematics.
While we're on the subject, what's so special about the subobject classifier having three values rather than two? Wouldn't having a subobject classifier with eighty million elements be more constructive?
Also, I hear that Heyting toposes are the natural kind of topos, but I don't see how that's true. Could you clarify?
@ Harry #8:
I don't know; where is there an example with a subobject classifier having three values? I suppose that, if somebody wants an example of a nondegenerate topos which is not two-valued, then the simplest example might be one whose subobject classifier has three values.
The relevance of such an example to constructive mathematics would simply be that it's a topos which is not boolean (although being boolean and being two-valued are actually independent properties of a topos). It's certainly not true that constructive mathematics is done in a topos whose subobject classifier has exactly three values. (I suppose that this might be true of some constructivists' mathematics, but not any that I know of.)
@ Harry #8 part 2:
Where do you hear that Heyting toposes are ‘the’ natural type of topos? I actually don't know what a ‘Heyting topos’ is! I know what a Heyting category is, and this is the natural type of category (not usually a topos) for internalising a certain fragment of logic; note that every topos is a Heyting category. There might be some predicativist constructivists whose mathematics is naturally described using precisely the kind of logic that a Hetying category is good for; I'm not sure.
I guess that this line (written by Mike Shulman at Heyting category) might be relevant: ‘Any Heyting category has an internal logic which is full (typed) first-order intuitionistic logic.’. If you want to know mathematically why that's true, or even exactly what it means, Mike knows that better than I do, although I could try to hand-wave it. (It's probably also in the Elephant somewhere.) So any mathematical theory that can be expressed in typed first-order intuitionistic logic can be done internally in a Heyting category, but not higher-order reasoning, even if it is constructive.
I meant "Heyting Pretopos".
Anyway, why is intuitionistic logic so important for topos theory. I mean, just give me a few technical points to look up.
Also, the thing about having three values, don't all intuitionistic topoi have subobject classifiers with three elements?
A Heyting pretopos has full internal typed first-order intuitionistic logic and also has a type theory with sums and products. That's a fairly nice environment for mathematics that is both constructive and predicative (and finitist, for that matter). There's actually a fair amount of mathematics that is expressible that way, such as elementary algebra.
The technical point is that the internal language of every topos validates intuitionistic logic, while the internal languages of most toposes do not validate classical logic. For example, the topos of sheaves on any non-discrete space, the topos of M-sets for any monoid M that is not a group, or the effective topos. (To be fair, the effective topos was pretty much invented for the purpose of studying constructive mathematics, I think. But the other two classes of examples come from other branches of mathematics.)
I don't know exactly what you mean by an ‘intuitionistic topos’, but I don't know any class of toposes that people study such that every topos in that class has a subobject classifier with exactly three elements. I do know a class of toposes that people study such that every topos in that class has at least three elements. That's the class of nondegenerate non-two-valued toposes. Because if it's non-degenerate, the subobject classifier has more than 1 element, so if it's doesn't have exactly 2 elements (two-valued), then it must have more than 2 elements, hence at least 3. Perhaps you heard something like that?
But to tell the truth, the number of elements in the subobject classifier is really a red herring. The important question for whether excluded middle is validated or not is whether the topos is boolean, not whether it is two-valued. And there are toposes whose subobject classifiers have more than 2 elements which are boolean, and in which classical logic does apply. And conversely, there are toposes whose subobject classifiers have exactly two elements which are not boolean, and in them, classical logic does not apply.
Is boolean or not?
"In constructive mathematics we have" instead as "From the constructive internal nPOV, we have"
But this entry is about intuicionistic set theory, not necessarily about the topos "internal" model for an intuicinionistic set theory.
I agree with Harry in disliking "we" when talking about independent mathematical objects. I think we should have a view of human-independent collections of axiomatic systems, models etc. It is not our choice that some of them exist and some does not. All do. Thus "Actually, these two definitions are equivalent only if we accept the principle of excluded middle" I would change into "Actually, these two definitions agree in axiomatics with excluded middle" or whatever of that sort. You can have an outsider to the site who will think that schools of people are wondering which axiomatic is true, and into which they believe and so on. It looks like there is something unsure at the human level and this makes a newcomer unsure. I find much more expering when mathematicians consider mathematical structures as abstract eternal beings of eternal existence and owe them without putting their wishes explicitly into the story (like "At the end of the day we realize...-- I find this story about the end of the day empty-content filling with random words, and when I myself resort to such things in some conference lecture in hurry and confusion how to deliver the lecture well and accessible to the audience I feel bad after the talk...).
Zoran writes in part:
But this entry is about intuicionistic set theory
Well, this entry is about set theory in general, whether classical or constructive. It is true that I wrote it only because I wanted to write down how the phrase is meant constructively. (After all, we all know what a proper subset is!) But that doesn't mean that anything added to the page has to be about that, by any means.
I grew up reading John Baez, so I like the personal talk about what ‘we’ or ‘I’ or ‘you’ might do with a mathematical concept. I don't seriously object if somebody wants to change the language to something more impersonal, as in Zoran's comment. I didn't think that this was what Harry was talking about.
I am saying that when we use "we" (and neither "I" nor "you"), we are guiding the reader through the subject and letting him/her make up his own mind. "We" means "you and I" in any technical part of a book (infrequent remarks put at the end of a chapter are often times when the author can express his/her opinions). I think that this use of "we" has a very restricted appropriate context. I can't really describe it, but it's something like, we don't use "we" unless the reader will agree. "We" with the certainty of a rigorous proof or "we" when describing a definition is different than "we" when you're at a conference. If that didn't make much sense, I'm trying to get across when I think and don't think it's appropriate to use "we" rather than "one".
I did not mean and do not care about a difference between "we" and "one". The very fact that you get astray by such trivailities confirms exactly what I conssider the deficiency of mixing people with mathematics. If one talks people for the sake of bridging a gap to a newcomer, it is equally OK to say "I", and more frank than "we" if you want. I do not care about all that political correcteness. But I do care about not mixing people in final forms of extraction of the edifice of mathematics. It reminds me of forceful exercise sessions, competition subculture and other distractive features of the external discourse which the true mathematics and piece of mind are actually an escape from. Mathematical entities, beauty of perfection, mistery of abstract entiteis is what attracts me to math at least, not the seeming power of few learned procedures. John is a good and creative teacher and for the first crush course (what is a style and audience for large part of his exposition) it is OK to have the workbook format with the atmosphere of the class, and even have the entertainment in between, but this is not attractive as a final etalon of cleaned up mathematical discourse.
Statements about math stay in my memory. I feel them worty reflecting on with inner voice. They are like clean water for drinking. Maybe a sip of brandy is good up to wake up in the morning but it is mind-poluting in the clarity of the day. I know many of you will not agree, but I hope you understand the difference between the two kinds of discourse. Most stubs I write are in the form of cluttered and vague congllomerates of hints of something what should become mathematics in future version of the entries. But if I believed that the evolution does not have an ideal target eventually I would not do it.
Well this is getting very philosophical if the question is whether mathematical objects exist independently of humans! I think the entry looks fine.
The topos of simplicial sets is not Boolean, though it is two-valued.
I am not talking about this entry. I am talking in general. Somebody was complaining before I entered the discussion about "we" as it presupposes something about attitude of people about intuitionism. This PROVES that such style is in general ofetn distracting from the content. If the content is accurately described it does not mislead as for about what issues from human attitudes are relevant for the descrption to have certain kind of sense.
Existence of objects is not important. If we love certain art it is true in artistic sense. As a drive and attraction it is sufficient. I do not talk philosophy here, I think.
@ Urs: Is your keyboard messed up?
My keyboard is small, I am typing fast, I post without proof-reading, to save some time. Sorry for the mixed characters here and there.
Of course, Toby's writing is very beautiful in its abstract cleanliness and thoughtfullness, in general, much better than average writing of mine (even if we neglect my English). So the fact that we have slight disagreement on what the ideal is, I prefer in general his realization to mine. :)
@ Harry #16:
So are you saying that you might not agree with the statement
in constructive mathematics, we usually prefer the latter definition
from proper subset, where ‘we’ has a meaning that includes you personally? I mean, you might not think that this is the best way to write it, but surely it is true!
More explicitly: If you never do constructive mathematics, then it is vacuously true. And if you ever do constructive mathematics, then I expect that you too will usually prefer the latter definition. If you ever do constructive mathematics and prefer the former definition, then please let me know!
@ Zoran #21:
Thanks!
<div>
<blockquote>Well this is getting very philosophical if the question is whether mathematical objects exist independently of humans!</blockquote><br/><br/>Yes, a few of us are having a very interesting debate along those lines both on my <a href="http://quantummoxie.wordpress.com">personal blog</a> as well as over at the <a href="http://fqxi.org/community/forum/category/5">FQXi forums</a>. Jump into the debate if you're so inclined (no flaming please).
</div>
I feel like constructive mathematics as practiced by constructive mathematicians is philosophically opposed to mathematics and the sciences in general. Mathematics isn't a matter of which axioms you accept or don't, but rather the study of the formal consequences of axioms and combinations of axioms. If constructive mathematicians used this as their justification, then that is fine, but they've politicised it into an issue over whether an undecidable axiom is right or wrong, calling into question the value of the work of mathematicians from Euclid onwards. It follows from the fact that standard and intuitionistic set theory are equiconsistent that this is not an intellectually defensible position, and worse, it's not respectful to mathematicians who choose other axiom systems.
I see this philosophy as fundamentally opposed to the nPOV. It's not that I don't respect the study of constructive mathematics, but more that I think that associating the nLab with that philosophy is a mark on its reputation.
are you sure?? What about the truth of the statement "every surjection has a section"? Diaconescu's theorem shows that Choice implies excluded middle, so the statement can't be true in intuitionistic set theory.
Equiconsistent means that they have the same consistency strength.
http://plato.stanford.edu/entries/logic-intuitionistic/
(By the way, the statement is that every epimorphism of sets is split. Surjections are by definition (at least in Bourbaki) those maps that split on the (right? left?)
I think that pointing out which constructions work internally and when is very useful, and an intuitionistic/predicavist/and-so-on version of Set is a useful test case for working in more general topoi, pretopoi, Heyting categories etc.
Absolutely! I never denied that. I'm saying that I think it's important to draw a philosophical line in the sand to make sure that people understand that we care about constructive mathematics because it's interesting, not because everything else is wrong.
Mathematics isn't a matter of which axioms you accept or don't, but rather the study of the formal consequences of axioms and combinations of axioms.
That is itself a debatable philosophical proposition. I agree with it, mostly, but the old constructive mathematicians did not. Therefore, it did not follow for them that just because classical and constructive mathematics are equiconsistent, that either one is equally acceptable.
However, I think that's not really the point at issue, because I also agree with this:
... it's important to draw a philosophical line in the sand to make sure that people understand that we care about constructive mathematics because it's interesting, not because everything else is wrong.
Ideally, there would be a term with the same meaning as "constructive mathematics" but without the same philosophical connotations.
Ideally, there would be a term with the same meaning as "constructive mathematics" but without the same philosophical connotations.
We can make this ideal a reality with nothing more than willingness to invent a name and a week thinking of nothing else.
There is a term with the same meaning as ‘constructive mathematics’ but without the same philosophical connotations. That term is ‘constructive mathematics’.
If you've only seen constructive mathematics done by people who philosophically oppose the meaningfulness of classical mathematics, then that's too bad. But that is not what I am doing when I write about constructive mathematics in the nLab.
I am a mathematical pluaralist. I do not (never have, never will) claim that any investigation of consequences from axioms is invalid mathematics. Nevertheless, I am particularly interested in what consequences may result from weak axiom systems (often ones with philosophical motivation, although that is not the only motivation), so I write about this on the nLab.
If you want to remove that or hide it behind inappropriate wording, then you are the one who has a philosphical objection to part of mathematics, not me. Don't project your prejudices on me in reverse!
<div>
<blockquote><br/>I feel like constructive mathematics as practiced by constructive mathematicians is philosophically opposed to mathematics and the sciences in general.<br/></blockquote><br/><br/>I'm going to play devil's advocate here for a moment (because, ultimately, I agree with you). Many scientists are empiricists and they require very specifically "repeatable" evidence in order to believe something is true. If mathematical objects are inherently related in some non-representational way to certain physical objects (i.e. they are inseparable from the physical objects), one could easily say many of these scientists are constructivist. The case that comes immediately to mind (but may not be the best example) is string theory which has, lately, taken a beating in certain circles for the lack of experimental evidence to support it. <br/><br/>And, in a sense, one major problem I have with it is that certain aspects of it are inherently non-testable and I prefer to be grounded in reality as much as possible (since I'm a physicist). Nevertheless, it seems as if I could devise a simple example or two that would undermine the constructivist viewpoint (though, by the very nature of the problem, you could never prove they were wrong).
</div>
@Toby: I guess should have said "ideally, there would be a term with the same meaning as 'constructive mathematics' but which has none of the same philosophical connotations for anybody." I never meant to imply that you, or any other particular person, oppose the meaningfulness of classical mathematics. But I think it's unfortunate that the only term we have to describe constructive mathematics makes some people think that we may be denying that meaningfulness, as Harry has demonstrated (#24).
Yes, I have never claimed that Toby denied the meaningfulness of standard mathematics, just that the "constructive mathematicians" did in the days of yore.
All right, well, if it's clear that doing constructive mathematics doesn't impugn the meaningfulness of classical mathematics (even though some practitioners of constructive mathematics did deny that meaningfulness), then is it OK to write ‘In constructive mathematics, we […]’?
This would all have my stamp of full approval if we put a little note at the top of the constructive mathematics page explaining the nPOV on the subject, but it's really not my decision to make. So, no pressure to do it, but I figured I'd at least voice my preference on the matter.
if we put a little note at the top of the constructive mathematics page explaining the nPOV on the subject,
I suggested this before: somebody here who cares about constructivism, please write an nPOV note about it and link to it from wherever it derserves to be linked.
I expanded the introductory paragraphs at constructive mathematics a bit to make this clearer.
I like it if Toby is okay with it!
Thanks, Mike. I added a link to internal logic.
I don't see how anybody who read constructive mathematics as it was would come to the conclusion that the Lab believed that classical mathematics was inferior. Nevertheless, I am pleased with what Mike has written, and I'm glad that this discussion led to it.
I added a bit on my own account about pluralism.
I agree that this is the POV from which constructive mathematics was already written, but I think it's good to have it explicitly and concisely right up-front, especially since the page then starts with a lengthly discussion of the origins and history. Thanks for your addition too.
1 to 41 of 41