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.
1 to 13 of 13
Recently in an edit of mine Frank Waaldijk found it necessary (here) to replace “intuitionistic” by “constructive”. This alerted me that it would be nice if the distinction were made a bit more transparent in the respective Lab entries. Presently our “constructive logic” simply redirects to “intuitionistic logic”. And while we do have separate entries for “constructive mathematics” and “intuitionistic mathematics”, I find it hard to extract from them their distinction.
I am not going to edit on these matters. This is an alert and a request to the logic experts around here. Maybe if you have some spare energy, it would be worthwhile to improve on this situation of Lab entries a little.
Some people insist that “intuitionistic mathematics” refer to Brouwerian intuitionism, which includes axioms that contradict classical logic; but other people use “intuitionistic” to mean the same as what in other contexts is called “constructive”, i.e. mathematics without excluded middle or choice but nothing added that contradicts them. Some people (particularly material set theorists) use “constructive” to mean predicative constructive and “intuitionistic” to mean impredicative constructive. So in my opinion there really is no consensus on what the distinction is, if any.
Thanks, Mike. It would still be nice if this situation were reflected in the Lab entries. Maybe I’ll copy over what you just wrote.
I went ahead and edited the Idea-sections at intuitionistic mathematics, constructive mathematics and at intuitionistic logic, following your paragraph in #2.
The distinction between these words is well established in certain fields but inconsistent across fields. Specifically:
The article intuitionistic mathematics already has a Terminology section that explains all of this in detail. (Which I guess you saw, Urs, since you linked it from your warning box.)
I’m inclined to follow Toby’s lead on this (#5), and intend to incorporate a succinct but clear disambiguation page/paragraph on the use of ’intuitionism’ and ’intuitionistic’ (in philosophy there is also the term ’ethical intuitionism’…).
’Intuitionistic mathematics’: I have only seen this used to refer specifically to Brouwer’s conception of constructive mathematics. Often the abbreviation INT is used, to indicate this reference. INT contains notably one axiom (or axiom-like insight if you prefer to not formalize, like Brouwer) that conflicts with classical mathematics (CLASS)1, involving ’continuous choice’. But INT also incorporates the classically true Bar Theorem (axiom) which in some aspects brings it closer to CLASS than ’neutral’ constructive mathematics.
’Intuitionistic logic’: arises from classical logic by dropping tertium non datur (excluded middle). It is therefore a part of both intuitionistic mathematics and classical mathematics. However, the constructive interpretation of the logical connectives and quantifiers (for example ) merits a good exposition, for instance to explain why intuitionistic logic is useful in computer science.
’Intuitionistic set theory’ is used to refer to a version of axiomatic set theory called IZF, developed by Myhill starting from ZF and using intuitionistic logic. I’m not really familiar with it, but it contains the full power set axiom which is far too impredicative to be acceptable in INT. The name is therefore quite a misnomer. Peter Aczel removed the impredicativity and called the result CZF.
(To be continued on the discussion page of intuitionistic mathematics)
One may safely ignore the ’fringe’ axiom called Kripke’s Scheme (KS), it is generally not useful and hard to justify in a precise way.] ↩
This sounds like “intuitionistic mathematics” is different from “mathematics using intuitionistic logic”. Is this true? Is this wise?
This needs an extra big alert box then. (What a profoundly bad choice of terminology. Who is responsible for this?)
It´s actually quite explainable, from the classical-mathematics point of view. Like I said, intuitionistic logic is a part of classical logic, with very nice properties. So from the classical point of view it makes perfect sense to study classical structures using only intuitionistic logic, and such research is carried out (I believe) quite lively today. [For a classical structure P, one should not call the result of such a study ’intuitionistic P’. But this happens, especially since often only intuitionistic logic is taught, without the context of intuitionistic mathematics].
Intuitionistic mathematics (INT) however holds strong (predicative) views on what kind of structures can be really considered meaningful. The study of impredicative classical structures with intuitionistic logic makes little sense in INT.
Nonetheless, most formal systems (classical or intuitionistic) have clear axioms and deduction rules which are acceptable to any mathematician. ZFC as a formal system is perfectly acceptable in INT, and likewise FIM (intuitionistic mathematics’ formalization system) is perfectly acceptable in classical mathematics.
The differences/discussions/disputes… are all about the interpretation, meaning, meaningfulness and ’worthiness’ of these formal systems. To an intuitionistic mathematician, ZFC does not reflect an accurate picture of mathematics (even though FIM can be modeled/coded perfectly in ZFC). Likewise, to a classical mathematician FIM makes no sense (even though ZFC can be modeled perfectly within FIM).
Brouwer maintained that formalization is only a part of mathematics (and he considered it a sterile part, one that can capture the essence nor the scope), and this was one factor in his dispute with Hilbert. Most mathematicians prefer a kind of mathematics that is not completely formalized, but do so ’knowing’ that a ’solid’ formalization (ZFC or other) is possible.
Brouwer’s views on the incompleteness of formalization, already stated and explained very well on a meta-level in his PhD thesis (1907), were vindicated by Gödel.
Still, there is today to my knowledge no natural intuitionistic theorem that cannot be formalized in FIM. If I understand correctly Harvey Friedman has been working for years on finding a ’natural’ classical statement/theorem of arithmetic that escapes formalization in ZFC.
My personal conclusion is that Brouwer and Hilbert both had very strong points… :-)
Frank, can you provide a reference for FIM? (I mean other than Kleene & Vesley passim, preferably something online that lists the axioms and rules.)
Regarding FIM. It is mentioned in the stanford encyclopedia. There are a number of pay-walled references by Kleene. An open reference is here. Joan Rand Moschovakis was Kleene’s student at the time and she is still developing the system in the context of reverse+mathematics#constructive_reverse_mathematics.
1 to 13 of 13