Not signed in (Sign In)

Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry goodwillie-calculus graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology newpage nforum nlab noncommutative noncommutative-geometry number-theory object of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeNov 26th 2010

    I finally wrote this: intuitionistic mathematics.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 26th 2010
    • (edited Nov 26th 2010)

    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.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 26th 2010

    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.

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeNov 26th 2010

    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.

    • CommentRowNumber5.
    • CommentAuthorspitters
    • CommentTimeMay 9th 2017

    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?

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 9th 2017
    • (edited May 9th 2017)

    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?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeApr 10th 2019

    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?

    diff, v30, current

    • CommentRowNumber8.
    • CommentAuthorspitters
    • CommentTimeApr 10th 2019
    Of course KV did not use topos theory, but they did try to capture Brouwerian mathematics (not unsuccessfully, I think).
    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeApr 11th 2019


    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 A\flat A 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?

    • CommentRowNumber10.
    • CommentAuthoratmacen
    • CommentTimeApr 11th 2019

    Is that the intuitionist intuition? That only continuous constructions can cope with non-lawlike objects? Why?

    • CommentRowNumber11.
    • CommentAuthorspitters
    • CommentTimeApr 12th 2019
    Yes, such modalities have been studied in the [thesis]( of Andrej Bauer and the [thesis]( of Lars Birkedal. Both were advised by Dana Scott.
    This was later connected to the logic of local toposes by Awodey and Birkedal; see modal type theory.
    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 12th 2019

    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”

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 12th 2019
    • (edited Apr 12th 2019)

    Has Per Martin-Löf tied together his work on algorithmic randomness and on constructive type theory?

    • CommentRowNumber14.
    • CommentAuthorspitters
    • CommentTimeApr 12th 2019
    In his thesis, Per developed constructive measure theory inspired by Brouwer. This was the beginning of his work on algorithmic randomness.
    He has often linked the type theory and measure theory, but I don't know whether he ever made a formal connection.
    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeApr 12th 2019

    The words “lawlike” and “predeterminate” don’t appear when searching either of those theses. Can you point to where they discuss intuitionistic mathematics?

    • CommentRowNumber16.
    • CommentAuthorspitters
    • CommentTimeApr 12th 2019
    As in the quote in #12, one can read lawlike as computable.
    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeApr 12th 2019

    I’m looking for an actual discussion of how such modalities relate to Brouwer’s intuitionistic mathematics.

    • CommentRowNumber18.
    • CommentAuthorspitters
    • CommentTimeApr 13th 2019

    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.

    • CommentRowNumber19.
    • CommentAuthorjonsterling
    • CommentTimeApr 16th 2019

    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.

    • CommentRowNumber20.
    • CommentAuthorspitters
    • CommentTimeApr 17th 2019
    I was thinking about e.g. example 2.18 of Awodey/Bauer. Kleene-Vesley realizability embeds into sheaves over Baire space.

    The "different line of research" is NuPrl-like? It would be useful if you added references. Perhaps even to intuitionistic mathematics or constructive mathematics.
Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)