aboutlogic: premises #03 | Synthetic vs. Analytic Math: Inspired by Emily Riehl

00:00:00: A short technical break, and now let's see whether we continue with slightly less barking.

00:00:07: Not supposed to bark!

00:00:08: It's

00:00:09: about

00:00:10: cats not dogs no?

00:00:11: Okay yeah.

00:00:15: Yeah category sir... Now I got it.

00:00:17: Slightly slow with the

00:00:18: fun.

00:00:24: Ah hello everybody this is a latest installment of AboutLogic our premises where we don't have a guest, and just Dennis and myself.

00:00:37: Ah yes!

00:00:37: And I should mention that you're becoming more professional in the way... ...that it can become member about logic.

00:00:48: We will soon add some sort of material to be accessible especially for members.

00:00:57: Okay Dennis what's on your on your mind.

00:01:04: Yeah, after last week's episode from Emily Real I wanted to ask about something that comes up quite often when you interview people and that is the idea of synthetic mathematics related to the analytic-synthetic distinction we have in philosophy.

00:01:22: what is a synthetic math?

00:01:26: Could

00:01:32: I'm not sure whether it's the same as a philosophical distinction, maybe you can comment on this later.

00:01:41: The prime example of analytic mathematics is Euclid geometry where Euclidean defined geometry or gave axioms for geometry last talking about lines and points, and then gives principles how to reason about them.

00:02:09: And this can be viewed in contrast with what we would call maybe analytic geometry where you actually think about coordinates.

00:02:22: The observation is that in a way the reasoning with axioms, with these abstract concepts.

00:02:40: it's much more elegant and so easier than doing this calculations on points and equations.

00:02:55: Euclid is the sort of first analytic mathematician.

00:03:02: And maybe we can summarize his... Sorry,

00:03:06: euclids would be synthetic right?

00:03:08: Synthetic?

00:03:08: sorry I just used the wrong word.

00:03:11: Yeah, synthetic mathematics by thus throwing away the coordinates instead.

00:03:15: always think about coordinates.

00:03:16: if you think about geometry in a more abstract way and this is also essence of synthetic mathematics

00:03:24: I mean, i think this is related to the philosophical side because it's not made up of the more basic but its really taking things as a whole.

00:03:36: The point that im always making when Im talking about the history of math That alot people say its only cumulative so we get know more and more.

00:03:47: But wait a minute.

00:03:48: sometimes we lose stuff like Euclid saying the line is more than the points on it.

00:03:54: And nowadays, the satirist says no-no, the line has exactly their point's on it and so somehow some meaning changed something was lost in transition and translation... Something related to that.

00:04:09: Yeah!

00:04:10: How does this look in practice?

00:04:12: I mean how can i see whether theory is synthetic or analytic whereas a synthetic theory particularly useful?

00:04:22: Yeah, I mean...I don't really have a sort of abstract definition.

00:04:28: But maybe it's interesting to look at some category theories or categories say okay the first step by Euclid is throw away coordinates because you can do geometric constructions without thinking about concrete coordinates but in more abstract synthetic way.

00:04:49: Now, let's look at that category theory.

00:04:52: The category theory is... I would say it's a synthetic theory of mathematics in any way or mathematical structures and instead think about the concrete analytic rates.

00:05:09: like we have groups where you've got some algebraic structure and functions between them We step back and say, okay we have these objects.

00:05:25: And then there are morphisms functions between them as they behave in a certain abstract way.

00:05:31: so you're saying OK we can...we always identity morphism and compose morphism.

00:05:39: Morphisms at the composition of morphisms satisfies associativity.

00:05:44: So this is a more sort of synthetic view of mathematics.

00:05:49: Instead of spelling everything out, we look at the big picture in a way and if you think about like sets and functions so they're an example for category.

00:06:01: So sets and function are very concrete.

00:06:05: We define what as a function?

00:06:06: And so on whereas categorical view it's much higher level.

00:06:13: We have objects and we have morphisms between objects.

00:06:17: And then using this sort of synthetic view, you can describe sets as by adding more constructions on set like for example products so the Cartesian product or a set the co-products, this joint union and so on.

00:06:43: And then we go up have exponential like functions and limits and co-limits... This leads to a theory of a topos as sort of an abstract way talking about sets.

00:06:59: but it's a synthetic theory of sets where you're not giving us concrete definition or any concrete definition, but do it in a synthetic way.

00:07:12: Which is... I mean also geometry.

00:07:16: already by playing around with the axioms you can capture different kinds of geometries like non-euclidean geometries and yeah so same we can do in categories here where sets by giving up some of these axiomes For sets, we get different structures which are more or less set-like.

00:07:40: So there's a rule of continuum and variation that arises from this synthetic view right?

00:07:49: If you do it analytically... You can't really see the big picture.

00:07:52: but once you describe things as synthetic for an abstract point much more possibility for variation giving up some properties and or adding so, arriving at different constructions.

00:08:13: Different universes.

00:08:16: in a way I am.

00:08:19: I mean i'm still slightly unsure whether got the grasp.

00:08:22: is my rephrasing correctly that you would say analytic will be pitting down One basic notion and building up stuff from that.

00:08:35: So I start with a notion of set, And i define functions as pair of sets With such-and-such properties and so on... And synthetic would be Okay?

00:08:51: I don't really know whether I got function but at least something function like by saying at least this must be given.

00:08:59: You

00:08:59: talk about functions without giving a sort of analytic explanation what the function is, you just say I know whatever functions and here's how they behave.

00:09:10: like Euclid says there are lines that no whole line behaves on not defining it in terms of its constituencies or points.

00:09:19: but

00:09:24: You have like this.

00:09:25: This should hold, this should hold... Otherwise it's

00:09:29: not a function?

00:09:30: Okay you could say but maybe it's rather that you have an intuitive idea of what do mean and you can break it down by saying okay I'm so concretely defining geometry for example by sets of points or coordinate if And constructions on sets, you say okay a function is the relation which has certain property.

00:09:57: and now we have products of sets.

00:10:00: We define that product set as a set of cares and so on here.

00:10:05: So one of them is analytics The other one it's just saying let us know what do mean?

00:10:17: For example, functions.

00:10:18: We know we can compose function and the function composition should behave in a certain way And so on.

00:10:25: So this is a synthetic way.

00:10:28: When you look at Euclid, Euclide sort of said let's forget about coordinates Let's do geometry, let's forgot about coordinates.

00:10:37: Category series says Okay!

00:10:39: We can do constructions or define structures like sets but also other structures But forget about the elements.

00:10:45: The elements are not so important, but how the structure we define is related to each other.

00:10:56: So it's in a way... throwing away concrete constructions and throwing away elements without talking about structures or going down into the element.

00:11:15: Yeah, I think essential or one of the central ideas of category theory.

00:11:22: Maybe in some sense this helps me to understand... Or to loosen a knot that i always had on whatever I programmed or saw somebody programming where people just write things down and it was like but where do we know whether something exists?

00:11:36: Like how is this instantiation did with the syntactic way off?

00:11:44: the synthetic way of thinking would be, okay let's work with this and I mean in theory.

00:11:50: This could be empty nothing could fulfill this

00:11:53: or

00:11:53: something.

00:11:54: yes so i'm not saying replace analytic mathematics by synthetic.

00:12:02: uh...I think that two can play quite well together.

00:12:05: but in the end yeah if you do a synthetic construction You should justify it by an analysis, but giving a concrete definition right?

00:12:17: So in the way we can understand as axioms of geometry.

00:12:23: By saying okay yeah We could understand these points as coordinates and you can understand lines And so on I think it's not giving up this analytic view But using this synthetic to have a better way of reasoning, more elegant ways.

00:12:48: A

00:12:49: short technical break and now let's see whether we continue with slightly less barking... I'm not

00:12:58: supposed to bark!

00:12:59: It's about cats but dogs no?

00:13:02: Okay yeah.

00:13:06: Yeah category sir know i got it slightly slower than one.

00:13:11: Okay, and you said that this viewpoint if you really push it brings us to Topos's.

00:13:18: And I find Topos is a quite interesting notion.

00:13:22: It also came up for instance in our Hamkins interview as like very general with Andre Like a very general notion of model maybe?

00:13:33: Also that this view point makes like salient to talk about the inner language of these toposes, right?

00:13:43: I mean okay.

00:13:44: First of all there is a... As far as topo is concerned i mean that lots different views.. There's this idea of a Grotendieg Topos which actually comes from algebraic topology.

00:13:57: and then this observation in such structure you can do lots of... This is actually an way it's analytic that we can.

00:14:05: in this construction, we do lots of constructions and sets theory.

00:14:13: It seemed to be an abstraction or it was observed.

00:14:18: these geometric or topological constructions lead to something which behaves like set theory.

00:14:25: And then the idea of elementary topos was introduced Instead of looking at the sort of concrete construction, or for golden digtoppers and for corpus of sheaves.

00:14:44: People just write down what you can do in such a universe, that's your category.

00:14:54: And that is then the definition of an elementary torcus.

00:14:57: I do have some issues with a standard definition for elemental torcus, but I think there are issues with lots things.

00:15:02: But yeah... The idea which was fine to say let's write down what properties of the category of sets and see if we know where.

00:15:18: different ways to think about sets.

00:15:21: Maybe you come from type theory, maybe here comes from classical set theory.

00:15:25: Maybe something else like some constructive sets theory.

00:15:28: but anyway so I think idea of a set as collection.

00:15:32: But how can we cast this categorical?

00:15:36: Okay So we have sets and we have morphisms between them.

00:15:39: these are functions.

00:15:40: This gives us the basic categorical structure.

00:15:43: But then there is obviously much more.

00:15:46: As we already mentioned products And dual co-products is something you can do with sets and exponentials or functions.

00:15:55: I mean, sets of functions are another important construction and so on.

00:16:02: So you build up more and more... You add more features to what you know about sets.

00:16:10: for example that could lead through the notion.

00:16:15: Okay, actually I think you have a Cartesian closed category with sub-object classifier where the subject classifier is basically an internal version of power set.

00:16:34: So it's categorical counterpart for having power sets.

00:16:40: and this may be also the point that maybe its too far in one plasticular perception of sets, which is classical.

00:16:54: And because it introduces the idea for power set and actually you can do lots of mathematics on sets without having powersets.

00:17:02: so that's maybe a point where I would say okay this has already too much assumptions in the category of sets of this idea for elementary topos.

00:17:22: So that's okay, there is some variability.

00:17:26: so what exactly should be a topos?

00:17:30: or do we want to have sub-objects?

00:17:36: Or maybe not but it's a detailed question onto like higher categories.

00:17:48: What about this?

00:17:48: If you

00:17:50: give me maybe one tiny question, as a classical not just classically trained logician may be I normally distinguish between the logic and the axioms.

00:18:01: so i willing to say something You can take ZFC And put in whatever logic you'd like into a synistic logic with it.

00:18:11: Maybe sometimes things break down don't really make sense.

00:18:14: So of course you need to find new things, but per se I'm thinking separately about these things.

00:18:20: You cannot or should not do that in Topos theory right?

00:18:24: It's really that they

00:18:27: aren't... Yes so yeah i think your axioms force um what we assume are both sets sort of determine what logic your head is.

00:18:40: okay the separation doesn't actually work very well Because for example, you can prove it to the middle.

00:18:55: So there's clear that all of a sudden the logic becomes classical even if we didn't start like this.

00:19:02: so they are versions... This

00:19:04: holds everywhere so-to speak right?

00:19:07: You started with the Intuitionistic Logic and then suddenly you got this Classical Logic.

00:19:14: It just comes up.

00:19:17: I mean, there are versions of the axioms which are compatible with intuitionistic logic.

00:19:27: so actually they're at least two that is iZF, intuitionistic ZF and CZF Which is constructive ZF And don't ask me exactly what's differences are?

00:19:39: I think one them has a sub-object classifier And what hasn't?

00:19:44: Which is which, okay.

00:19:47: But this again you can play so extra of choice.

00:19:51: for example introduce lots of logic but sub-object classifier as well.

00:19:57: the subject classifier basically says You have a type or an object which represents propositions which classifies the injections.

00:20:08: I mean injective functions because the injector functions really correspond to subsets in the process.

00:20:16: And this is a bit problematic from a predictive point of view, but it's a question whether let's say that type of propositions itself.

00:20:38: In classical mathematics you would say, yeah sure it's just two and fours.

00:20:41: Yeah

00:20:42: that is

00:20:44: a very small set.

00:20:45: Two elements but in international mathematics its not clear.

00:20:51: It´s the question you can answer either way.

00:20:54: You could say yes or no really And if you said No really then you do a predictive theory.

00:21:07: I mean, it's a bit like comparison if you're in predictionistic logic as being a vegetarian and the predicate version is vegan.

00:21:22: so we can go further.

00:21:24: but that's the comparison.

00:21:30: Maybe we should go to higher categories just on.

00:21:33: This leads to this very weird sounding thing.

00:21:37: that is the set of all subsets, two element sets.

00:21:42: Zero one can be larger quite large right into the synestically

00:21:47: which

00:21:48: often a moment where communication breaks down because I mean naively it sounds weird.

00:21:56: but if you see and these details matter.

00:22:03: Yeah, I mean there are lots of propositions right?

00:22:07: Yeah yeah

00:22:08: exactly if you say one if this and that and you distinguish these things it's not only zero-and-one like Frege would have loved then this is a complicated structure

00:22:21: but... I mean the loads of programs which compute things or compute these subsets.

00:22:39: And it seems to be a bit brutal too, all equator and what?

00:22:46: Yeah I mean this is something...I was always fighting with classical math because if i say for even this theorem followed from that one.. ...i'm not saying one ends one or something like that.

00:23:00: Or really me want have a finer graded structure, but maybe let's jump to higher categories because we have like ten minutes left for these shorter premises.

00:23:13: And how is this mess starting?

00:23:15: What making your category or higher-category?

00:23:18: what does the infinite category?

00:23:20: so many notions...

00:23:21: Yeah!

00:23:21: So categorical theory it's little bit like a drug addiction.

00:23:27: once you start and realize that sort of categories itself are or maybe not really sufficient.

00:23:35: I mean, okay this comes up when you start thinking about the category of categories which... Okay and some people think it's a category other people thing that is not two-category so on.

00:23:49: So what's happening?

00:23:53: You have let say objects in a category points then there are more phases between them like functions for example.

00:24:04: But then you can draw diagrams, I mean in category theory people always draw diagrams.

00:24:13: so like if you want to say that the two function compositions agree It has the same result.

00:24:26: So it's a way to write down equations, and in category.

00:24:30: there is reason with these diagrams by gluing them together right?

00:24:34: By having one diagram once another... And you glue it together!

00:24:39: You see that a diagram commutes if all of the paths through this diagram gives the same results.

00:24:44: This is pasting of diagrams.

00:24:47: That actually happens at next level because previously we were gluing or pasting functions and now you're pasting together these diagrams.

00:24:59: And there's a nice geometric view of this, which is like you have points or lines but now you've got some two-dimensional spaces, some surfaces right?

00:25:15: Like a square or maybe a triangle.

00:25:18: Yeah, and you can glue these spaces together.

00:25:23: And by gluing them together they have to fit the lines.

00:25:26: where you glue them has to fit like same way.

00:25:29: if your glue lines together then the points had to fit.

00:25:32: so now we do the same one level up.

00:25:34: You glue diaderms together yeah?

00:25:38: That is beginning of higher category theory because how actually my diadorm are.

00:25:47: but like bow the objects one level up and we compose, you can compose them.

00:25:53: And actually composition again has some properties which correspond to associativity

00:26:00: etc.,

00:26:00: You can go higher and high then say okay if I now compose these diatoms what do i get?

00:26:08: A three dimensional structure maybe a cube or tetrahedron.

00:26:12: so tetrahedral says that If you compose three triangles, you get one triangle on the bottom.

00:26:19: So it's a law of gluing together diamonds.

00:26:26: and what do in higher categories?

00:26:29: And they arise quite naturally also when we do some concrete analytic constructions is that if... That you do this all dimensions here don't stop You go at infinity And you can define this using the language of categories here.

00:26:51: This is used to these Khan vibrations and so on, as this has also done very synthetically in the work about model categories.

00:27:07: that's not my specialty but yeah... higher categories, when you try to write down exactly what they are it actually becomes quite subtle and complicated.

00:27:28: but there is a nice way out.

00:27:32: And I would say this type theory so types theory And then the functions between types, is a function type are the morphisms.

00:27:47: Then equality of these functions on the diagrams and then you have equalities or equalities... I mean okay it's particular kind for higher category It what we call infinity one category where all the higher morphisms which represent as equalities, they are symmetric.

00:28:13: They're invertible right?

00:28:15: So their group is... so it's not the full or most general version of a higher category but it's quite useful and that's got good.

00:28:25: first step to have this infinity one categories.

00:28:30: And here again the synthetic theory of Infinity One Categories is type theory.

00:28:39: So we throw away all this sort of concrete geometry, these very high-dimensional definitions.

00:28:50: And if you just work with types and equality types... ...and have a synthetic view on these inferior categories?

00:29:03: Maybe two questions at the beginning when were still talking about first diagrams.

00:29:10: I mean, this proof technique is notorious as these diagram chasing where people joke about category theories just drawing errors and then saying the diagram commutes.

00:29:23: The poof has finished.

00:29:24: so... And i could scan my way into the category conference to say it commutes but the crowd will agree because they fell off of details.

00:29:35: We encountered that as mere mortal mathematicians in our linear algebra.

00:29:40: But when we talk about the universal properties of groups, that it doesn't matter whether you go to the quotient structure first or not.

00:29:49: Or however these concrete properties look like but it simply doesnt' matter which path of errors follow right just for audience who have some embeddings?

00:30:08: which is using string diagrams.

00:30:11: And

00:30:15: then this building up of these diagrams, if you really make the geometry part heavy—which is probably not what you wanted to do—then as a combinatorialist I would think about doing it with simplices... If we go for triangles or cubes and do cubical stuff.

00:30:39: Right, the simplisher sets... I mean there's actually some interesting tension.

00:30:43: so in mathematics what is usually used are triangles, simplisher set.

00:30:50: And yeah it turns out that this a bit of mismatch to tag theory where its nicer to use cubicle sets.

00:30:58: So anyway The tension between triangles and cubes Is quite present.

00:31:06: That's two alternatives, which is as many.

00:31:09: And then you mentioned that there are still different ways of looking at these higher categories?

00:31:16: Is there any other viewpoint you would like to make specific that might help the audience think about this?

00:31:23: highly abstract things?

00:31:25: Yeah I mean...I think most direct approach to higher categories by actually constructing categories.

00:31:36: So you have a structure whose objects are against the categories, and then what are more reasons between categories?

00:31:47: More reasons between category is simple for the functors.

00:31:54: They're maps between the object which preserve composition identity... ...and those classical view of categories say this as a category.

00:32:07: I would from a point of type theory disagree because the complexity, category of categories.

00:32:21: The equality of functors is much more complicated than the equality or functions right?

00:32:28: So if you have two function they are equal in most one way Whereas if you have functors, there can be equal in lots of ways.

00:32:39: You need an isomorphism between these functor and natural isomorphisms but this has much more possibility many more choices And so on.

00:32:50: But what do we construct?

00:32:53: What are the two categories?

00:33:04: starting to do, I mean doing an algebra.

00:33:07: Like if you know what a category is it's not too difficult to define the two categories and then you can go on and try to find out of three categories but that becomes... You really get bogged down in very nasty combinatorial details In particular If your want to define this as weak notion of a higher category, which I think is the right one.

00:33:33: And also it's a white one for most of topological product of you.

00:33:36: and so Yeah So yeah You can start constructing these higher categories.

00:33:49: It becomes incredibly complicated and then actually this geometric view Is already big improvement because It makes it possible at least to define higher categories, but still is quite hard to do concrete constructions on them.

00:34:07: And then having this even more self-synthetic view of high categories via type theory enables or simplifies things much further.

00:34:24: So I mean what i was saying There are, the idea of higher categories arises quite much.

00:34:33: Okay let me say something.

00:34:36: there is this when you do algebra I mean it start to do maybe if we have some structures and then you define your saying you defined algebraic structure so they're saying that's a ring or as group and so on?

00:34:51: And can you things already more synthetic reason about this in abstract.

00:34:57: but But then you talk about between, I mean working with a group to have group morphisms.

00:35:09: and then if we analyze the category of group morphism which has particular structure.

00:35:16: Which is actually quite different from the category sets.

00:35:20: but now you have categories for structure So they are a bit more complicated than just algebras.

00:35:28: There's the algebra of categories, for example there Cartesian closed categories or their top way and so on.

00:35:37: And then you have morphism between top-way.

00:35:41: It is quite natural emerges somehow that You need to climb up these towers.

00:35:52: I

00:35:54: mean, that's why this used to be called universal algebra a few years ago or decades maybe even at that point.

00:36:02: But really coming from this

00:36:03: algebra... It is the first level right?

00:36:06: So you know there was an algebra.

00:36:07: You say okay we have an algebraic structure where they have associative operation and so on.

00:36:16: but now look at algebraic structures.

00:36:19: You have a particular algebraic structure, for example the category of groups.

00:36:25: And you look at how two groups relate to each other?

00:36:29: I mean what are the morphisms between groups and what does it?

00:36:33: constructions in groups there's an initial object which is also terminal... ...and so on.. ..and if you analyze this from sort of higher point-of-view you climb up your layers of abstractions all of a sudden the algebraic structures or your objects, and you think about what kind of categories arise from certain algebraic structure.

00:37:04: So there is this tension here...

00:37:08: Okay I guess that's enough for one episode of premises.

00:37:13: it's a lot to grasp on me because i'm completely unknowledgeable in categories.

00:37:21: But it helps me to illuminate some of the comments made by our guests and see how useful this would

00:37:29: stay.

00:37:29: I mean, obviously we have been lying at some points but let's say

00:37:33: for educational purposes... That is always fine!

00:37:39: We are rather honest with details than messinesses or foundations.

00:37:49: You need to simplify things.

00:37:52: Okay, great!

00:37:53: So thanks y'all for tuning in.

00:37:56: you can now become a channel member and as always you can comment subscribe buy us coffee.

00:38:01: that's always helpful And we look forward to see you then bye-bye.