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 finally wrote this: intuitionistic mathematics.
Good, recently I was equipping somebody else’s writings here with hyperlinks and didn’t know which entry the term “intuitionistic mathematics” should point to. I ended up making it point to intuitionistic logic.
I have added the floating TOC to your entry now.
Great. I looked a little at intuitionism and constructivism more generally around 20 years ago. It’s good to catch up again.
Is it worth saying something on what is coalgebraic about intuitionistic maths? I see i quoted there Bauer on fans and spreads as terminal coalgebras.
Is it worth saying something on what is coalgebraic about intuitionistic maths?
My ideas on that are pretty vague, but at least I can link to that comment in the article.
I’ve started to edit the page intuitionistic mathematics, as Urs asked me to. What I’m trying to do is give a short but really precise description of the essential features. So far I’ve only tackled the first section ’Idea’, I intend to continue from there but would appreciate some feedback on what I’ve written so far.
Thanks, Frank! I like it.
But I hope the other regulars who are more expert than me on these matters will give you some feedback, and maybe interact with the editing of the entry.
I don’t know very much about Brouwer’s intuitionism, so I don’t have much to say there. My main concern is that no reader should be led to identify Brouwer’s intuitionism with constructive mathematics in general, and I think that with a long Idea section first it is too late to wait until the “Terminology” section to address this, so I added a standout box at the beginning.
By the way, why the term “intuitionistic”? Who brought it up? Was that Brouwer? This would deserve a comment in the Idea section. Especially since the amount of explanation that intuitionistic mathematics requires is in contrast to what the term might suggest, namely that it appeals to our intuition. (But I gather Brouwer’s point would be that it does appeal to intuition more than classical mathematics. Even more so, this would be nice to discuss.)
Actually, I think it would be better just to give Brouwer’s ideas on intuitionism its own section, and not go into that in the Idea section. If we could keep the Idea section relatively short and to the point, it would help.
Thanks Frank! (For those interested, Frank Waaldijk is my older academic brother).
Quick comments, will try to add more next week if necessary. The link to computability should be explicitly to K2, or type II, computability, as explained on computability.
The work of adding choice sequences to NuPrl PDF may be the closest we have to an intuitionistic type theory.
I am not sure whether this has been made completely precise, but troubles with function sets in INT are related to the fact that topological spaces are not cartesian closed. nice category of spaces.
Bridges and Richman in Variaties of Constructive mathematics discuss INT, RUSS and CLASS, and BISH a neutral core. Perhaps, this can be brought out in constructivism.
“Intuition” goes back to Kant and the French semi-intuitionists (Borel, Lebesgue, …). See Stanford encyclopia of philosophy
I made some of these edits now. The page constructivism seems a bit crowded, as it also includes finite+mathematics#finitism. I suggest to move that material there.
Thanks. Where you have the external link to an article it would be better to instead list this article in the list of reference at the bottom of the entry, equip it with an anchor, and point to that. That’s more informative (the reader may see the author and title of the article without having to follow a link) and more robust (the external link might break).
(NB added in 2021 following the thread merger mentioned in #30: This comment originally followed #4.) Just came across this thread while looking for something else. The relation to coalgebras and streams processors is well-understood. eating trees. Does that fit with what you have in mind?
I think I was wondering if there was something more ’philosophical’ to say. I see you joined in that discussion at the Café. I guess I was wondering if anything coalgebraic was to be seen in Brouwer’s thinking.
How about the ’Second act of Intuitionism’?
Brouwer’s second act of intuitionism gives rise to choice sequences, that provide certain infinite sets with properties that are unacceptable from a classical point of view. A choice sequence is an infinite sequence of numbers (or finite objects) created by the free will. The sequence could be determined by a law or algorithm, such as the sequence consisting of only zeros, or of the prime numbers in increasing order, in which case we speak of a lawlike sequence, or it could not be subject to any law, in which case it is called lawless. Lawless sequences could for example be created by the repeated throw of a coin, or by asking the creating subject to choose the successive numbers of the sequence one by one, allowing it to choose any number to its liking. Thus a lawless sequence is ever unfinished, and the only available information about it at any stage in time is the initial segment of the sequence created thus far. Clearly, by the very nature of lawlessness we can never decide whether its values will coincide with a sequence that is lawlike. Also, the free will is able to create sequences that start out as lawlike, but for which at a certain point the law might be lifted and the process of free choice takes over to generate the succeeding numbers, or vice versa. (SEP: Intuitionism)
Are these not streams?
I moved some references from intuitionistic mathematics to constructive mathematics because as far as I could see they were not at all about Brouwerian intuitionistic mathematics but rather about constructive mathematics more generally (though sometimes using the label “intuitionistic”).
Is the Kleeny-Vesley topos really about intuitionistic mathematics in Brouwer’s sense?
Thanks.
I just happened to be reading Brower’s cambridge lectures, and it occurred to me that he seems to use qualifiers like “lawlike” and “predeterminate” like a (comonadic) modality. Which makes sense when thinking about how in spatial/cohesive type theory the function with domain don’t have to be “continuous”, and similarly how in intuitionistic mathematics it’s the presence of the non-lawlike objects (free choice sequences) that’s supposed to force things to be continuous. Has anyone tried to formalize Brouwerian intuitionistic mathematics using a modality like this?
Is that the intuitionist intuition? That only continuous constructions can cope with non-lawlike objects? Why?
From the latter
the modal logic for local maps in the case of RT(A,A#) and RT(A#) can be seen as a modal logic for computability
where RT(A,A#) is a realizability topos
which one intuitively can think of as having “continous objects and computable morphisms”
Has Per Martin-Löf tied together his work on algorithmic randomness and on constructive type theory?
The words “lawlike” and “predeterminate” don’t appear when searching either of those theses. Can you point to where they discuss intuitionistic mathematics?
I’m looking for an actual discussion of how such modalities relate to Brouwer’s intuitionistic mathematics.
The relation between lawlike and computable is made for instance in Kreisel and Troelstra - elimination of choice sequences. This work has later been connected to continuous truth. The relation between realizability and sheaf models has been made by Awodey and Bauer. I am not sure all the dots have been connected though. I don’t know of any work directly relating modal logic and lawlike sequences.
It may be unnecessarily confusing to try to make the connection between sheaf-models-of-choice-sequences and sheaf-toposes-for-realizability in the sense of Awodey and Bauer. Sheaf models of choice sequences are about taking sheaves over either some space or some category of well-behaved spaces, and using the resulting toposes to study the relationship between lawlike and non-lawlike operations and objects; this is the tradition of Fourman (“continuous truth”), Troelstra, many others, etc. In these sheaf toposes, the non-constructive Brouwerian principles (like continuity, bar induction, fan theorem, etc.) hold.
The paper of Awodey and Bauer on the other hand uses sheaf toposes in a different way (i.e. not over a notion of space whose open sets give finitary data about choice sequences), as a means to study general realizability: you render a PCA into a site, and obtain a Kripke-Joyal forcing semantics for realizability. One of the results is that you can embed the modest sets for the PCA into this grothendieck topos.
Now, in a very different line of research, others have studied a totally different connection between realizability and Brouwerian/continuous truth, which is where you basically “do realizability” over a space or some category of spaces. A purpose of doing this might be to connect Brouwer’s notion of truth, based on infinitary well-founded trees trees (and did not ever involve the notion of an algorithm in the sense formalized by a PCA, in apparent contradiction with the so-called BHK interpretation) with the BHK interpretation of intuitionistic truth.
added pointer to:
I have merged together three threads which all were to do with the page intuitionistic mathematics. The comments 5-12 comprised one of these threads.
The comments 1-4, 13-28 comprised the second of the threads. In fact comment 13 was originally made 45 minutes earlier than is now recorded on the server (at 03:59:16 server time), and actually came before comments 11 and 12, but I have moved it 45-ish minutes later (to 04:46:00) to make the merge cleaner.
The comment 29 was the only entry in the third thread, created earlier today.
There is also this relevant thread, but I’ll not merge this one in as it’s not exclusively to do with the page intuitionistic mathematics.
With regard to #5, Frank was referring to #14 in this thread I think.
Changing a link name to now point article for a topic that was previously previously (before 2020) non-existent.
Brouwer-Kripke scheme => Kripke’s schema
It seems both ways of writing it (BK resp just K) are still in use.
Related note: I think there’s many “schema”’s in math, but authors (mostly non-English authors I conjecture) like to write “scheme” for such “schema”’s (not to be confused with affine scheme type of schemes, etc.) I’m not 100% sure when the latter is appropriate (I’m Viennese myself), but I think “schema” is generally the right way to to in those situations.
added the missing list of original articles on formalizing intuitionism (all grabbed and polished-up from BHK interpretation, where their relevance is dubious):
Arend Heyting, Die formalen Regeln der intuitionistischen Logik. I, II, III. Sitzungsberichte der Preußischen Akademie der Wissenschaften, Physikalisch-Mathematische Klasse (1930) 42-56, 57-71, 158-169
abridged reprint in:
Karel Berka, Lothar Kreiser (eds.), Logik-Texte, De Gruyter (1986) 188-192 [doi:10.1515/9783112645826]
Arend Heyting, Die intuitionistische Grundlegung der Mathematik, Erkenntnis 2 (1931) 106-115 [jsotr:20011630, pdf]
Andrey Kolmogorov, Zur Deutung der intuitionistischen Logik, Math. Z. 35 (1932) 58-65 [doi:10.1007/BF01186549]
Hans Freudenthal, Zur intuitionistischen Deutung logischer Formeln, Comp. Math. 4 (1937) 112-116 [numdam:CM_1937__4__112_0]
Arend Heyting, Bemerkungen zu dem Aufsatz von Herrn Freudenthal “Zur intuitionistischen Deutung logischer Formeln”, Comp. Math. 4 (1937) 117-118 [doi:CM_1937__4__117_0]
L. E. J. Brouwer, Points and Spaces, Canadian Journal of Mathematics 6 (1954) 1-17 [doi:10.4153/CJM-1954-001-9]
Georg Kreisel, Section 2 of: Mathematical Logic, in T. Saaty et al. (ed.), Lectures on Modern Mathematics III, Wiley New York (1965) 95-195
added pointer to:
1 to 35 of 35