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.
noticed that neither the entry intuitionistic mathematics nor the entry constructive mathematics even mentioned the entries type theory or setoid, for instance. I have now added these bare terms in the list of “related entries”, but maybe somebody feels like adding a little paragraph to these entries to do the issue justice?
These don't particularly fit into intuitionistic mathematics (intuitionistic logic would be different), and they were already linked from constructive mathematics.
I'm confused by where you put in the (duplicate) links to type theory and Bishop set; what are they classically equivalent to? These seem to belong under the foundational material, so I moved them there.
And I'm confused by your arrangement of the References. Bishop's book is perhaps the original work in his school, but not in constructive mathematics in general. I've moved it to the general references.
Okay, thanks for looking into it!
I still feel it would be desireable to add to the entries. Currently a novice reader will have little chance to come from these entries to the plethora of type theory entries that we have which are related.
I am aware that nobody is being paid for doing this, but on the off chance that you or anyone feels like giving it a go, this here would be my wish:
the entry intuitionistic mathematics should have not just an uncommented link to intuitionistic type theory, but should have a paragraph that says a bit about how intuitionistic type theory is a very well-developed chunk of intuitionistic mathematics that has good claims to serve as a useful foundations for mathematics.
Similarly for the entry on constructive mathematics.
I just think currently these entries don’t match well in their brevity with all the related stuff explored elsewhere on the nLab .
I think that intuitionistic mathematics, at least, looks better now.
Thanks!
coming back to the commented list that Toby had kindly created at intuitionistic mathematics:
should there be also a pointer to intuitionistic number theory?
in the bullet item “intuitionistic mathematics” at intuitionistic mathematics I have added the sentence
One example of intuitionistic mathematics (which nicely shows that intuitionism is not a matter of “belief” but of subject) is computable mathematics (see for instance Bauer 05, section 4.3.1).
There had been no references at intuitionistic mathematics. I have added some, briefly commented.
“Brouwer developed a very controversial style of mathematics and even logic” (citation needed). A few sentences below, you say the mathematics is not controversial. Why not link to e.g. the Stanford encyclopedia for a discussion of his philosophy ?
Intuitionistic Set Theory: do you mean the system IZF ?
What do you mean by weakly predicative?
Why is type theory a set theory ?
I don’t think Brouwer would have used a pretopos, the Kleene-Vesley system makes a good attempt at formalizing Brouwer’s mathematical foundations.
On the relation between set theory and topology. This recent paper by Mike Fourman makes them precise. I would add it, but it probably deserves a page “Continuous Truth” on its own, combined with elimination of choice sequences.
I think Toby had a lot to do with the writing of the article, and so obviously he should be the one to respond. But I doubt he or anyone would object to linking to SEP; you should just put it in.
I don’t think Brouwer would have used a pretopos, the Kleene-Vesley system makes a good attempt at formalizing Brouwer’s mathematical foundations.
Obviously not, since the notion of pretopos wasn’t available in his time. :-) Sometimes the nLab adopts an nPOV to develop modern conceptual niches for modern readers. Could you explain more specifically what about a pretopos conceptual explanation Brouwer would find objectionable? (Of course the Kleene-Vesley system was also given in the references.)
Again, you can add the Fourman reference without fear of controversy, and no one would object to a page on “continuous truth” (I don’t know his paper, but connections between constructivity and continuity would seem to be familiar ground. I am probably not the best one to consult for this; Toby might be better placed.)
Yes, Bas, please make obvious non-controversial improvements to entries right away, and then announce here. Even potentially somewhat controversial additions, if not outrageous, I would suggest to put into the entry with due discussion and then announce here. Then we can all jump on it and edit further until things converge. (If they don’t converge, we can always “roll back” and no harm will have been done.)
As opposed to SEP articles which I guess are first finalized and then uploaded, nLab articles are mostly all “under construction”. (Which is great, I think, because it makes eventually for very efficient collection of information).
The analog in finalization state of SEP articles is more what we once envisioned to be at nLab-reviewed and Publications of the nLab. In fact, I guess we are still envisioning this (I am) but for lack of manpower these projects have been dormant for a while now…
By the way, recently I had started a stub on Kleene-Vesley topos. If you could cross-link with that more or even expand it more, that would be greatly appreciated.
I made some small changes and created Continuous Truth. I think I was too quick about the pretopos, this would probably be accepted.
About #11, I think I would leave this under realizability and let the “topos” just follow from the general realizability topos. Kleene-Vesley did not do topos theory.
It is common to refer to the “Kleene-Vesley topos”, notably so in Jaap van Oosten’s standard monograph on realizability, page 279. So if it is being referred to, it deserves to have an entry.
OK. Let’s follow Jaap.
Intuitionistic Set Theory: do you mean the system IZF ?
I mean any set theory called ‘intuitionistic’, such as IZF.
What do you mean by weakly predicative?
With function sets but without power sets. I'll make weakly predicative mathematics redirect to predicative mathematics and explain it there.
Why is type theory a set theory ?
No idea. Probably a typo (or a copy-and-pasto).
The page on predicative mathematics looks nice, I don’t have the time to read it carefully now. Peter Aczel makes the distinction “predicative” to mean Feferman predicative () and generalized predicative for the stronger Martin-Lof, or constructive set theories mentioned here. E.g. MLM would be considered generalized predicative, I think. I once heard it described as anything that admits and ordinal analysis.
In the proof theory community,
It can be a bit confusing that systems of strength are termed predicatively reducible when rather they represent the limit of what is predicatively reducible. But typically they are not finitely axiomatizable, so any one particular sentence (say, in arithmetic) provable in such is predicatively provable.
Note also that function sets are only impredicative classically when functions are identified with their graphs (otherwise we may have for instance recursion theoretic interpretations of functions and then quantifying over them is not impredicative).
I might try to update predicative mathematics if there is interest.
I might try to update predicative mathematics if there is interest.
Please consider doing so!
Ulrik, yes, it would be nice if you could do so. There are a number of subtleties when working constructively. E.g. is predicative in type theory.
If you could clearly define what even ’predicative given the totality of natural numbers’ means, then that would be helpful right there. The terms ’generalized predicative’ and ’weakly predicative’ are met in constructive mathematics, where there is (as I see it, which is reflected in the article as currently written) a very different sense of what ’predicative’ means than in the classical proof-theory community. But if I could get a definition, then maybe we could see better how they relate.
Ulrick, as you probably know constructivity seems curcial here, both in connection with higher toposes, see Mike’s post and in connection with geometric type theory. Geometric type theory does not include the power set. Urs suggests that this is connected to geometric homotopy types, but I am not sure I have seen the details. Urs, where you thinking about Mike’s post?
Urs, I’ll get to in a couple of days, I think.
Bas, I agree that some notion of constructivity is crucial, but that is already present in the very conception of predicativity. What I mean is, predicatively, definitions can serve as a construction of what is being defined, whereas impredicatively, definitions always merely single out some object which is already presumed present. (I think this is what Poincaré had in mind when he introduced the vicious circle principle (1906), but I don’t claim to know precisely what conception of predicativity either Poincaré or Russell had).
Toby, there are a number of different ways of defining “predicative given the totality of the natural numbers”: There is the classical analysis in terms of the ramified hierarchy, but you might object that it relies too closely on the classical conception of ordinal. Then there is the unfolding analysis (Gödel’s program for new axioms, Section 3; see also Appendix A of my thesis). In terms of a subsystem of second order arithmetic, you can take -CA plus the bar rule.
I’m afraid any proposed formal definition will be open to attack. In that sense perhaps predicativity is similar to constructivism. But at least a number of proposed definitions converge at the same level of proof-theoretic strength.
By chance there is a thread on predicativity in constructive maths on the constructive news mailing-list right now. If Ulrik does not include it in his rewrite, I’ll add some stuff.
Some kind soul pointed out to me that there is something in the Phenomenology of Spirit that sounds a whole lot like a complaint about mathematical proof not being (regarded as) constructive and about lack of proof relevance. I have added the quote with pointers to the very bottom of constructive mathematics (please see there):
section 12 Historical and mathematical proof of the Preface: All the same, while proof is essential in the case of mathematical knowledge, it still does not have the significance and nature of being a moment in the result itself; the proof is over when we get the result, and has disappeared. The process of mathematical proof does not belong to the object; it is a function that takes place outside the matter in hand.
footnote 42: Mathematical truths are not thought to be known unless proved true. Their demonstrations are not, however, kept as parts of what they prove, but are only our subjective means towards knowing the latter. In philosophy, however, consequences always form part of the essence made manifest in them, which returns to itself in such expressions.
also created proof relevance
Re #25, there’s an older history of the idea that a proof can get at the essence of the issue or not. In particularly, proof by contradiction was seen as not getting at the ’cause’ of the result. There’s plenty on this in Mancosu’s book.
Thanks! Maybe you could add a comment to the entry?
OK. I added that comment.
Thanks! I have copied it also into proof relevance.
(brief suggestion for relevant additions to constructive mathematics, or perhaps even a new article; no intent on my part to do so any time soon, just in case there is someone out there who likes to do so and is happy to be reminded of there being some sort of under-emphasis in this regard; this is very important, and familiar-to-all-mathematicians, kind of topic: the suggestion is to recognizably treat on the nLab, in particular in a constructive-mathematics-informed way and with a slant towards category theory, what is known various noun phrases as “proof by exhaustion”, “proof by cases”, “proof by case analysis”, “case distinction”, “Fallunterscheidung”. We do not currently have a dedicated treatment of this.]
Fallunterscheidung is not familiar-to-me. Your other suggestions seem to all be synonyms. It may be worth highlighting at excluded middle that EM generalises to non-binary case analysis. Also relevant is decidable object; any problem parameterised by a decidable object in a reasonable category admits case analysis over that object (eg odd and even natural numbers, but not positive, negative and zero reals).
Fallunterscheidung is nothing but the German word for “case distinction”.
1 to 33 of 33