Introduction to Synthetic Mathematics (part 1)

February 26, 2015

Introduction to Synthetic Mathematics (part 1)

Posted by Mike Shulman

$MathML-enabled post (click for more details).$

John is writing about “concepts of sameness” for Elaine Landry’s book Category Theory for the Working Philosopher, and has been posting some of his thoughts and drafts. I’m writing for the same book about homotopy type theory / univalent foundations; but since HoTT/UF will also make a guest appearance in John’s and David Corfield’s chapters, and one aspect of it (univalence) is central to Steve Awodey’s chapter, I had to decide what aspect of it to emphasize in my chapter.

My current plan is to focus on HoTT/UF as a synthetic theory of $\infty$ -groupoids. But in order to say what that even means, I felt that I needed to start with a brief introduction about the phrase “synthetic theory”, which may not be familiar. Right now, my current draft of that “introduction” is more than half the allotted length of my chapter; so clearly it’ll need to be trimmed! But I thought I would go ahead and post some parts of it in its current form; so here goes.

$MathML-enabled post (click for more details).$

In general, mathematical theories can be classified as analytic or synthetic. An analytic theory is one that analyzes, or breaks down, its objects of study, revealing them as put together out of simpler things, just as complex molecules are put together out of protons, neutrons, and electrons. For example, analytic geometry analyzes the plane geometry of points, lines, etc. in terms of real numbers: points are ordered pairs of real numbers, lines are sets of points, etc. Mathematically, the basic objects of an analytic theory are defined in terms of those of some other theory.

By contrast, a synthetic theory is one that synthesizes, or puts together, a conception of its basic objects based on their expected relationships and behavior. For example, synthetic geometry is more like the geometry of Euclid: points and lines are essentially undefined terms, given meaning by the axioms that specify what we can do with them (e.g. two points determine a unique line). (Although Euclid himself attempted to define “point” and “line”, modern mathematicians generally consider this a mistake, and regard Euclid’s “definitions” (like “a point is that which has no part”) as fairly meaningless.) Mathematically, a synthetic theory is a formal system governed by rules or axioms. Synthetic mathematics can be regarded as analogous to foundational physics, where a concept like the electromagnetic field is not “put together” out of anything simpler: it just is, and behaves in a certain way.

The distinction between analytic and synthetic dates back at least to Hilbert, who used the words “genetic” and “axiomatic” respectively. At one level, we can say that modern mathematics is characterized by a rich interplay between analytic and synthetic — although most mathematicians would speak instead of definitions and examples. For instance, a modern geometer might define “a geometry” to satisfy Euclid’s axioms, and then work synthetically with those axioms; but she would also construct examples of such “geometries” analytically, such as with ordered pairs of real numbers. This approach was pioneered by Hilbert himself, who emphasized in particular that constructing an analytic example (or model) proves the consistency of the synthetic theory.

However, at a deeper level, almost all of modern mathematics is analytic, because it is all analyzed into set theory. Our modern geometer would not actually state her axioms the way that Euclid did; she would instead define a geometry to be a set $P$ of points together with a set $L$ of lines and a subset of $P\times L$ representing the “incidence” relation, etc. From this perspective, the only truly undefined term in mathematics is “set”, and the only truly synthetic theory is Zermelo–Fraenkel set theory (ZFC).

This use of set theory as the common foundation for mathematics is, of course, of 20th century vintage, and overall it has been a tremendous step forwards. Practically, it provides a common language and a powerful basic toolset for all mathematicians. Foundationally, it ensures that all of mathematics is consistent relative to set theory. (Hilbert’s dream of an absolute consistency proof is generally considered to have been demolished by Gödel’s incompleteness theorem.) And philosophically, it supplies a consistent ontology for mathematics, and a context in which to ask metamathematical questions.

However, ZFC is not the only theory that can be used in this way. While not every synthetic theory is rich enough to allow all of mathematics to be encoded in it, set theory is by no means unique in possessing such richness. One possible variation is to use a different sort of set theory like ETCS, in which the elements of a set are “featureless points” that are merely distinguished from each other, rather than labeled individually by the elaborate hierarchical membership structures of ZFC. Either sort of “set” suffices just as well for foundational purposes, and moreover each can be interpreted into the other.

However, we are now concerned with more radical possibilities. A paradigmatic example is topology. In modern “analytic topology”, a “space” is defined to be a set of points equipped with a collection of subsets called open, which describe how the points vary continuously into each other. (Most analytic topologists, being unaware of synthetic topology, would call their subject simply “topology.”) By contrast, in synthetic topology we postulate instead an axiomatic theory, on the same ontological level as ZFC, whose basic objects are spaces rather than sets.

Of course, by saying that the basic objects “are” spaces we do not mean that they are sets equipped with open subsets. Instead we mean that “space” is an undefined word, and the rules of the theory cause these “spaces” to behave more or less like we expect spaces to behave. In particular, synthetic spaces have open subsets (or, more accurately, open subspaces), but they are not defined by specifying a set together with a collection of open subsets.

It turns out that synthetic topology, like synthetic set theory (ZFC), is rich enough to encode all of mathematics. There is one trivial sense in which this is true: among all analytic spaces we find the subclass of indiscrete ones, in which the only open subsets are the empty set and the whole space. A notion of “indiscrete space” can also be defined in synthetic topology, and the collection of such spaces forms a universe of ETCS-like sets (we’ll come back to these in later installments). Thus we could use them to encode mathematics, entirely ignoring the rest of the synthetic theory of spaces. (The same could be said about the discrete spaces, in which every subset is open; but these are harder (though not impossible) to define and work with synthetically. The relation between the discrete and indiscrete spaces, and how they sit inside the synthetic theory of spaces, is central to the synthetic theory of cohesion, which I believe David is going to mention in his chapter about the philosophy of geometry.)

However, a less boring approach is to construct the objects of mathematics directly as spaces. How does this work? It turns out that the basic constructions on sets that we use to build (say) the set of real numbers have close analogues that act on spaces. Thus, in synthetic topology we can use these constructions to build the space of real numbers directly. If our system of synthetic topology is set up well, then the resulting space will behave like the analytic space of real numbers (the one that is defined by first constructing the mere set of real numbers and then equipping it with the unions of open intervals as its topology).

The next question is, why would we want to do mathematics this way? There are a lot of reasons, but right now I believe they can be classified into three sorts: modularity, philosophy, and pragmatism. (If you can think of other reasons that I’m forgetting, please mention them in the comments!)

By “modularity” I mean the same thing as does a programmer: even if we believe that spaces are ultimately built analytically out of sets, it is often useful to isolate their fundamental properties and work with those abstractly. One advantage of this is generality. For instance, any theorem proven in Euclid’s “neutral geometry” (i.e. without using the parallel postulate) is true not only in the model of ordered pairs of real numbers, but also in the various non-Euclidean geometries. Similarly, a theorem proven in synthetic topology may be true not only about ordinary topological spaces, but also about other variant theories such as topological sheaves, smooth spaces, etc. As always in mathematics, if we state only the assumptions we need, our theorems become more general.

Even if we only care about one model of our synthetic theory, modularity can still make our lives easier, because a synthetic theory can formally encapsulate common lemmas or styles of argument that in an analytic theory we would have to be constantly proving by hand. For example, just as every object in synthetic topology is “topological”, every “function” between them automatically preserves this topology (is “continuous”). Thus, in synthetic topology every function $\mathbb{R}\to \mathbb{R}$ is automatically continuous; all proofs of continuity have been “packaged up” into the single proof that analytic topology is a model of synthetic topology. (We can still speak about discontinuous functions too, if we want to; we just have to re-topologize $\mathbb{R}$ indiscretely first. Thus, synthetic topology reverses the situation of analytic topology: discontinuous functions are harder to talk about than continuous ones.)

By contrast to the argument from modularity, an argument from philosophy is a claim that the basic objects of mathematics really are, or really should be, those of some particular synthetic theory. Nowadays it is hard to find mathematicians who hold such opinions (except with respect to set theory), but historically we can find them taking part in the great foundational debates of the early 20th century. It is admittedly dangerous to make any precise claims in modern mathematical language about the beliefs of mathematicians 100 years ago, but I think it is justified to say that in hindsight, one of the points of contention in the great foundational debates was which synthetic theory should be used as the foundation for mathematics, or in other words what kind of thing the basic objects of mathematics should be. Of course, this was not visible to the participants, among other reasons because many of them used the same words (such as “set”) for the basic objects of their theories. (Another reason is that among the points at issue was the very idea that a foundation of mathematics should be built on precisely defined rules or axioms, which today most mathematicians take for granted.) But from a modern perspective, we can see that (for instance) Brouwer’s intuitionism is actually a form of synthetic topology, while Markov’s constructive recursive mathematics is a form of “synthetic computability theory”.

In these cases, the motivation for choosing such synthetic theories was clearly largely philosophical. The Russian constructivists designed their theory the way they did because they believed that everything should be computable. Similarly, Brouwer’s intuitionism can be said to be motivated by a philosophical belief that everything in mathematics should be continuous.

(I wish I could write more about the latter, because it’s really interesting. The main thing that makes Brouwerian intuitionism non-classical is choice sequences: infinite sequences in which each element can be “freely chosen” by a “creating subject” rather than being supplied by a rule. The concrete conclusion Brouwer drew from this is that any operation on such sequences must be calculable, at least in stages, using only finite initial segments, since we can’t ask the creating subject to make an infinite number of choices all at once. But this means exactly that any such operation must be continuous with respect to a suitable topology on the space of sequences. It also connects nicely with the idea of open sets as “observations” or “verifiable statements” that was mentioned in another thread. However, from the perspective of my chapter for the book, the purpose of this introduction is to lay the groundwork for discussing HoTT/UF as a synthetic theory of $\infty$ -groupoids, and Brouwerian intuitionism would be a substantial digression.)

Finally, there are arguments from pragmatism. Whereas the modularist believes that the basic objects of mathematics are actually sets, and the philosophist believes that they are actually spaces (or whatever), the pragmatist says that they could be anything: there’s no need to commit to a single choice. Why do we do mathematics, anyway? One reason is because we find it interesting or beautiful. But all synthetic theories may be equally interesting and beautiful (at least to someone), so we may as well study them as long as we enjoy it.

Another reason we study mathematics is because it has some application outside of itself, e.g. to theories of the physical world. Now it may happen that all the mathematical objects that arise in some application happen to be (say) spaces. (This is arguably true of fundamental physics. Similarly, in applications to computer science, all objects that arise may happen to be computable.) In this case, why not just base our application on a synthetic theory that is good enough for the purpose, thereby gaining many of the advantages of modularity, but without caring about how or whether our theory can be modeled in set theory?

It is interesting to consider applying this perspective to other application domains. For instance, we also speak of sets outside of a purely mathematical framework, to describe collections of physical objects and mental acts of categorization; could we use spaces in the same way? Might collections of objects and thoughts automatically come with a topological structure by virtue of how they are constructed, like the real numbers do? I think this also starts to seem quite natural when we imagine topology in terms of “observations” or “verifiable statetments”. Again, saying any more about that in my chapter would be a substantial digression; but I’d be interested to hear any thoughts about it in the comments here!

Posted at February 26, 2015 6:15 AM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2809

50 Comments & 0 Trackbacks

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I think your argument from pragmatism (“any consistent axiomatization could be interesting”) undersells HoTT/UF. The point is that there is a large and growing community of mathematicians who find this style of argument to be personally appealing. In this sense HoTT/UF is an active mathematical sub-discipline like any other, supported by a community of researchers who think it’s cool. (Here I’m making no distinction between sub-disciplines that are traditionally regarded as more “problem-solving” than “theory-building.” Even for the problem solvers, the question of whether a particular collection of problems is interesting persists.)

I’m really taken by your claim that ZFC is the only remaining synthetic mathematical theory, at least from the perspective of the standard foundations. Of course this is very far removed from common mathematical practice, particularly in higher category theory! A “model-independent” proof involving $(\infty,1)$ -categories frequently has the form “such and such is true in 1-category theory and such and such is true in homotopy theory, so by standard arguments we conclude our result.”

I might argue that my joint project with Dominic Verity, to redevelop the foundational category theory of $(\infty,n)$ -categories, is “relatively synthetic.” As we explain in a forthcoming paper, all of the basic categorical definitions and proofs are interpretable relative to a particular axiomatization that we introduce. (These axioms, which are ultimately defined using ZFC, are a subset of the axioms satisfied by the fibrant objects in a model category enriched over the Joyal model structure with all objects cofibrant.) Quasi-categories, (iterated) complete Segal spaces, and weak complicial sets all fit into such a “context” from which point the development of their basic category theory is “synthetic”, by which I mean agnostic to which of these varieties of $(\infty,n)$ -categories we are talking about.

Of course, a lot of category theory has exactly the same flavor. The introduction describes how several motivating examples are special cases of a new general definition, and then all the theorems are proven relative to the new axiomatization. (See e.g., Combinatorial categorical equivalences of Dold-Kan type.)

Posted by: Emily Riehl on February 26, 2015 9:59 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I think your argument from pragmatism undersells HoTT/UF

I haven’t even gotten to the part of the chapter where I talk about HoTT/UF yet! Right now I’m just talking about synthetic theories in general. Are you suggesting that I should put more emphasis on synthetic theories that are appreciated by a community of mathematicians, rather than suggesting that it’s okay to study a synthetic theory just because I personally may find it interesting or beautiful?

I’m really taken by your claim that ZFC is the only remaining synthetic mathematical theory, at least from the perspective of the standard foundations. Of course this is very far removed from common mathematical practice…!

I guess you are talking about the “two levels” of synthetic/analytic that I mentioned? As I said, at one level there is this rich interplay involving examples and abstractions, which arguably is one of the things that mathematics is all about. But nevertheless, in modern mathematics, even the “relatively synthetic” theories are generally all defined in terms of sets: a category is a set of objects with a set of morphisms, a fibration category is a category with extra structure, etc. etc.

Posted by: Mike Shulman on February 26, 2015 10:17 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Ah! I had read this:

The next question is, why would we want to do mathematics this way?

as referring to the synthetic topology of the previous paragraph, which I took to mean HoTT/UF. But maybe that was a misattribution.

Part of what I was talking about was the definitions/examples level of the synthetic/analytic dichotomy, but I was also intending a more pointed criticism of what might be seen as a trend toward synthetic reasoning in the absence of a clear axiomatic framework.

I worry that in certain areas of higher category theory there can be found “proofs by analogy”, which resemble classical proofs, but in their intended contexts cannot obviously expanded into a complete argument based upon set theoretical foundations. Quoting Voevodsky’s IAS slides:

A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.

Of course, in common practice, we never require a proof to be presented in the level of detail attempted in Principia Mathematica and for good reason: at some point, more detail obscures rather than facilitates human understanding of the argument. But in a newer field, such as higher category theory, there is always a potential concern that the community of practitioners hasn’t yet developed sufficient technical expertise to expand proof sketches into more rigorous arguments. This isn’t to say that there ultimately will be any problem with the current arguments. Mochizuki’s proof of the ABC conjecture seems to be a case where the argument is correct but few are able to understand what he has done.

But perhaps I have digressed from the dialectics you were intending to consider.

Posted by: Emily Riehl on February 27, 2015 2:53 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Ah, thank you! That means that if I do include any form of this in my chapter, I’ll need to be extra-clear that HoTT/UF has nothing to do with synthetic topology. HoTT/UF is a synthetic theory of $\infty$ -groupoids, which are totally different things from topological spaces.

I was using synthetic topology as an example because I wanted to discuss the general idea of what it would mean to use a synthetic foundational theory other than ZFC, and for that I thought it would be helpful to choose an example whose basic objects are something more familiar than $\infty$ -groupoids. But perhaps the potential confusion between $\infty$ -groupoids and topological spaces (due to accidents of the history of $\infty$ -groupoid theory, a.k.a. homotopy theory) means that this is not a good idea.

Unfortunately, there aren’t a whole lot of other good examples of synthetic foundational theories. There’s synthetic computability theory, but in that case when constructing an set-theoretic model the basic objects we need to use aren’t directly familiar things from analytic computability theory. Synthetic differential geometry has something of the same problem, plus it’s close to synthetic topology. Hmm.

I worry that in certain areas of higher category theory there can be found “proofs by analogy”, which resemble classical proofs, but in their intended contexts cannot obviously expanded into a complete argument based upon set theoretical foundations.

Ah, I see. Yes, I share that worry, and I also share also your hope that new frameworks like your project with Verity will help that situation. I think this is related to the point I made about the foundational debates:

among the points at issue was the very idea that a foundation of mathematics should be built on precisely defined rules or axioms, which today most mathematicians take for granted.

although at the definitions/examples level rather than the foundational level. I wasn’t planning to say any more about this issue in my chapter — it didn’t seem to have much to do with category theory in general or HoTT/UF in particular. But your point makes me wonder whether it actually does: since HoTT/UF is a precisely defined synthetic world for homotopy theory, it gives us a way to make precisely justified arguments that previously might have involved handwaving and analogy.

I wonder whether I can work that in somewhere. Maybe it falls under the “modularity” category of reasons to use a synthetic theory — if the “common lemmas” in an analytic subject are intuitively clear and technically tricky, people will start to omit to prove them at all.

Posted by: Mike Shulman on February 27, 2015 5:04 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

For the me most interesting synthetic theories are those which are not based on classical logic. This allows us to use axioms in the synthetic theory which are inconsistent with classical logic, e.g. differentials in synthetic differential geometry. Of course the model is usually build using classical logic.

I don’t know if this is widely known, but a good model of Brouwers intuitionism, where you can also do synthetic topology, is the function realizability topos. And indeed all functions between metric spaces in this topos (using Bishop’s constructive definition) are continuous.

Posted by: Martin Pape on February 27, 2015 4:22 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

You’re anticipating part 2! (-:

Posted by: Mike Shulman on February 27, 2015 6:47 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Just a quick comment: the following jarred somewhat!

But from a modern perspective, we can see that (for instance) Brouwer’s intuitionism is actually a form of synthetic topology

Whilst I see what you are getting at, this does not seem quite right.

In his Cambridge lectures on intuitionism, Brouwer writes of ‘two acts of intuitionism’. The ‘first act’ involves:

Completely separating mathematics from mathematical language and hence from the phenomena of language described by theoretical logic, recognising that intuitionistic mathematics is an essentially languageless activity of the mind…

He later writes of this ‘first act’:

mathematical creation by means of logical axioms is rejected

and

In the edifice of mathematical thought … language plays no part other than that of an efficient, but never infallible or exact, technique for memorising mathematical constructions, and for communicating them to others, so that mathematical language by itself can never create new mathematical systems.

However, he then writes (the italics are quoted, not my own):

But because of the highly logical character of this mathematical language the following question naturally presents itself: Suppose that, in mathematical language, trying to deal with an intuitionist mathematical operation, the figure of an application of one of the principles of classical logic is, for once, blindly formulated. Does this figure of language then accompany an actual languageless mathematical procedure in the actual mathematical system concerned?

A careful examination reveals that, briefly expressed, the answer is in the affirmative, as far as the principles of contradiction and syllogism are concerned, if one allows for the inevitable inadequacy of language as a mode of description and communication. But with regard to the principle of excluded third, except in special cases, the answer is in the negative, so that this principle cannot in general serve as an instrument for discovering new mathematical truths.

It may be perfectly true that ‘synthetic topology’ captures a formalisation of those principles of logical reasoning that Brouwer, as in this last quote, considers acceptable from an intuitionistic point of view, together with a formalisation of aspects of Brouwer’s ‘second act of intuitionism’ (this is where choice sequences enter).

However, the quotes make clear, in my opinion, that Brouwer would not have regarded intuitionism as defined by any formal system: not as any kind of synthetic mathematics in the sense you have in mind. I don’t see that a modern perspective changes this!

Posted by: Richard Williamson on March 1, 2015 8:10 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I agree entirely that Brouwer would not have regarded intuitionism as defined by any formal system! (In particular, I mentioned while discussing the argument from modularity that “among the points at issue was the very idea that a foundation of mathematics should be built on precisely defined rules or axioms”.) Thanks for your feedback; I should revise the text to make it clear that I’m not claiming this. What I mean to claim is that from a modern perspective, the concrete mathematics that Brouwer did (which stands on its own independently of his own philosophical views about it) can be regarded as a form of synthetic topology.

Posted by: Mike Shulman on March 1, 2015 9:33 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

In relation to both the philosophy and synthetic mathematics related to the work of Brouwer you might want to look at Fourman’s work on the gross topos on the category of separable locales.

Posted by: Bas Spitters on March 2, 2015 12:27 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

What I mean to claim is that from a modern perspective, the concrete mathematics that Brouwer did (which stands on its own independently of his own philosophical views about it) can be regarded as a form of synthetic topology.

Indeed!

This is still a strong statement as you put it, though! I do not have enough of an overview of Brouwer’s work to make a judgement either way as to whether the full strength of this claim is reasonable. It also depends upon exactly what you mean by ‘synthetic topology’. But, for example, the formalisation of Brouwer’s ‘second act of intuitionism’ (which he uses mathematically to justify the aspects of his work that you refer to) in the paper of Fourman that Bas linked to (thank you, I had not seen this paper before!) is intended, it seems to me at a glance, to be thought of as passing from ‘synthetic constructive set theory’ to ‘synthetic topology’. It would seem a stretch to regard this too as ‘a form of synthetic topology’.

Posted by: Richard Williamson on March 2, 2015 6:45 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I don’t quite understand your point. The only really nonclassical principle I’m aware of that Brouwer used says more or less literally that every function $N^N \to N$ is continuous with respect to the standard topology on $N^N$ . So it seems to me that at a mathematical level, any mathematics developed based on this principle is a fortoiri synthetic topology.

A separate question is to what extent Brouwer’s thought processes can be connected to topology. I think there are things to say here too, as I implied in the post: e.g. if we think of an open set as a statement about points that can be verified by an observation with finite precision, then continuity relates very directly to Brouwer’s justification for his continuity principle in terms of the existence of “choice sequences” being selected unpredictably by a creating subject, about which we can never know more than a finite amount. I’ve read that van Dalen also referred to Brouwer’s intuitionism as “a topologist’s constructivism”, although I’ve never tracked down the exact reference. However, all of that is secondary to the purely mathematical question.

Posted by: Mike Shulman on March 2, 2015 8:05 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

My ‘Indeed!’ was not intended as an exclamation of surprise, but rather something like: ‘I agree that this seems closer to expressing what you had in mind’!

So it seems to me that at a mathematical level, any mathematics developed based on this principle is a fortoiri synthetic topology.

Yes, I think that is reasonable.

What I was reacting to is that the following is rather a sweeping statement.

What I mean to claim is that from a modern perspective, the concrete mathematics that Brouwer did (which stands on its own independently of his own philosophical views about it) can be regarded as a form of synthetic topology

If you are closely acquainted with all of Brouwer’s work and feel that you can justify this claim, then of course you are entitled to make it. Otherwise, or perhaps in any case, it might be preferable to restrict to something more specific, as you did in the following, rather than make the sweeping statement above in passing.

The only really nonclassical principle I’m aware of that Brouwer used says more or less literally that every function $N^{N} \rightarrow N$ is continuous with respect to the standard topology on $N^{N}$ . So it seems to me that at a mathematical level, any mathematics developed based on this principle is a fortoiri synthetic topology.

As I wrote, I do not feel well enough acquainted with Brouwer’s work to make a firm, reasoned judgement either way about the ‘sweeping statement’, but my instinct from the little I have read is that it is an oversimplification, and could thereby be misleading.

Regarding what I wrote about the ‘second act of intuitionism’: I intended this and its consequences to be an example of Brouwer’s mathematics that does not seem to be ‘synthetic topology’ in the sense that, from the last quote, I think you have in mind. In the second to fourth paragraphs of the introduction to his paper, Fourman writes that his intention is to express formally this ‘second act of intuitionism’ in such a way that a continuity principle can be derived. I have no idea (I have not thought about it at all) to what extent the mathematics in Fourman’s paper can be considered to fulfill this goal, but it is at least clear that he regards aspects of Brouwer’s mathematical work as laying the foundations for ‘synthetic topology’: that is what I was getting at when I wrote that Fourman seems to be investigating the passage from ‘synthetic constructive set theory’ to ‘synthetic topology’ in Brouwer’s mathematics.

My impression from the Cambridge lectures is similarly that an aspect of Brouwer’s mathematics is to lay the foundations for the ‘continuity principle’, rather than take it as given. But, as I say, I wouldn’t feel that I know this work well enough to wish to defend this point of view in detail.

Posted by: Richard Williamson on March 3, 2015 7:39 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

No, of course I’m not closely acquainted with all of Brouwer’s work. But I assumed that if he had introduced any other nonclassical principle, then it would have been mentioned in some of the secondary sources I’ve read, such as Troelstra & van Dalen, or Bishop & Bridges, or Hesseling. I don’t fully understand what the “second act of intuitionism” was supposed to mean, but Fourman’s quotation seems to express it as a sort of philosophical position; so if it didn’t lead to any other mathematical consequences then I still think my statement is justified.

Posted by: Mike Shulman on March 3, 2015 4:12 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

My impression is that the ‘second act of intuitionism’ is more of a fundamental foundational principle for mathematics. Its justification will be philosophical, but this is the case for the assumptions and principles in any foundations.

I have browsed a little more in some secondary sources to see if others have shared my feeling that to characterise the consequences of the ‘second act of intuitionism’ simply as ‘all functions from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ are continuous’ is an oversimplification, and that its consequences are wider and more profound.

What I have seen has indeed strengthened my feeling in that regard. From the Cambridge lectures, without having worked through them in detail, I got the impression that Brouwer had explored an intuitionistic analogue of set theory, of which synthetic topology is only a part. Others, for example Dummett in Elements of intuitionism, have indeed argued that Brouwer’s notion of ‘species’ is exactly of this nature. This set theory is significantly different from the classical one: there is a distinction between ‘intensional’ and ‘extensional’ equality of species, and on the whole it strikes me as closer to type theory àla Martin-Löf than ordinary set theory (and this is almost certainly not a coincidence, I feel it highly likely that there must have been an influence upon Martin-Löf’s thinking). Indeed, I found it remarkable the extent to which this seems to be the case.

As a specific example of something that makes use of the ‘second act of intuitionism’ but does not rely on the continuity principle: Dummett gives a proof of the ‘fan theorem’ via the ‘bar principle’, which proof he takes care to emphasise does not require the continuity principle. This ‘fan theorem’ still concerns, or can be viewed as concerning, something ‘topological’, but this is not surprising: the focus of Brouwer’s work is on establishing that it is possible to work effectively with the real numbers in intuitionistic mathematics.

My overall impression now is that the ‘second act of intuitionism’ could justify all kinds of mathematics which has a different flavour from classical mathematics, as with Martin-Löf type theory, and that Brouwer himself does make a start on such a mathematical endeavour, even if his own principle focus was on the real numbers.

On a different note, to clear up possible confusion: what I wrote in my last comment about a continuity principle being derived was to do with the principle akin to ‘all functions from the reals to the reals are continuous’, not the one about functions from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ being continuous. It seems to me that the former is really the heart of a ‘synthetic topology’: it follows from the latter, but at least in Dummett’s presentation, the proof makes use of species as well, and thus it does seem meaningful to regard it as derived rather than given.

I have also seen it argued that the ‘functions from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ are continuous’ principle requires justification/proof in some sense, and seen such a justification/proof on intuistionistic grounds attempted, even if Brouwer took it as given. One can imagine that it might be possible and interesting to find a mathematical formulation of such reasoning: after all, Brouwer will no doubt have had a justification for the principle, and it would seem to me consistent with the essence of intuitionism to argue that such justification is mathematics, even if we do not yet have a way to formalise it.

Posted by: Richard Williamson on March 3, 2015 8:42 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

What if I clarify my claim further to “the concrete mathematics that Brouwer did and that a modern mathematician would regard as ‘mathematics’ can be regarded as a form of synthetic topology”? The way I see it, a “principle” is not precise enough to be considered mathematics, and I still haven’t seen any examples of mathematics that Brouwer claimed to derive from this principle but that can’t be considered synthetic topology.

Also I don’t see why a continuity principle regarding $R$ is any more or less a part of synthetic topology than a continuity principle regarding $N^N$ . Indeed, there are theories I would call synthetic topology in which not every function $N^N\to N$ is continuous (e.g. sheaves on a big site of locally connected spaces), and I wouldn’t be surprised if there are also theories I would call synthetic topology in which not every function $R\to R$ is continuous. (Certainly it depends on what you mean by $R$ as well, e.g. in the aforementioned sheaf model there are discontinuous endomorphisms of the Cauchy reals, though not the Dedekind reals.)

In any case, though, your objections have made me recognize that I should be very careful what I write in the paper, because I don’t want to produce this reaction in any reader! The point of the chapter is to talk about HoTT/UF, not make any contentious claim about Brouwerian intuitionism. So to that extent, at least, I concede the point. (-:

(By the way, based on what I’ve learned from the comments on this post, I am also currently planning to reorganize my plans for the chapter to such an extent that the next installment will not be “part 2” but rather “part 1, take 2”. Unfortunately circumstances are conspiring against me, so I don’t know when I will manage to actually write it.)

Posted by: Mike Shulman on March 3, 2015 10:12 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

What if I clarify my claim further to “the concrete mathematics that Brouwer did and that a modern mathematician would regard as ‘mathematics’ can be regarded as a form of synthetic topology”?

Alas, my remarks would be unchanged! I have been trying to point to aspects of Brouwer’s work that I do regard as mathematics, and which I do not regard as naturally being able to be considered as a form of synthetic topology.

I don’t have a great deal to add to what I have already written: it seems to me that Brouwer’s work on ‘species’ is interesting mathematics, and is not naturally a part of synthetic topology; and I think that the fan theorem in Dummett’s book is a specific example of a theorem in Brouwer’s work that is not naturally a part of synthetic topology in the sense that I thought you had in mind. This fan theorem may be able to be interpreted as asserting something topological, but that does not, in my view at least, necessarily mean that it is proven or even expressed within synthetic topology.

I don’t wish to enter into a terminological debate about ‘synthetic topology’! One interpretation is that there is a formalisation of some gadgets which we think of ‘topological spaces’ and some gadgets which we think of as ‘continuous maps’. There is no way in such a formal system to speak of anything which is not a continuous map. The gadgets in this formal system might not necessarily correspond to all topological spaces as we think of them in the usual set theoretic way, or on the other hand there might be more of these gadgets. But my point was that I would regard it as essential, at the heart of any ‘synthetic topology’, that there is a gadget corresponding to $\mathbb{R}$ or, better, the unit interval. Putting all this together, we arrive at what I wrote: it is at the heart of any ‘synthetic topology’ that ‘all maps from $\mathbb{R}$ to $\mathbb{R}$ are continuous’. I do not regard the continuity principle regarding maps from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ as at the heart of ‘synthetic topology’ in the same way.

To emphasise this point further: my opinion is that it could reasonably be argued that ‘synthetic topology’ begins with a formal system as I just described together with some gadget corresponding to $\mathbb{R}$ . If one has to derive the fact that all maps from $\mathbb{R}$ to $\mathbb{R}$ are continuous, this would, most naturally, it seems to me, be thought of as ‘outside synthetic topology’.

But as I say, no doubt there could be many other interpretations of synthetic topology, and many other opinions as to what gadgets it must contain, and how they should be related to one another.

In any case, though, your objections have made me recognize that I should be very careful what I write in the paper, because I don’t want to produce this reaction in any reader! The point of the chapter is to talk about HoTT/UF, not make any contentious claim about Brouwerian intuitionism.

By the way, based on what I’ve learned from the comments on this post, I am also currently planning to reorganize my plans for the chapter to such an extent that the next installment will not be “part 2” but rather “part 1, take 2”

I hope that you do not feel obliged to do so on my account! I was reacting to only one sentence, which didn’t seem quite right to me personally, but maybe the vast majority of readers would be happy with it and not consider it contentious; and you might judge that is fine in the context of the rest of your essay to make the point in this way (you will never be able to satisfy everyone!). Perhaps a footnote/endnote or something to elaborate upon the point would work perfectly well, if you wish to address it all.

Posted by: Richard Williamson on March 4, 2015 8:26 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I guess the difference is that we just have very different ideas of what “synthetic topology” means. To me, synthetic topology is, as I said, a rich enough system that all of mathematics can be developed in it. Therefore, just the fact that some piece of mathematics doesn’t “look like topology” says nothing about whether or not it could be part of a mathematics built on synthetic topology. It might, for instance, live in the sub-universe of indiscrete spaces inside synthetic topology. Or it might be about objects that do (in synthetic topology) turn out to have nontrivial topological structure, but that topology plays no noticeable role in the theory. None of that excludes it from being a part of a mathematics whose foundation is synthetic topology, just like the absence of (say) well-orderings doesn’t exclude a subject from being part of a mathematics built on ZFC (which is, arguably, really a synthetic theory of well-founded relations). So the examples of species and the fan theorem are, to me, not at all counterexamples to the claim that Brouwer’s mathematics can be seen as founded on synthetic topology, whether or not they “look like topology”.

Moreover, this is the specific point about synthetic foundational theories that I was trying to get across! So if I failed to communicate it, then I should at least think about rewriting to give it the correct emphasis.

(Regarding specific gadgets that must exist in synthetic topology: I would indeed be a bit disappointed if something called “synthetic topology” didn’t include something to play the role of $R$ , but I don’t think I would demand that that object necessarily be the one constructed inside the theory using Dedekind cuts, nor that every endomorphism of it be continuous in the $\epsilon$ - $\delta$ -sense expressed inside the theory (as opposed to the intrinsic sense in which every map in a synthetic-topological-theory is continuous). And whether or not that continuity is postulated or proven is, to me, just a question about which axioms it is more convenient to start from; perhaps interesting to discuss over lunch, but not affecting the substance of the resulting theory.)

Posted by: Mike Shulman on March 4, 2015 8:57 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Ah, then I indeed completely misunderstood what you had in mind! I agree that with a sufficiently rich ‘synthetic topology’, one could develop topology, and many other things, ‘internally to that system’: in other words, one could have both the ‘foundational’ gadgets that we think of as topological spaces and continuous maps, and ‘internally constructed’ ones. This reminds me a little of our discussion about the meaning of the homotopy hypothesis in homotopy type theory!

But do I understand correctly from your last comment that your claim is that Brouwer’s mathematics can be developed ‘internally’ to some notion of synthetic topology? That ‘species’ (and their intensional/extensional notions of equality), and thereby a Brouwerian definition of $\mathbb{R}$ using species, can be defined internally in synthetic topology? For me that would be remarkable, and I would very much like to see and understand the details: it is not at all obvious to me! What is it about synthetic topology as a formal system that allows for this?

What I thought you were asserting was that ‘synthetic topology’ as a formal system can be thought of as capturing Brouwer’s mathematics, in an analogous way to which synthetic differential geometry as a formal system is intended to capture differential geometry: in other words, that the axiomatics of synthetic topology as a formal system can somehow be seen to ensure that the mathematics developed inside it is precisely that which is intuitionistic in the Brouwerian sense. This is why I was pointing to things in Brouwer’s mathematics that are prior to continuity principles of various kinds.

It is of course very different to say, as I now understand you to be saying, that there is some way to develop Brouwerian mathematics internally to synthetic topology: one could presumably make this statement about very many different kinds of mathematics, so I then don’t quite follow why one should draw attention to Brouwerian mathematics in this regard (even though, as above, I would find it very interesting to see how it is possible to develop Brouwerian mathematics in this way)? Or is the point precisely an affirmative answer to my questions above: that there is something about synthetic topology that allows one to develop all of Brouwerian mathematics internally, that would not be possible in a formal system which lacks some aspects of synthetic topology as a formal system?

Regarding specific gadgets that must exist in synthetic topology: I would indeed be a bit disappointed if something called “synthetic topology‘“didn’t include something to play the role of $\mathbb{R}$ , but I don’t think I would demand that that object necessarily be the one constructed inside the theory using Dedekind cuts, nor that every endomorphism of it be continuous in the $\epsilon$ - $\delta$ -sense expressed inside the theory (as opposed to the intrinsic sense in which every map in a synthetic-topological-theory is continuous).

I agree entirely.

And whether or not that continuity is postulated or proven is, to me, just a question about which axioms it is more convenient to start from; perhaps interesting to discuss over lunch, but not affecting the substance of the resulting theory.

I didn’t quite follow this. My point was that, for me, in a good synthetic theory of topology, one should be able to use the foundational $\mathbb{R}$ , for which all endomorphisms are continuous just because of the way in which the formal theory is set up, for all the purposes to which one puts $\mathbb{R}$ in set theoretic topology which one is interested in. This would indeed, for me, be the whole point of such a synthetic theory. There need not be a way to construct an ‘internal $\mathbb{R}$ ’ by Dedekind cuts or any other method, and even if there is, and in addition there is a way to define an internal notion of continuity, then I would not regard the ‘internal topology’ built upon these gadgets as ‘synthetic topology’ any more (of course it would be synthetic topology in one sense, namely carried out within a formal system that can be thought of as synthetic topology, but it would not be synthetic topology in the sense that it is the investigation of some primitive notions of topological space and continuity).

Posted by: Richard Williamson on March 4, 2015 2:40 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

What I meant to say is that those nonclassical aspects of Brouwer’s mathematics — the ones that distinguish it from “pure” or “neutral” constructive mathematics, in the same way that the Kock-Lawvere axiom distinguishes SDG, and the axioms of excluded middle and choice distinguish classical mathematics — are the same as those that might appear in a theory constructed to be a “synthetic topology”. In particular:

there is something about synthetic topology that allows one to develop all of Brouwerian mathematics internally, that would not be possible in a formal system which lacks some aspects of synthetic topology as a formal system?

Yes. The continuity principles that Brouwer derives from “choice sequences” are precisely the sort of nonclassical axioms that appear in synthetic topology. They are false in other formal systems, such as classical mathematics.

As for “species”, possibly I don’t understand what you think Brouwer meant by a “species”. The definitions of it that I’ve seen look just like he is saying it’s an extensional predicate, which I would expect to be able to represent in any system at all. None of the books I’ve read that discussed Brouwer’s intuitionism mentioned anything interesting called a species. Can you point me to somewhere that describes what you think Brouwer meant by it, in language a modern mathematician can understand?

I didn’t quite follow this.

You said “If one has to derive the fact that all maps from $\mathbb{R}$ to $\mathbb{R}$ are continuous, this would, most naturally, it seems to me, be thought of as ‘outside synthetic topology’.” I was saying that I don’t see any substantial difference between whether this fact is derived (i.e. proven) from some other nonclassical axiom, or take as an axiom itself (which you seemed to be insisting on), as long as the resulting system is the same.

Posted by: Mike Shulman on March 4, 2015 5:54 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Can you point me to somewhere that describes what you think Brouwer meant by it, in language a modern mathematician can understand?

Perhaps pg.38-39 (at least in the 1978 reprint which I have access to) of Dummett’s Elements of intuitionism would be a good place to look to begin with. These pages are quite early on in section 2.2, entitled ‘Real numbers’.

I was saying that I don’t see any substantial difference between whether this fact is derived (i.e. proven) from some other nonclassical axiom, or take as an axiom itself (which you seemed to be insisting on), as long as the resulting system is the same.

I completely disagree! I would regard it as the essence of a synthetic approach to anything to think carefully about the axiomatics: the whole point is to capture directly the objects and properties one is interested in. To ask that ‘the resulting system is the same’ is a very strong requirement. If one has to derive that endomorphisms of $\mathbb{R}$ are continuous in one’s synthetic topology, then I would be extremely doubtful that such a theory is the same as one in which this fact is an axiom.

Regarding the rest of your comment: perhaps I can try to summarise what I think are our points of view. Am I correct that your claim is as follows?

1) One of the axioms that distinguishes synthetic topology as a formal system is that ‘all functions are continuous”.

2) In such a system, we in particular have that all maps from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ are continuous.

3) This corresponds to being able to construct choice sequences in Brouwerian mathematics.

4) Thus any ‘ordinary mathematics’ together with the use of choice sequences can be formalised in synthetic topology.

5) Being able to construct choice sequences is the only significant aspect of Brouwerian mathematics that is not classical (constructive) mathematics.

6) Putting 1) - 5) together: all of Brouwerian mathematics can be formalised in synthetic topology. It is 1) that ultimately makes this possible.

My points of contention are with 4) and 5), and one additional point about this argument as a whole.

Regarding 4): it is not at all evident to me that this is a valid conclusion, or indeed evident what precisely it means in practise. It seems to me to depend upon the precise axiomatics of one’s synthetic topology: in particular, how the ‘ordinary (let me say discrete) mathematics’ living inside it and the ‘non-discrete mathematics’ formalising choice sequences interact. At least, it seems to me that this conclusion needs careful justification.

Regarding 5): this is the main point we have been discussing.

Regarding the argument as a whole: even if there was no dispute over the argument’s validity, it doesn’t seem right to me to draw from it the conclusion that Brouwerian mathematics is a form of synthetic topology. It would be true to say that it can be formalised within (or internally to) a form of synthetic topology, and that it is the precise axiomatics of synthetic topology that allow for this. But to say that Brouwerian mathematics is a form of synthetic topology would, for me, be to say that the axiomatics of this synthetic topology precisely capture Brouwerian mathematics, as discussed in my previous comment. I wouldn’t have thought that one can just ‘throw away’ all the non-discrete part of synthetic topology except that needed in 2)?

Posted by: Richard Williamson on March 4, 2015 7:58 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I would regard it as the essence of a synthetic approach to anything to think carefully about the axiomatics: the whole point is to capture directly the objects and properties one is interested in.

I’m not sure in what sense those two statements are related by the colon: two theories with different-looking axiomatics can of course capture exactly the same objects and properties. Think e.g. of Boolean algebras and Boolean rings.

This reminds me of the old discussion about what is a theory. When we say that two theories are “the same”, do we mean they are the same presentation by rules and axioms, or they have the same models? I would say that the “objects and properties” are an invariant of the class of models, i.e. an invariant of “Morita equivalence” of theories, rather than depending on the specific presentation of a theory. Hence, I would argue that a property of a theory like “being a form of synthetic topology” is also an invariant under Morita equivalence, hence not depending on the particular axiomatization.

Regarding (4), the “ordinary” and “non-discrete” mathematics inside synthetic topology aren’t “separate worlds”. For instance, the object $N^N$ in the statement “all functions $N^N\to N$ are continuous” is (from the perspective of the theory) the ordinary set of functions from $N$ to $N$ . So the “ordinary” mathematics doesn’t have to live in the special world of “discrete” objects; it looks, well, ordinary, but we also have additional continuity properties coming from synthetic topology, in the same way that Brouwer used choice sequences to prove things about the set of real numbers (say). There is no interaction to worry about.

Regarding (5), thanks for the reference. It however confirms my impression that “species” is just another word for a predicate (or perhaps the extension of that predicate), I guess with some extra stratified-predicativity restriction imposed. The synthetic theories that I’m most interested in are forms of type theory in which any predicate has an extension, and they are naturally predicative in the sense that we have a hierarchy of universes; but if that isn’t predicative enough then one could easily restrict to a subcollection of the predicates to call “species”.

Finally, regarding your point about the argument as a whole, my use of the phrase “synthetic topology” is expansive enough to include “subtheories” as long as they include some of the distinctive features. If Brouwerian mathematics “embeds” into some theory of synthetic topology, and includes some distinctive topological features of that theory (such as continuity principles), then it is a fortiori also a form of synthetic topology.

Posted by: Mike Shulman on March 5, 2015 6:08 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I’m not sure in what sense those two statements are related by the colon: two theories with different-looking axiomatics can of course capture exactly the same objects and properties.

Yes, but my point of view is that the choice of axiomatics is significant when one wishes to refer to something as a synthetic theory of something. In the language of the following…

I would say that the “objects and properties” are an invariant of the class of models, i.e. an invariant of “Morita equivalence” of theories, rather than depending on the specific presentation of a theory. Hence, I would argue that a property of a theory like “being a form of synthetic topology” is also an invariant under Morita equivalence, hence not depending on the particular axiomatization.

…my point of view is that is the presentation is significant when one wishes to refer to something as a ‘synthetic theory’ of something.

One might, for instance, be trying to prove something in the setting of a category equipped with some structure. Now it might turn out that a category admits this structure if and only if it admits some other structure. But the proof of this equivalence will have some content, and it may be that one regards the one structure as better from a foundational point of view as the other. For instance, we might consider (not necessarily strict) monoidal categories. One can describe these as models for an ‘unbiased’ theory or a ‘biased’ theory (the usual one). The models are equivalent, but the proof of this is significantly non-trivial. I much prefer the theory of unbiased monoidal categories over the biased one, because the coherence theorem, which should be at the heart of any theory of monoidal categories, is straightforward and can be understood conceptually: a foundations in which one needs a deep result (MacLane’s coherence theorem for ‘biased’ monoidal categories) to establish something fundamental is not a good foundations, in my opinion. In particular, I don’t feel the matter of choosing between the theory of unbiased and biased monoidal categories is just ‘something to be discussed over lunch’: I feel that it is a choice that has significant mathematical consequences.

For another example, consider the difference between a material set theory and a structural one. One might be able to show that the models (with appropriate choices in the theory on either side) are equivalent (I don’t wish to enter into technicalities about how or whether this can be made precise, the example is just intended to try to illustrate what I am getting at), but I would regard there as being a great difference between them as ‘synthetic set theories’.

Regarding 4), my feeling remains: what I am looking for is a precise statement of how ‘ordinary mathematics plus choice sequences’ can be made sense of within synthetic topology. For example: some kind of monadic adjunction between ‘synthetic intuitionistic set theory’ and ‘synthetic topology’ that ‘freely throws in the possibility of using choice sequences’.

I feel the same way about your response to my point about the argument as a whole: it is not at all clear to me how Brouwerian mathematics ‘embeds’ in synthetic topology, or indeed whether this can precisely be made sense of at all. I wrote that I wouldn’t have thought that one can just ‘throw away’ the parts of synthetic topology except that needed for 2), and this is all the more the case since you are not thinking of ‘ordinary mathematics’ as that which is ‘discrete’. Again, I would be looking for a precise statement along the lines of the adjunction mentioned in the previous paragraph.

Regarding species, the point is that they appear to play the role of a notion of set or type in Brouwerian mathematics, and are prior to any notion of continuity. One might try to argue that these gadgets can be thought of as topological spaces, and thus live inside synthetic topology as primitive gadgets. But this doesn’t seem right to me: the species of real numbers is defined in Brouwer’s work, so it can’t be the species corresponding to the primitive $\mathbb{R}$ . Similarly, one can define continuity for the species of real numbers in Brouwer’s work, so it can’t be the primitive notion. And then it seems to me that the way in which you envision that synthetic topology captures the continuity principle breaks down. Thus one is left with the conclusion that it is not at all clear that species fit into synthetic topology, which is the point I have been making all along.

Posted by: Richard Williamson on March 5, 2015 8:47 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

my point of view is that is the presentation is significant when one wishes to refer to something as a ‘synthetic theory’ of something.

Okay. We will probably have to agree to disagree on this one.

For instance, I agree entirely that biased vs unbiased monoidal categories has real mathematical content, but that isn’t relevant for me. From my point of view, it could be that theory X turns out to be a theory of synthetic Y, but that this fact is a deep and surprising theorem that is not discovered until many years after theory X is first formulated.

Material vs structural set theory is a great example to illustrate exactly what I’m saying and what I’m not saying. It is true that there is a sort of equivalence between the collection of models of ZFC and the models of ETCS+R. However, this is not induced by an equivalence of walking models, because among other things the two theories have different signatures and so their walking models do not even live in the same world. Thus, it is not a Morita equivalence of theories, and so I can consistently say that the property of “being a synthetic theory of well-foundedness” (which I would apply to ZFC and not ETCS+R) does not transfer across it, even though such properties do transfer across Morita equivalences.

It seems clear from these examples that the underlying issue is that you just want to use the phrase “synthetic theory” differently than I do, and probably neither of us is going to convince the other.

what I am looking for is a precise statement of how ‘ordinary mathematics plus choice sequences’ can be made sense of within synthetic topology… it is not at all clear to me how Brouwerian mathematics ‘embeds’ in synthetic topology, or indeed whether this can precisely be made sense of at all.

I’d be willing to try to give you want you want, if you can point me to a precise definition of “choice sequences” or “Brouwerian mathematics” from which to start. My impression was that Brouwer was opposed to making his foundations precise, so that it’s not possible to prove any precise theorem in modern language about his mathematics. So I don’t know quite what you’re looking for.

the species of real numbers is defined in Brouwer’s work, so it can’t be the species corresponding to the primitive $\mathbb{R}$ .

Now I’m totally confused about what you think synthetic topology should be. I’ve agreed with you that synthetic topology ought to have an object playing the role of “the real line”, and I don’t see any reason why that object must be the internally defined object of real numbers, but I also certainly don’t see any reason why it must not be! Indeed, in what I wrote in the above draft post, I was assuming (for simplicity) that it always would be.

Similarly, the synthetic notion of “continuity” is basic, but there’s no reason that it couldn’t happen to coincide with an internally defined notion of continuity in certain cases. Indeed, that is the whole point of a synthetic axiom or theorem like “all functions $\mathbb{R}\to \mathbb{R}$ are continuous” — all such functions are of course synthetically-continuous (because all functions in synthetic topology are synthetically-continuous, essentially by definition), but a hallmark of many synthetic-topological theories is that at least for $\mathbb{R}$ , this notion of continuity happens to coincide with the internally defined $\epsilon$ - $\delta$ notion of continuity, and that therefore all functions $\mathbb{R}\to \mathbb{R}$ are also $\epsilon$ - $\delta$ -continuous.

So, yes, Brouwer’s “species” would correspond to (perhaps a subclass of) the basic objects of synthetic topology, which one might call “types” or “spaces” or (confusingly) “sets”.

Posted by: Mike Shulman on March 5, 2015 5:15 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

We will probably have to agree to disagree on this one.

It seems clear from these examples that the underlying issue is that you just want to use the phrase “synthetic theory” differently than I do, and probably neither of us is going to convince the other.

I agree!

I’d be willing to try to give you want you want, if you can point me to a precise definition of “choice sequences” or “Brouwerian mathematics” from which to start. My impression was that Brouwer was opposed to making his foundations precise, so that it’s not possible to prove any precise theorem in modern language about his mathematics.

In this case I was referring to ‘Brouwerian mathematics’ as you wish to regard it, namely the fact that ‘all maps from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ are continuous’. In other words: I was looking for some kind of adjunction between synthetic intuitionistic set theory and synthetic topology which expresses the fact passing from set theory to topology under this adjunction ‘freely’ ensures that all maps from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ are continuous. The ‘freeness’ is crucial: I am trying to find some way to precisely formulate your claim that within synthetic topology we have ‘ordinary intuitionistic mathematics and in addition choice sequences’. We should in particular be able to ‘ignore’ the fact that all maps from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ are continuous if we so wish.

I appreciate that it might be difficult to see what I am getting at, but that is somehow exactly my point of contention: how to make sense of the notion of ‘ordinary mathematics and in addition choice sequences’. I feel that the latter has meaning in Brouwer’s mathematics, but that it is a tricky (and interesting!) matter to formalise this meaning. It seems to me that whilst I can certainly agree that there is something to the analogy between synthetic topology and Brouwerian mathematics, it is another thing to claim that there is a precise sense in which we have ‘ordinary mathematics together with choice sequences’ in synthetic topology. Maybe it is the case, and I would then be very interested in the details.

But you may wish to leave the discussion here and not go into a possible formalisation of this aspect, and this would be perfectly fine for me. The discussion has raised an interest in me to at some point (who knows when, but at some point!) really try to think in depth about formalisations of Brouwerian mathematics!

I’ve agreed with you that synthetic topology ought to have an object playing the role of “the real line”, and I don’t see any reason why that object must be the internally defined object of real numbers, but I also certainly don’t see any reason why it must not be!

The ‘constructed’ species of reals will not intensionally be the same as the ‘foundational’ species of reals, for the trivial reason that the latter is not constructed at all. And if species are regarded as spaces, then intensional equality should, it seems to me, correspond to isomorphism. Maybe it obscures things slightly to use $\mathbb{R}$ , so I will try to put the point I was trying to make slightly differently here: for trivial reasons, the fact that ‘all maps from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ are continuous’ as expressed internally (the continuity principle as expressed in the language of species) is not the same intensionally as the synthetic version of this statement (i.e. the ‘meta’ one which is true just because of the way that we think of synthetic topology as a formal system). And thus the way in which you are thinking of synthetic topology as formalising Brouwerian mathematics (1) - 6) in my earlier comment) breaks down, it seems to me.

Beyond this, there are many other difficulties, I think, in regarding species as the spaces in synthetic topology. For instance, one can presumably make sense of a ‘morphism of species’. Why should such a notion correspond to the notion of a continuous map? Even if there is a way to do this, how is it compatible with the statement of the ‘continuity principle’? How does one make sense of a ‘species of species’? What is the correct notion of ‘extensional’ equality of species? And a question more to do with meaning: in Brouwer’s second act of intuitionism, there is emphasis on species being defined by ‘properties supposable for mathematical entities previously acquired’; how can this aspect be captured within synthetic topology?

Again, feel free not to enter into these questions. As I mentioned, the discussion has led to consider some aspects of Brouwerian mathematics and its formalisation that I had not contemplated before, and to become interested into looking into this further: I am entirely content with that state of affairs!

Posted by: Richard Williamson on March 5, 2015 8:09 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I don’t see how you get from wanting to see one theory sitting inside another to demanding that that inclusion be “free” in any sense. Why do you need anything like an adjunction to allow you to ignore something? Just ignore it!

All your questions about species also seem to me likely to have straightforward answers, but I’m also about out of energy and time for this thread, so as you suggest, let’s wrap it up. Thanks very much again; you’ve given me a new perspective on Brouwer’s mathematics and a lot to think about.

Posted by: Mike Shulman on March 5, 2015 9:36 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

As precursors to Fourman’s work, Kreisel and Troelstra provide an elimination translation from a theory with choice sequences to one without. This builds on the concept of neighborhood functions, an inductive presentation of the functions $N^N\to N$ . The proof that all such functions can be presented by neighborhood functions is classical. However, for Brouwer, to give such a function precisely means giving neighborhood functions. Fourman’s part I provides a topos theoretical analysis of this. At the same time, Moerdijk and van der Hoeven consider the topos of $M$ -Sets for the monoid $M$ of neighborhood functions. In this model, like in the work by Kreisel and Troelstra, Baire space ( $N^N$ ) is more fundamental than the reals.

We collected some references here before. It would be good to elaborate a bit on that.

Posted by: Bas Spitters on March 5, 2015 10:55 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Thank you for the interesting references, Bas!

Thank you for the interesting discussion, Mike! (In the interest of concluding it as we both wish, I’ll not respond directly to your last comment - maybe these things are something that will crop up again some time in the future)!

Posted by: Richard Williamson on March 6, 2015 11:53 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

The influence of Brouwer on PML is quite explicit in his thesis and continues at least through the development of formal topology.

Posted by: Bas Spitters on March 4, 2015 3:27 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

By ‘his thesis’, are you referring to Notes on constructive mathematics?

I should say that I would regard it as clear that there is a significant influence of Brouwer in a general sense on Martin-Löf’s type theory and his philosophical justification of it. I was referring specifically to what seems to me be an influence of Brouwer’s notion of a ‘species’ on Martin-Löf’s conception of the notion of a ‘type’. While I have not seen it, Notes on constructive mathematics looks, from what I can gather from the mathscinet review, very relevant in this regard, thanks!

Posted by: Richard Williamson on March 4, 2015 3:23 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I’m very looking forward to reading this chapter.

…and regard Euclid’s “definitions” (like “a point is that which has no part”) as fairly meaningless.

And yet that repository of wisdom, $n$ Lab has at point

As a topological space, the point is the usual point from geometry: that which has no part.

Then

The distinction between analytic and synthetic dates back at least to Hilbert.

Well that’s true, but then so is “The use of the wheel dates back at least to Henry Ford”.

We have Pappus in c.300 AD writing

Now analysis is the way from what is sought—as if it were admitted—through its concomitants [akolouthôn] in order to something admitted in synthesis. For in analysis we suppose that which is sought to be already done, and we inquire from what it results, and again what is the antecedent [proêgoumenon] of the latter, until we on our backward way light upon something already known and being first in order. And we call such a method analysis, as being a solution backwards [anapalin lysin].

In synthesis, on the other hand, we suppose that which was reached last in analysis to be already done, and arranging in their natural order as consequents [epomena] the former antecedents [proêgoumena] and linking them one with another, we in the end arrive at the construction of the thing sought. And this we call synthesis.

But perhaps you meant Hilbert was an early user of analysis and synthesis in something like the sense of the preceding paragraph, even if he used other terms, ‘genetic’ and ‘axiomatic’ (or at least their German equivalents).

Did you know our editor has worked on this aspect of Hilbert, here?

I wouldn’t mind betting the matter is extremely complicated, as it usually is when one looks closely. See a careful historian, José Ferreirós, write

In my book (1999), the links between Dedekind’s work and Hilbert’s early axiomatics were not appraised properly, one important reason being that I followed a traditional (but incorrect) way of understanding the contrast between “genetic” and “axiomatic” methods. By contrast, Sieg was the first to clearly grasp the intimate links between the methodologies of the two mathematicians; for more detailed remarks on the relations between my views and Sieg’s, and clarifications about the points on which my understanding has shifted, see pp. 458-463 of the new paperback edition of Labyrinth of Thought (Birkhäuser, 2007, Epilogue).

and

In Hilbert’s mind the “genetic” approach was associated with Weierstrass and not Dedekind. Indeed, an examination of Hilbert’s 1905 lectures on the logical principles of mathematical thought confirms this idea: in the discussion of the genetic method (Hilbert 1905a,9–10; see also 212) he mentions only Weierstrass and Kronecker, and he accuses this method of defining things “through processes of generation, not through properties” (durch Erzeugungsprozesse, nicht durch Eigenschaften) – a reproach that can only be levelled against the Berliners, not against Dedekind.

Posted by: David Corfield on March 2, 2015 9:37 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Thanks for checking my facts! And also for the link to Landry’s paper.

Personally, I don’t quite understand how the nLab gets from “that which has no part” to the terminal topological space. The most generous interpretation I can think of is that “has no part” is being interpreted to mean “has exactly two subobjects, itself and the empty space”. That might even be sort of like what Euclid had in mind — except that Euclid clearly was not trying to define the terminal topological space. (-:

Regarding analytic/synthetic, what I meant to suggest was that Hilbert was one of the most influential early emphasizers of the analytic/synthetic dichotomy in mathematics (even if he didn’t use those words for it). Am I wrong about that? Your quotation from Pappus seems to be more about the general nonmathematical meaning of the words. I do expect the matter is very complicated, which is why I used the weasel words “at least”, but I thought that Hilbert’s writings were some of the more influential.

Posted by: Mike Shulman on March 2, 2015 11:46 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Well just before that extract from Pappus he had written

The so-called Treasury of Analysis [analuomenos] .. is, in short, a special body of doctrines furnished for the use of those who, after going through the usual elements, wish to obtain the power of solving theoretical problems, which are set to them, and for this purpose only is it useful. It is the work of three men, Euclid the author of the Elements, Apollonius of Perga, and Aristaeus the Elder, and proceeds by the method of analysis and synthesis.

All three are mathematicians. I had to look up Aristaeus to check on that.

Then there’s Proclus in the 5th century writing

beauty and order are common to all branches of mathematics, as are the method of proceeding from things better known to things we seek to know and the reverse path from the latter to the former, the methods called analysis and synthesis.

I completely agree that the meaning of analysis and synthesis change. Were you telling the whole story, you’d have to talk about what synthetic meant to geometers. E.g Lacroix in 1816

The Elements of Euclid are treated by the synthetic method. This author, after having posed the axioms, and formed the requisites, established the propositions which he proves successively being supported by that which preceded, proceeding always from the simple to compound, which is the essential character of synthesis.

My point is that it seems to me not best practice to give the impression that there’s a timeless notion of analytic and synthetic in mathematics, and credit with promoting this notion a man who uses different terms, genetic/axiomatic.

Synthetic/Analytic were very much in the air, think of Klein and Lie. Why would Hilbert choose different names?

Posted by: David Corfield on March 3, 2015 8:10 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Okay, thanks a bunch! I’m glad someone who knows some history is keeping me honest. I’ll be sure to change that paragraph.

I am puzzled, though, as to

Why would Hilbert choose different names?

Did he actually mean something different by genetic/axiomatic?

Posted by: Mike Shulman on March 3, 2015 4:06 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I didn’t know about the term genetic, but I like it.

Because the meaning of analytic and synthetic changes so often, it makes perfect sense for Hilbert to introduce new names for those concepts. Now we can use genetic and axiomatic to refer to analytic and synthetic in the sense of Hilbert.

Judging from his disagreement with Brouwer, he would certainly had trouble accepting synthetic models where the axiom of excluded middle fails.

Posted by: Martin Pape on March 3, 2015 8:24 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

For better or for worse, “synthetic” is already in common use by various communities of people doing that kind of mathematics (synthetic topology, synthetic differential geometry, synthetic domain theory, and now with HoTT/UF synthetic homotopy theory). Moreover, “axiomatic” has sometimes been appropriated for mathematics that is “relatively synthetic” but still analyzed into set theory; e.g. people say “axiomatic homotopy theory” to refer to Quillen model categories.

Posted by: Mike Shulman on March 3, 2015 8:40 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Regarding “Euclid’s” definitions of points and lines, in his book The Forgotten Revolution, Lucio Russo writes:

“As already discussed, there is much to suggest that Euclid subscribed to the nominalist and constructivist blueprint, but this is apparently contradicted by the first few definitions in Book I of the Elements, of which we quote the first four:

A point is that which has no part.

A line is breadthless length.

The extremities of a line are points.

A straight line is a line that lies equally with respect to the points on itself.

Such definitions, and the next ones for a surface and a plane, are clearly Platonist-essentialist, and fit better with the cultural imperial age than with that of the early Hellenistic climate of the period: they find no parallel in the works of Archimedes and Apollonius.

The Elements have reached us with interpolations from late Antiquity, and it is not unreasonable to suspect that these definitions are instances thereof.”

This is followed by many pages advancing this thesis.

Posted by: S. on March 4, 2015 3:20 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I certainly don’t want this chapter to delve into the question of whether Euclid was Euclid!

Posted by: Mike Shulman on March 4, 2015 6:00 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

I am sure you don’t. You wrote:

“Although Euclid himself attempted to define “point” and “line”, modern mathematicians generally consider this a mistake, and regard Euclid’s “definitions” (like “a point is that which has no part”) as fairly meaningless.”

My point was that Lucio Russo would contend that Euclid probably did no such thing, and that Euclid himself, along with his contemporaries, would probably have considered such definitions “fairly meaningless”.

Therefore, if you lend any credence to Russo’s contention, it would be better to write: “Although Euclid’s Elements does contain definitions of…” or “Although Euclid’s Elements, as they have come down to us, does contain definitions of…” or something along those lines.

Posted by: S. on March 4, 2015 8:49 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

Okay, thanks; that’s a pretty easy change to make, which can easily be ignored by the reader who doesn’t know of any controversy about Euclid’s identity, and which is a perfectly correct statement on its own that doesn’t require me to learn enough about such a controversy to have an informed opinion (which I admit that I don’t want to do). (-:

Posted by: Mike Shulman on March 5, 2015 12:21 AM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

One can easily argue that any foundational formal theory (such as ZF) is an analytic approach to the primitive concepts it tries to capture. ZF tries to capture “synthetically” the relation of sets membership, and obviously builds all the other “objects” from such “synthetism” in an analytical way. Your example of synthetic topology as opposed to theories built “over ZF” in an analytic way is confusing for two reasons 1) you’re just having a new foundational theory whose primitive concepts is not the ones of sets and and memberships contrary to ZF, but the one of spaces… 2) All the mathematics you’re going to construct “over this theory of space”, will be analytically constructed with “pieces of spaces”. No difference.

I therefore think that this distinction between analytic and synthetic is irrelevant and is confusing more than it helps to understand one thing: how abstraction works.

Feel free to discuss this http://math.stackexchange.com/questions/1175166/stratification-typage-of-logic-and-syntax-at-the-same-time-is-such-a-dream-fe

Posted by: sure on March 4, 2015 6:14 PM | Permalink | Reply to this

$MathML-enabled post (click for more details).$

replace “analytic” by “synthetic” in the first sentence, obviously.

Posted by: sure on March 4, 2015 6:46 PM | Permalink | Reply to this

Re: Introduction to Synthetic Mathematics (part 1)

$MathML-enabled post (click for more details).$

any foundational formal theory is a [synthetic] approach to the primitive concepts it tries to capture

Of course it is! Almost by definition.

All the mathematics you’re going to construct “over this theory of space”, will be analytically constructed with “pieces of spaces”

No, not all the mathematics. If the base theory is synthetic topology, for instance, then while the group theory will be analytic, the topology will be synthetic, since it is built into the base theory. And the topological group theory will be partially synthetic and partially analytic. By contrast, if the base theory is ZFC, then the theory of well-founded relations will be synthetic, since the basic objects of ZFC are well-founded relations, while the theory of topology will be analytic. By contrast, if the base theory is synthetic topology, then the theory of well-founded relations has to be analytic.

Posted by: Mike Shulman on March 4, 2015 6:51 PM | Permalink | Reply to this

$MathML-enabled post (click for more details).$

I agree with that. Hence the need to build a general framework in which synthetic theories (what I call foundational formal theories) could all cohabit and talk to each other in a subtle talk!

My intuition tells me that not all synthetic theories are “as deep” as the others (when it comes to proving theorems, simplicity, expressive power, …), and that if we have such a framework (that is, a synthetic theory of synthetic theories), then it might be possible to make such a claim formal and provable…

Posted by: sure on March 4, 2015 7:01 PM | Permalink | Reply to this

Re:

$MathML-enabled post (click for more details).$

Hence the need to build a general framework in which synthetic theories could all cohabit and talk to each other

Part of the claim of part 2 was going to be that category theory is that general framework. With the new reorganization I don’t know where that will end up, but I’m pretty sure it’ll be in there somewhere, since this is supposed to be a book about category theory.

Posted by: Mike Shulman on March 4, 2015 7:03 PM | Permalink | Reply to this

Re:

$MathML-enabled post (click for more details).$

I think you’re right in some sense, one can see any category to be a “synthetic theory”, and functors between them as either models or what make these synthetic theories talk.

Yet, what would it mean to speak about an (analytic) theory over a category C seen as a synthetic theory? Would that be internalizations inside C?

What would still miss, is the possibility of category theory to speak about its own propositions and syntax, which is, in my opinion, a key point/motivation to such frameworks.

PS: I’d rather see category theory as a “model” of such synthetic theory of synthetic (and resulting analytic) theories.

Posted by: sure on March 4, 2015 7:09 PM | Permalink | Reply to this

Re:

$MathML-enabled post (click for more details).$

Yes, internalizations. I don’t understand what you’re worried about “its own propositions and syntax” though: any sufficiently rich synthetic theory can define syntax and logic, just like any other part of mathematics, and prove facts about models of other synthetic theories constructed from it.

If you want a synthetic theory of the “universe” of synthetic theories, then maybe what you want is 2-category theory. (-:

Posted by: Mike Shulman on March 4, 2015 7:14 PM | Permalink | Reply to this

$MathML-enabled post (click for more details).$

That’s what I want (feel free to read the stackexchange post I linked), and even more: I want to stratify analytic theories over a synthetic theory, and I want the analytic theory of “propositions in the synthetic theory” to make sense. That is, I want to make sense formally of the meta-mathematics of some synthetic theory as an analytic theory “over” it. Hence, I want both definitions and propositions to be stratified in order to avoid diagonal inconsistencies, and I want that to be recursively defined up to infinity (you’re always free to build another analytic theories over an analytic one. That is, you would have levels of analycity).

Posted by: sure on March 4, 2015 7:21 PM | Permalink | Reply to this

Re:

$MathML-enabled post (click for more details).$

Well, I hope you find what you want. (-: Personally, I would say that the meta-mathematics of any rich synthetic theory can be studied in that theory, by defining the objects of logic (formulas, propositions, etc.) in the obvious way. For instance, the meta-mathematics of ZFC, in the sense of studying its models, logical consequences, independence results, and so on, can be formalized in ZFC itself, and I think generally would be regarded to be so formalized (just like the rest of mathematics). If you want to be able to construct models of the theory inside itself, you can add a tower of universes to pretty much any synthetic theory.

Posted by: Mike Shulman on March 4, 2015 8:06 PM | Permalink | Reply to this

$MathML-enabled post (click for more details).$

Some precisions: if my foundational formal theory/synthetic theory $F$ is built up from a language $L$ , a logic $I$ and some axioms $A$ , then the internalization of $I$ inside $F$ , say $I_F$ is by no mean the same thing as the propositions of $F$ .

If $Prop(F)$ denotes the “collection” (in natural language) of propositions of $F$ , then it is by no mean trivial that Prop(analytic theory with logic $I_F$ , axioms $A$ + something and language $L$ with underlying synthetic theory $F$ ) is equivalent to $Prop(F)$ .

Example: a group object in Grp is necessarily abelian. Thus, one shouldn’t trust such internalizations. One needs a way to speak “naturally” of Prop(F) as an analytic theory over $F$ that comes from scratch with $F$ . (Then, one could also make sense of $PropProp(F)$ , and so on…)

Posted by: sure on March 4, 2015 7:32 PM | Permalink | Reply to this

Re:

$MathML-enabled post (click for more details).$

That sounds like you’re looking for some kind of reflection principle, like in the paper of Fourman’s that Bas mentioned. Which is interesting, but seems to be a very strong condition on a particular theory.

Posted by: Mike Shulman on March 5, 2015 5:31 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

February 26, 2015