12
$\begingroup$

In Introduction to Higher-Order Categorical Logic, Lambek & Scott remark that Brouwer's Theorem (all functions $\mathbb{R}\to\mathbb{R}$ are continuous) holds in the free topos $\mathcal{T}$.

EDIT: L&S do not say that it holds in the free topos, they are incorrectly quoted as saying this in the nLab.

Let me present a naïve syllogism which is bothering me:

  1. The free topos is the initial object in the category of toposes & logical morphisms / nLab
  2. Logical morphisms preserve truth of sentences in the internal language of toposes. / nLab
  3. Brouwer's theorem is false in the topos of sets $\mathbf{Set}$.
  4. By (1) there is a logical morphism $\mathcal{T}\to\mathbf{Set}$ whence by (2) Brouwer's theorem should hold in $\mathbf{Set}$, which is not the case.

Therefore, I think I have misinterpreted something. Is the claimed theorem (attributed to Joyal by Lambek & Scott) really that Brouwer's Theorem holds internally to $\mathcal{T}$ (i.e. as a statement in the internal language of $\mathcal{T}$)?

Or could it be that it holds externally of the functions defined in $\mathcal{T}$ or something? The latter case sounds plausible, because we can certainly show that the definable functions in extensional type theory are continuous, but we cannot do this internally for certain important reasons (I believe Beeson's Foundations of Constructive Mathematics explains why—later, Escardó and Xu have established this also for intensional type theory).

Thanks to anyone who can help demystify this for me.

$\endgroup$
  • 1
    $\begingroup$ Do you have a page no for Lambek/Scott? $\endgroup$ – Jonas Frey Mar 15 '17 at 3:24
  • 1
    $\begingroup$ My guess is that Brouwer's theorem is not a statement in the internal language. $\endgroup$ – Qiaochu Yuan Mar 15 '17 at 3:24
  • $\begingroup$ @JonasFrey It is mentioned (attributed to Joyal, apparently unpublished) in the preface on page viii, but I cannot find a statement of the theorem or proof elsewhere in the book. $\endgroup$ – Jonathan Sterling Mar 15 '17 at 3:27
  • 1
    $\begingroup$ I think it is what you write in the last paragraph. LS do not say that that the statement "all endomorphisms on R are continuous" holds, but that all arrows on R "represent continuous functions", which is a more external statement. $\endgroup$ – Jonas Frey Mar 15 '17 at 3:34
  • 1
    $\begingroup$ Jonathan, thanks for asking! Please also consider making a note of your edit at the nForum: nforum.ncatlab.org/discussions/?CategoryID=0 $\endgroup$ – Todd Trimble Mar 15 '17 at 3:57
6
$\begingroup$

To summarize, the Lambek and Scott book actually says that functions on the reals in the free topos represent continuous functions. The nLab previously made the stronger claim that Brouwer's Theorem holds in the free topos (which is not the case for the reasons I described), but I have edited the page appropriately.

$\endgroup$
  • 1
    $\begingroup$ Thanks @DavidRoberts! MO will let me do so in about 22 hours :) $\endgroup$ – Jonathan Sterling Mar 16 '17 at 4:53
5
$\begingroup$

Dear All: you must be precise on what you mean by Brouwer's theorem. The free topos is closed under many rules, but unlike the realizability topos, it is seldom closed under the internal implicative statement. Thus the free topos is closed under Church's rule (see the original paper by Lambek and me on Intuitionist type theory and the free topos, JPAA (1980), but obviously not the internal Church's theorem. The statement about Brouwer's principle (an original beautiful sketch of a proof, due to Joyal, but never published) is in LS, p. viii (Introduction). Here is the version you would want: using an appropriate version of the reals, if |-- f: R-->R (is provable in higher order int. logic) then |-- "f is continuous" . And, by the way, of course this is formalizable in the internal logic. For a reasonable proof, similar continuity rules were formalized and proved by Susumu Hayashi for second order logics and type theories in the 1970's. There are some versions of this also in Troelstra's SLN344 (the "bible" of such formalizations). Phil Scott

$\endgroup$
  • $\begingroup$ Welcome to MathOverflow! Gerhard "Looking Forward To More Postings" Paseman, 2017.03.15. $\endgroup$ – Gerhard Paseman Mar 15 '17 at 20:01
  • 1
    $\begingroup$ Hello @PhilipScott! You can't meant that the meta-theorem "if $\vdash f : R \to R$ then $\vdash \text{$f$ continuous}$ is formalizable in the internal logic. It's not an internal statement. $\endgroup$ – Andrej Bauer Mar 15 '17 at 20:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.