Intuitionist logic and the reals

[Hurkyl]

I'm thinking specifically of Brouwer's theorem that all functions R->R are continuous.

I know this isn't a theorem of intuitionist logic, because Boolean logic is a special case, and it's clearly not true in that framework.

My question is if there is a nice example of an intuitionist logic in which the theorem is true. I know that intuitionist logics can have interesting interpretations. For example, they might tell me "where" something is true, or maybe "how long" until something is true.


In Sheaves in Geometry and Logic, Saunders Mac Lane constructs a topos in which Brouwer's theorem is true. Unfortunately, I don't see a nice interpretation of it -- instead of being built upon a topological space, it's built upon the entire category of topological spaces! Unfortunately, I don't see a nice interpretation of the corresponding intuitionist logic.

Saunders Mac Lane mentions that there are lots of topoi in which Brouwer's theorem holds -- maybe the logic associated with one of them have a logic with some sort of natural interpretation?



Saunders Mac Lane prefaces the section on this by mentioning that Brower treated real numbers as "free choice sequences" -- a mathematician only has an incomplete information about a real number (which is really a Cauchy sequence). No concrete interpretation of this leaps out at me -- does someone know of an actual concrete intuitionist logic that corresponds to this?

 

[gilkesk]

just wondering if you have a BA in mathematics?

 

[JSuarez]

I think there is some confusion about a few things in your post:

I know this isn't a theorem of intuitionist logic, because Boolean logic is a special case, and it's clearly not true in that framework.

This is not true: from the phrasing, I wager that you're thinking of Heyting algebras and comparing them to Boolean ones. This is not (my opinion) the best way to think about logical issues, but that's not the problem: the continuity theorem you mention IS provable in Intuitionistic Analysis, which is a proper extension of Intuitionistic Logic with the axioms that define Brouwer's continuum (his model of the real line; on a side note, Brouwer was profoundly hostile to formal logic, and never formalized anything). Strictly speaking, the theorems of IL are the first-order sentences that are true in all Kripke models (as the theorems of classical, first-order, logic are the logically valid sentences).
The truth of the continuity theorem you mention is relative to Brouwer's model of the real line, and it's true there (as is false relative to the usual model); this is not about Boolean (I think you mean classical) or intuitionistic logic.

The fact is that Intuitionistic and Classical Logic are not two incompatible ways of thinking: the former emphasizes constructibility and effective proof; the latter truth, and both are connected by the Gödel-Glivenko translation, which states, roughly, that a sentence is intuitionistically provable iff its double negation is provable in classical logic (there's a little more to this).


I will not discuss topos interpretation because I think there is not much to it: it was proved some years ago, by Moerdijk, that topoi are redundant; they can be reduced to topological spaces.

Saunders Mac Lane prefaces the section on this by mentioning that Brower treated real numbers as "free choice sequences" -- a mathematician only has an incomplete information about a real number (which is really a Cauchy sequence).

That is not exactly true, either: there is much more to the Brouwer continuum than choice sequences; MacLane (and many others), never really understood intuitionism; more accurate and correct exegesis of Brouwer appeared only recently (mainly by Mark van Atten). But the real problem is your last sentence, where you state that a real number is a Cauchy sequence. Remember that we are talking here about models of the real numbers: if you accept the more usual model of Cauchy sequences (or Dedekind cuts), then you have discontinuous functions, continuous functions that are not uniformly continuous and a nondenumerable infinity of individual numbers that you cannot name by any finite means; if you accept Brouwer's model, then all functions are continuous, etc.

But this is all about models: nobody knows what a real number IS (or even if it exists in any meaningful sense).

 

[Hurkyl]

Alas, I can no longer remember why I was curious in this question three years ago.

I'm curious what precisely you mean by this:

it was proved some years ago, by Moerdijk, that topoi are redundant; they can be reduced to topological spaces.

And I have a comment:

if you accept the more usual model of Cauchy sequences (or Dedekind cuts), then you have discontinuous functions, continuous functions

In the example I was referring to, MacLane-Moerdijk construct a particular topos for which Brouwer's theorem is true for the Dedekind reals -- if, in the internal logic of this topos, we construct R as the object of Dedekind cuts on (Q, <), then every function R to R is continuous.

 

[JSuarez]

My apologies for the late response, by I was trying to track the Moerdijk's article, that I also read a few years ago, where he reduced (or so it seemed to me, at the time) a topos to a particular kind of topological space (therefore interpreting topos theory in set theory), but I can't find it. It's very possible that it was withdrawn and I am wrong in dismissing Topos theory, but it's really not my flavour of choice in Logic (I'm a logician).

Regarding your second comment, I don't remember that particular example (but I will check it; the last few days were a bit compressed), but it is possible to twist the internal language so that this happens; the question is if it's interesting to do so. In my opinion it's not; after all, you may have topological spaces with the trivial or discrete topology, but they are not particularly interesting.

 

[Hurkyl]

I believe there is a theorem that says something like

Every Grothendieck topos is (equivalent to) the classifying topos of a continuous groupoid.​

Is that what you were thinking of?

A continuous groupoid apparently being a groupoid object in the category of locales. I'm less sure what the classifying topos is -- although in the case of a group it's just the category of G-sets.

I haven't really thought that through (or gone digging for references), though maybe I should. It's certainly not a reduction to just sheaves on spaces because that cannot describe, e.g., the category of G-sets for a group G. But... maybe it amounts to choosing a space, a sheaf G of groups, and then looking at the corresponding category of sheaves with a G-action?




Anyways, I think you have reminded me why I asked my question!

(A correction to my description -- it wasn't the entire category of topological spaces, but instead any small, full subcategory T that contained R, the one-point space, and was closed under binary products, equalizers, and the taking of open subsets)


There is a natural way to view real numbers in this topos: they would be pairs (X,f) where X is a space in T and f is a continuous function X-->R.

(The real number object in this topos is the sheaf represented by R)


However, this doesn't seem to resemble any sort of free-choice sequence. Of course, I don't really know what those are supposed to be anyways, so that's not saying much.

So, I was wondering if there was some other topos for which you could view its real numbers in a way more obviously resembling free-choice sequences.



Edit: fixed an error in the stated theorem