Wolfram Physics Project: Working Session Tuesday, Aug. 4, 2020 [Empirical Physical Metamathematics]

I talk about uh, where I talk about the correspondence between um oh boy, so this is oh, this is about quantifiers and if I don't think this is relevant, we should not get too involved in this, but I think we need to understand this to understand that way degenerating this multi-way thing, let me ask you, let me ask the obvious question, Stephen would be, um, if we think about a multi-way system where the rules are literally mathematical rules, mathematical rewrite rules, yeah, rule delays and the initial condition is an expression. extremely well defined what is that that will be a multi-track system in general, haven't we studied them properly? graphical form that the tester is effectively doing, I mean, in a sense, the tester is doing a single test, I mean, this is, you know, I think the fancy version of Curry Howard's correspondents or whatever else you know um, this whole thing about program testing type of thing that actually says that the tester takes a single pass through this graph, yeah right, and the question of what do I mean arbitrary, so you know, simplify it to say just an operator, let's say a binary operator, no, that has not been done properly. studied and that's, um, I just started studying these things as essentially multi-way generalizations like what I called symbolic systems that are kind of analogous to combinators, right, because yeah, because combinators are a special case of those that they simply have. be on tour or some of them are on tour complete instances of mathematical rewriting exactly, but you can study the general case, you can study the ones that are not complete, but you know, I think the big story of the multi-weight graph is still the same and a lot of what I was going to talk about today is really just a story.

Well, it starts with the history of multi-weight graphs, then multi-way graphs have to be interpreted for mathematics or for

physics

and that's where these kinds of problems are going to arise, but I'm still a little frustrated because I can't find my um, my whole discussion, uh, you know, it really bothers me how many things I actually do. I understood 25 years ago that I had completely forgotten about it and this is one that Jonathan rhee uh re-discussed recently and I had completely forgotten about it, but what I'm looking for is the discussion of how this relates to things like calligraphy um and uh . um oh let me do a search here uh oh here we go here's the discussion okay it's always good to take a look at these semi groups okay so what we have in a multi way system is a semi semi group right, so in a semi group one has something, uh, you know, what we're saying is that um um, okay, they're called magmas or monoids or something like that, which, um, when you relax the inverse requirement, no, I think this is called semi-tui systems I don't think they have a name in the traditional I don't think I mean monoids they just have an element of identity um I don't think they have any other name other than semi-tui system or system of production So, okay, so let's look at uh, I mean, here I'm talking about well, given a particular representation of a group in terms of rules for a multi-way system, it was often loose Kelly graph, okay, so I think that the calligrapher is a kind of complementary thing. to what we're getting in this representation here because what it says is that you're identifying everything, I mean you know I had a version of this that was another piece of code that I wrote where you're just applying the group relationships that you're not applying this extra weird thing that is generating elements, right, you're only applying group relations, which means that given a particular, then we could do that, we could write something that only applies group relations, so for example we could say um a a goes to nothing um well yeah to a goes to nothing a to goes to nothing um I think I had a resource function that actually did this um those those two relationships so we want to say um uh what else do we want um uh we want nothing to go to to to nothing goes to to to and that should be the free semigroup on an element those are the relations for the free semigroup on an element, so if we say multiway graph of that, what we should get, I mean, it's not very exciting, but what we should get it's um if now we say, for example, a resource function string tuples um and then let's say we say aaa, I don't know three, for example, um, let's say a graph of three comma states, oh God, a graph of two states comma, okay, so these are the separate elements, right, these are the things that in the calligrapher become a single element, right, a single node in the calligrapher makes sense, okay, you understand what's going on here, yeah, I mean, this is here, let's take a simpler case. take this case here, so these are each element, where, right, these are all the things that are related simply by the relations in the group, these are all the words in the group related by the relations in the group, I mean , and unless I have something wrong here, oh, I see, oh, this was a little crazy of me, so this particular walk through the group is going to be particularly extreme because I'm allowing the identity to go to a, for example , and that is. making me go, you know that's what generates a lot of identities here makes sense, yeah, if you just wanted to add because I mean, the typical thing about the generator is that you can pre-apply or post the generators right. you don't put them in the middle of the word um, which maybe you can do with the end of the rope arrow and the beginning of the rope arrow.

I mean, those are chord patterns. Yes, they are string patterns. I mean, you're just suggesting that we. It should be fine, we should avoid inserting identity elements in the middle of the string because I guess the fundamental point would be that there are some vertices of the graph it produces that are actually identical to other vertices under the group accents, but it hasn't . I gave them enough time to figure it out, sure, but the point is that each of these consists of words that are equivalent in the group. Each connected component is words that are equivalent depending on the group.

Well, yes, these. they're all the same group element actually what is the identity this is that one is all the same group elements it's all identity and I'm just trying to explain the relationship between this and a calligraphy, the Cayley graph is because that's going to Be important for what we'll talk about in a minute, I mean, the Cayley graph is kind of complementary to this, the view that we're taking for this multi-way graph, it's given an element that we can think about. of the multiple wave system as the reductions of that element, and we can also try to have something where we are also injecting things into the system by adding, I mean, this is the most natural thing to do, you just give it a given initial. string, we're just generating words that are equivalent to that initial string according to the rules of some particular group, for example, it makes sense, yeah, okay, so let's go back to the big picture of what we're trying to do, so the The big picture is that we have You know, we have these kinds of proof structures right, so let's talk about some facts about mathematics.

A fact about mathematics is that there is not necessarily an upper limit on the length of the path you need to get from one string to another. another one that is basically a statement of the undecidability of the word problem in the case of a group that is a statement of the existence of undecidable propositions in you know, that's the existence of undecidability in a system of random mathematical axioms, so that is the story now the question is, you know, what I'm trying to understand is whether one of the mysteries of mathematics is that the typical questions you ask don't involve these arbitrarily long proofs, that is, that mathematics is somewhat doable, so To give an analogy in

physics

, it could be the case that everything you care about requires going down to the most microscopic level and looking at every update you want to see every time you know, that's the story of computational irreducibility that could be the case everything in you knows that to know what happens after one second in the history of the universe you have to make ten to a thousand updates because you have to follow each individual update to know what is going to happen, that's the type of history of computational irreducibility, but in fact the big surprise of the physics

project

is that it is not necessary to go down to that level of detail because floating above that level of detail are things like general relativity and quantum mechanics, which are generic.

Do the facts that emerge from looking at the generic characteristics of this system, regardless of all its microscopic details, make sense? So the challenge of the day is what is the analogue for mathematics or

metamathematics

of the general statements of general relativity and quantum mechanics. do about the

physical

version of these multiway graphs, if there are any, I mean, it would be really cool if there were some, but hey, I think there are, that's why I'm making this discussion, right? I think there may be something because I think the raw material is the same as the raw material of physics, so in a sense, let's make another analogy so that another point is in the

physical

world where we can imagine that it is all the history of the universe. just a giant multi-way graph correct the universe as it was in the past the universe as it is now the universe says it will be in the infinite future just generates this whole multi-wave graph but in our experience of the universe we only get to sample pieces of this multi-way graph, yes, similarly in mathematics, we can say that ultimate platonic mathematics is just this giant multi-way graph, right, but in the human mathematics that we have done, we have only sampled a part of that weight graph multiple makes sense, then the question is like in physics, we can say, you know, we just sample the things around us, you know the Earth or something, but there can still be laws that apply to everything we can say.

The same goes for mathematics, that is, we have sampled a few million theorems of mathematics, but perhaps there are general principles about how or general principles about what happens that apply to all mathematics, not just the part we have sampled , so the question is what could there be um uh well I'm struggling to do that. I'm starting to understand something which is the fact that we can test general abstract things that you know like you know you test things about graphs or groups correctly, um and it's not like that. No matter what the group is, how does that fit into this picture of little bubbles of computational reducibility in what would otherwise be the hopeless tangle of physics, of microscopic closures, so I think the answer is that one group in particular and this is where I wanted to do a bunch of specific examples, a particular group is a model of the general axioms of group theory, so this particular thing here, well, this is this particular image, it's the general axioms from the theory of abelian semigroups, this is this one. tells you about things that are true, this set of connections, like the theorems we can prove here, are general theorems true about all abelian semigroups.

Okay, so if we have a particular abelian semigroup, we have two ways of describing a particular abelian semigroup. group we can say that we are going to add a bunch more relations to complete the relations of the obelian semigroup or we can say that we actually have a multiplication table for the ability and the semigroup and I guess these are equivalent things, but we can imagine and here it is where you know we can imagine essentially spinning, we can imagine defining a model that corresponds to that particular abelian semigroup and the claim from previous discussions we had is that we can think of a model as being like doing foliations in this image is fine, because a model It basically says that we are in a model, one of these strings could have a value, a coordinate position that is equal to another one of these strings, because the actual multiplication table is something in particular, right?

What we're saying is that in a model we're doing foliations here and in the model to know if some two things are the same, we're just going to have to ask well and this is where I need to adjust this a little bit, but you know, basically we're asking, in this case we are asking in the underlying rules of the system what follows from what is right and in other words, does this this does this down here follow from this up? Here then we will say, for example, that they have the same right, but another way of knowing that this follows from this is to say that we have some kind of foliation of this thing in which this is at a later time.

The next thing from this, in other words, this set of relations here defines some kind of partial order that we can try to do, um, we can, for example, do foliations, that's fine,understanding

metamathematics

en masse, if that makes sense, because normally in mathematics you're understanding, you know, each theorem is a unique thing, so to speak, the goal of the goal. Mathematics or this kind of continuous metamathematics is to understand mathematics en masse just as we understand spacetime en masse, that is, we could take the view that you know that this particular place in space has a name, it's called bob or something like that and that's what we want to focus on, but we don't do that, we think about mass space, right, um, well, maybe part of the dictionary is already clear to you, so, for example, paper of geodesics, like what are your shortest tests, okay, um in this image what is the appropriate time along a geodesic is to measure step by step how long it takes you to do the test, is it more or less correct and the The idea is that you can do a frame change based on the claim and that's the same thing with models is that there are two alternative ways to determine if something is right, so this is an interesting statement that there are two ways to find out if something is right. true in mathematics, so to speak, one is to symbolically follow the proof and the other is to say I know what that is in terms of a model and conclude something just from the model from a fact about the model, okay, so the concept would be and let's return again to the question of groups.

You know, a model of the abstract concept of a group is a particular group. Right, which could be finite, could not be finite, whatever it is, any group obtained by adding relations to the free group will be, in some sense, a model that you can think of as a kind of model of the free group, a model model. of groups in general um, uh, yeah, we have several people on our live stream pointing out all sorts of things, like a group can have multiple calligraphies depending on the generators you select, yeah, totally sure, um, but if I can , if I can.

I can rephrase what you just said because I think I understand it and maybe if I say it in a slightly different way you will agree and then I will know that we have the same idea, it would be that there are some truths that are self-evident. of that will be true for any group and it will also be true for a particular group and you could prove it by doing calculations on that particular group or just saying oh, but that's a group axiom, I mean, that's a, you know. general theorem of group theory that we know for all groups and therefore is true for this group of this particular model, right, you might not even think of that thing as a group, it could just be the numbers integers or whatever, yeah, and then there will be particular truths that are only true for the detailed structure that arises from some particular group, some particular model, and there is no group theory theorem that arises from that, it's just a accident that is true for a particular thing, right? but for a particular truth you could access it in two different ways in some cases that's right that's right you could say something you could prove some general result of group theory by instantiating it in a particular model of group theory that corresponds to that group in particular, well, then the claim will be that, when you look at it as a whole, okay, this is the intended claim, when you look at it as a whole, this notion of models is like the notion of frames of reference, also known as foliations, on these multi-way graphs, can you say that again?

Sorry, okay, so the claim is that the notion of models and again this is what I want to reinforce, the notion of models is related to what we have previously thought about in the case of spacetime as the notion of frames of reference okay, so what is a reference frame? a reference frame is a way of doing an equivalence class of uh, we could say, I mean, if this were in spacetime, which it's not, but we can consider the case of spacetime um, just I'm thinking to what extent we can see this, okay, let's ignore that, okay, what we're effectively doing is we're saying we're doing some kind of state equivalence here. these as these nodes indicate correctly, yes, a node equivalence class that corresponds to the things that we would consider quote-unquote simultaneous if we were thinking about this in space-time makes sense, and normally when we invent simultaneity it is a convenient way of giving it sense to space-time, that is, we could simply say that for every point in space and time you know that these are things that follow from that point, but it is convenient for us to say that no, you know if it happened now somewhere then and that happened.

I still don't think I'm explaining this as well as I'd like to be able to, but you know, the point is that doing foliations is a way of making sense of space-time. is a reduced description of space-time in which we don't have to say that each point has its own separate history, we can say that this slice of space-time has an effect that can have an effect on the next slice of space-time. well, I can, I can, I suggest adjusting the phrase do foliations to coordinate correctly because it's a little bit stronger than doing foliations, they just introduce a time coordinate, that's not the only type of coordinate that could have multiple importance, um and maybe a good analogy. that would help me is with ev was with the things that antonia and I did about evolution where you can say you know the mutation graph or the species graph, I suppose it can produce all possible biological organisms, of course, almost all . would die or never be born in the first place, and you can capture that fact simply by foliation, you say those things happen, but in infinite time, so foliation can represent natural selection, it can represent a preference for certain things to happen and other things to happen. won't occur or relative frequencies um, although in theory everything works out at some point and maybe there's something similar here, yeah, let's understand that, um, you're saying okay, so let's understand what you said there, so you're saying the graph of mutation of the dna mutation chart contains everything, but it is the library of babel, right, it is in the borje, every book is present, it is not interesting and does not contain information, but what you are saying is the fitness panorama of the world. let's say it makes you say that that particular mutation you want to foliate occurs only in infinite time, so it's like there's nothing new under the sun, but you know that the trilobite occurred early, but you know that something else could have happened early by mutation. but I didn't mean it's basically your statement I mean more or less yes, I mean I would say that humans could have occurred a billion years ago in principle by virtue of but I think it's the case that I see one of the things that tends to happen and one of the interesting things are these cones of light that you get that relate a kind of progression and time to a relationship in some version of space and that's where I think really non-trivial things start to happen, and that's why the question: What is the analogue of the cone of light in this evolutionary case?

Well, I mean, it's kind of funny, I guess, I mean, and in the context of metamathematics it might be that the analogue of natural selection or the fitness landscape is. some kind of human preference for the aesthetic qualities of particular correct or particular theorems um yeah, particular theorems I don't see what the really safe choice is, all yeah, that's right, I mean, ultimately, platonically, all mathematics already They exist like this babel library, right? but we're just like in the physical universe we're just exploring certain parts of you know we've lived a certain amount of time and you know we're also exploring well I mean it's a little bit different because I mean we could pick a It would get really a little bit strange if we said that we simply don't care what happened in this part of the universe.

We would have more and more incompatibility when saying that that part of the universe has not evolved and that is where the light cones come in. I can't maintain that consistently for long, we might say um, but that's okay, but by the way, someone asks how the monster group fits into this, just for fun, I can point it out, I mean, it's just a set of relationships. I mean, we could, we could write it, there's the icosahedral group um and uh, I don't know how many relationships the monster group has, it's not many um and what that says is that what one is saying is that if we were to build if we had to enumerate all possible, the claim that the group of monsters is a finite group is the claim that if we look at all possible sequences they go in a particular way of configuring generators if we look at all possible sequences of generators of all possible words, there are only a finite number of equivalence classes of those under the reductions corresponding to those relations, in other words, what do I mean in terms, now I don't know what the claim that something is a finite group is if it allows this possibility of adding group elements here, what does it mean that something is a finite group?

It means that when we add group elements we will always return to what it has, what does it mean to add the group elements? It doesn't really get you anywhere new because it's a finite group and therefore the number of unreachable inequivalents you're not, you're not, you know, you're no longer looking at new territory, so to speak, the multidirectional system would still be infinite. . right that's right yes I think that's right and because you're adding longer and longer words you're injecting more and more generators to add longer words but those words will always have paths back to somewhere else so It is not like this.

You could imagine that there is a tip from which you will never return. There is a one-way tip, so to speak, but that couldn't happen. How do you control that? So it feels like a weakness of this way of thinking. Is that so? something like it drifts towards these infinities, no, no, that's just in the case where I think it's Jonathan's code that makes what he called a multi-way group where you just, whether you want to or not, add generators is fine. this way of doing it where all you're doing is looking at relationships that don't happen, you're just saying when two words are the same answer, there's a theorem that says they're equal when there's a path that goes, you know, from one word to the other, so to understand, I mean the way that there are homotopies here that correspond to equivalent proofs, you know there is a homotopy between different proofs of the same theorem, can we understand that a little more?

Yeah, I mean, I find that a fast is the first thing I gave up too and way beyond what you just said in my head. Well, okay, then I mean everyone. to say is that there is a way to know that there can be two different paths that um um uh you know two different paths that um uh prove the same theorem correctly in the sense that they now have the same starting and ending point and many more those paths will be just superficially different, right, they will be differentiated by a small delta that is explained by one of the axioms of the group.

Sure we can always do we can, we can warp one path into the other by adding um completions, also known as group axioms, any path can be warped to another path by simply adding more relations that simply map the elements of one path to the elements of the other. path, okay, but if I have complete freedom to add those axioms, then I can make any path the same. like any other path, then there must be something I don't understand, is when there are two fundamentally different parts, like what are the obstructions to trivial homotopy, well I think a lot of what is discussed in homotopy type theory and things like this. it has to do with actual transformations that go from one path to an equivalent path that picture like this it is obvious what those trivial things are yes those things are yes yes it is obvious in the theorem proving approach it is saying that you are By adding endings, a termination says that there is a branch that you know you start from a node and it has a couple of branches that can go in two different directions.

If you want to combine those two directions, you need a termination that says the two elements of the two things that come out in that pair of branches are considered equivalent, in other words, you add a relation that combines those two elements in the pair of branches, okay , so, that's what it means, that's how we implement, you know, something like that. going from one path to another and that's why you know in homotopy theory, okay, in the interpretation of category theory, just to review that, I mean you know these would be isomorphisms in the interpretation of the theory of categories if They are just one-way arrows, they would be like morphisms, so in the interpretation of this from category theory we have to understand, you know, category theory is what is the correct analogy, I mean, you know thatright, that's exactly what we're talking about, yeah, I think so, so you're saying it's even called torsion as a group with torsion, yeah, that's a particular type of relationship that you can add. true, but then your point is um, your point is that the presence of those additional axioms goes from having a flat space to having a non-planar space, yes, when your coordinates are the generators, the counts of the different generators are correct, but the question is to what extent the quotes coordinate the singularity and to what extent it is a real thing, so just to remind us in these proofs, okay, this is an attempt to represent a one-path proof, the only difference here is that there are these dashed lines that represent the dependence on a lemma the reuse of a lemma so these the triangles are lemons the triangles are lemmas because the triangles are pairs of branches that became flames okay, in other words, this is a place if we look at the original multi-way system there will be a part of the multi-wave system that is one-way, okay, every time it has branched, this says I'm going to add a lemma to represent that branching, why is it done that, but this never made sense to me and Jonathan. explanations I don't know why that's an important part of theorem improvement technology because okay, because remember well, let's think about it what the theorem prover is trying to do a theorem prover is trying to find a way through this multi-way graph, right? so the question is how to find a path through the multi-way graph and this is a trick to do that because every time there might be a oh we could have gone one direction or another, add a lemma that says that says those two ways the ones we could have gone on are equivalent why can you do that? because whatever the two branches are, you know they're equivalent because let's take, let's take two branches from one of these things above, well from one of our things where we're just looking at the equivalence, in the case you can do that because let's say that this branch and This branch here are equivalent because you just derive them from the same thing so you know they're the same, you know? that this is equal to that because they would both come from this good, so what it does is it says instead of you know, instead of worrying about which branch to take, you just collapse the two branches together, you do it immediately or you wait, no, it you do. immediately you do it immediately and then I don't know which one so you do it immediately okay so what's happening here you collapse those branches and then, um, let's see, since you collapse the branches, then you continue, I mean, there's something a little confusing. about this because we need to.

I think you know that these images were drawn long before you understood multidirectional systems well. Actually, they weren't. They were drawn after I understood multi-way systems, but before we understood road systems in the context of this

project

, um, but the point is that each of these is a branch that you can follow any of the branches, um and uh, but then you have in your bag of tricks, you have that motto now and you reuse that motto later. about when it applies again now there's still a question okay maybe maybe it's an analogy I mean it just occurred to me but it's like some kind of spontaneous breaking of symmetry you know it has to be something of what you have not yet found the proof. right, you know it has to be something and there can be complete symmetry in which thing you expand first and you know one of them is going to work, you just don't know which one and you expand one of them and it just asserts the symmetry between all of them at that point like a motto, yeah, in the hope that then you can undo the symmetry by breaking later through that motto that you introduced, which is like an analogy that might help me think about it, I mean, I think this image is essentially, you know, this would be a path through the multi-track system, if it weren't for the fact that there are bits here that are bits of things coming out in the essentially gill direction. it will be a single time-like curve with things you know connected to the multi-track system where these pairs of branches correspond to alternative branches in the multi-track system.

I'd love to understand this better because especially the quality of Boolean algebra seems like a powerful way to think about multiway system branches right now, yes actually Max was just mentioning me yesterday when he realized that space type branches and branch type are like dnf and cnf, so branch is like a cool mineral. true, but in this image, you know, the question is in space-time, effectively, in our metamathematical space-time, we are looking at a path, we are modeling mathematics as a group of gd6 in metamathematics. space when modeling mathematics, I mean, we assume that mathematicians are extremely smart and come up with extremely short proofs, which is not correct, but suppose it is correct, then the question would be: do you know what the relationship is, for example, between those testing and classification?

Do you know that one of the possible ideas is that there is a notion of accumulation of lemmas that arise due to branching? Well, I'm not sure I mean there's a backlog of mottos they'll use later. You could have a field of mathematics where there are no useful lemmas being developed there is a field of mathematics where every theorem I'm not sure if this is correct I mean I don't think it can happen with strings but I think it could happen with arbitrary expressions where um where you essentially just have a single jd stick, okay, um or but just so you know, the bigger picture potentially is that you have a field of mathematics where you've accumulated a bunch of accumulated lemmas.

I'm just trying to understand what it is. the way you know the form of statement we would expect suppose there is an Einstein equation in the mathematical space of matter, basically the statement will be that the geodesics in the mathematical space of matter are deviated by the presence of accumulated lemmas , but I think this comes back to the The struggle we just had was to what extent, where, when, the curvature is intrinsic and when, is it simply a reflection of the room, a coordination, possibly, yes, possibly, but I think the coordination , you know, what seems to be the case, look how confusing.

Here it is, yes, you could think of coordination as what's the relationship? What is it? I just had a fun idea. I had a funny idea of ​​a powerful theorem as if they were very heavy objects that gravitationally lens distant theorems, as if it were difficult to understand. see them, you should yeah, that's cute, okay, that's a nice idea, a powerful theorem, eh, it corresponds to a high-mass gravitational lensing object, right, but the point is that I guess we can see further because of That, right?, we can reach more distant theorems. by virtue of the fact, well, in a sense, it's narrowing down, I don't know if it's very confusing, no, I think it's the other way around, actually, because what you really want is to know any of these looks, there's this notion of jumping . as you add a lemma, you can jump, oh my god, this is confusing, I mean, look, I think, but look as a model, as a model of what makes Paul like it if you have less respect for mathematicians and imagine them doing something that often amounts to. to a form of random search, whether they realize it or not, then what really makes the theorems good is simply that if you do a random search near them, you end up in useful places, just as they take you further. , they make your random search more effective I guess. that's the gravitational lensing connection, it could be that like the big important tests we come up with, they are often quite arbitrary, but because they exploited something powerful, they are somehow tilted in the right direction to be able to use the results, but the What I'm curious about is what is our conceptual way of thinking, so there is mathematics as it has been practiced, you know, that is the solar system that we have explored, so to speak, there is a whole universe of possible mathematics out there, what kind?

What statement can we make about the entire universe of mathematics that exists that is analogous to statements about? I mean, help. What do we get? What is the cosmological constant? Yes, okay, there is a curved math wall. There is an important point about the universe is that we have photons that have light for which time does not pass but they propagate and allow us to be sensitive to things that are happening in other parts of the universe in a way that it is not clear that there is anything analogous in in mathematics that we have explored we have only seen this is the statement this is the type of partial statement that we are making about the non-constructive proofs corresponding to the similar propagation in light of that what is the statement The statement is that if you try to foliate one of these systems, you can only do it with a kind of finite slope, not finer, with a slope less than the speed of light, so there is a test speed in any of these images. kind of a notion of test speed, which is how fast the test light cone expands, right, I mean, you can't, you can't reach things, there's only a certain speed you can reach. new new results, new expressions make I understand well, why is that not tautological?

I mean, it's an edge length by edge length. Why isn't that tautological? Because there is also a notion of space. What is the national space? because there's been a, I mean, at least there's a gill space here there's a notion of space in a gill sense, okay, in other words, it's saying there's a maximum speed if you're trying to get there, let's see if you want to know. as a common successor of these two things would take a while these two theorems that are separate these two separate expressions in bronchial space will take a while to intersect, that is the claim that there is a maximum proof speed that would also be known if we look forward down in a direction similar to time, we would also have the same effect, contact introduced an axiom or lemma that simply says: you know bb a b over there a b over here and then there is a zero distance that you can but you cannot introduce the lemma that is incompatible with the um uh with the original partial order defined by the original axioms, right, and that's what one is saying is that it cannot be introduced, so there is a limitation on the lemmas of the foliation models that can be introduced in the affirmation. are the slanders one can make to this image by adding slogans by adding valid slogans, there are limited smears one can make to this image by adding valid slogans and the claim is that there is a notion that, for example, if you try to add slogans as well, what happens if you add slogans.

Okay, so if you add equivalences that are essentially spatial equivalents, like you would do in space-time simultaneity, like add, you know additional relations that go from general groups to a specific group, yeah, and that's a lemma. We are adding that essentially it is providing new information, that is the important point, that is the important point, that there is a motto that provides new information that you did not have before and that says that this is actually equivalent to that right, that is the important . I mean you can add lemmas with bar relations that give new information, but they have to be consistent with the underlying axiom system, yeah, which is another way of saying, how you could say, these things are called billion groups, but it turns out that there are actually no groups, you could imagine them, but they don't exactly exist, of course, we know that they are articulated groups, all right, so they provide new information that wasn't there before, that's what it means to have a model. equivalences between things that were not equivalent before now those equivalences could violate the underlying law equivalences could violate our uh uh underlying set of relations here now the claim is that this constructivity of I mean, you know, okay, so the potential claim is Well, what is a model?

What is the objective of a model? The goal of a model is to say: You know, I know there are all these constraints, but what these constraints lead to is actually something we can talk about. for example, you know integers or something, there is a set of constraints, but the set of constraints is rigid enough to allow us to talk specifically about integers, it actually forces us to talk specifically about integers or specifically about this particular one. group, I mean, I'm not that familiar with group theory, you know, as you go from the main axioms to the abstract axioms of group theory and you start adding relations, okay, what obsesses the most people are the finite groups, yes, and then if you add more relations you will get some subgroup of the finite groups, etcetera, etcetera, etcetera, but I think what you're doing is yeah, I mean, essentially justyou're saying you're going, you know you're adding relationships, you're getting subgroups. basically, which is um, yeah, and at some point you get to the point where you have, for example, a finite group and then you might say uh, I don't know if you'd say that's something or not, but, I mean, I had this plot in the ncaa book um that showed um this was the degree to which a system of axioms is about something, so this shows the possible multiplication tables, like the axiom system b dot b equals a has no tables of multiplication consistent with it, so some axiom systems have like a dot b dot b equals have these multiplication tables consistent with them of size 2 these of size 3 and so on that's cool, then the argument could be which I mean is an incorrect argument, I think the fields of mathematics are really about something when they when the set of possible multiplication tables is, you know just one multiplication table, for example, right, that's what it means that it's about something and so, but but, I mean again, I just want to come back to this question because I think we're actually kind of close to being able to have a reasonable answer to this.

You know, we have the question: what claim could you imagine making about some kind of infinite metamathematics? So, for example, here is one type of statement that can be made. because this is the kind of thing we were talking about a couple of

session

s ago is this notion of constructive testing that was created by making models where the testing follows just from knowing things about the model without having to trace the entire type of application or all the individual pieces and well, look, the big statement I was going to make at the beginning of this was that the amazing thing about physics is that it's possible as in amazing.

The point is that one can say that it is not necessary to follow every micro detail of the universe. One can make these global statements that come from relativity and quantum mechanics, so the question in mathematics is what statement is analogous to the analysis statement. you're not stuck in you don't have to go down well mine and the undecidability that's probably related to you're not you're not you don't have to go down to I don't know how that relates to the question if you have to go down to the kind of irreducible level of having to go step by step without being able to use slogans, so to speak, I mean, maybe maybe maybe the analogue, what the hell is the analogue?

Look, look, the statement would be like this, well, can I have? Can I take a quick break? Yeah, and it's also making me quite sleepy, so I'm probably not going to stop thinking that I'm quite interested in the idea that quantification is like an important part of the puzzle, um, and in that. I guess it would be a surprise if mathematics isn't riddled with singularities like coordinate singularities where you just can't tell anything beyond a very short distance, there's so much curvature that your coordinates get confused and make no sense, right? But I guess they retract that they are useful and that maybe there is some scale involved that you can zoom out a little bit and there is a change of coordinates that you can do and suddenly you can talk about a new type of object that is more abstract than before and things continue to work at that new scale maybe that's my version of what you're saying, well, you're saying that there is space, right, that there is some kind of yes, things are limited to some kind of space and enough parts of mathematics that group together, for example. you have examples that are not just tautological and you find groups in other parts of mathematics.

I see what you're saying, so you're saying that the fact that this can be limited to a space rather than being full of singularities throughout the good, the claim is that the group like, for example, the idea of ​​a group is a particular type of quantification that appears in all kinds of different axiom systems; In other words, there are models of groups in all other parts of mathematics, yes, and those phenomena of The fact that mathematics can describe itself is quite common: if you look at one part of mathematics, you will see other parts of mathematics. mathematics in a sort of fractal way and that's a statement about things that don't.

Being so incredibly intricate and textured anywhere in metamathematics that there's just no quantification that lasts very long, well, you're claiming that's fine, so the claim would be that there is reasonably uniform coordination or patches of them, okay? Yeah, okay, or patches in metamathematical space and the implication of that thing you're drawing is like this, for example, this secure computational reducibility that things like groups appear elsewhere in mathematics and are not just empty descriptions of themselves , TRUE? but you can apply them elsewhere, so I mean my logical thinking, my logic for all of this is that it was the following, okay, in the physics of all possible rule systems there is an underlying irreducibility, but the point is that The behavioral aspects of those rules that we observe are those that have been ruled out by the fact that we are computationally limited, that is, we cannot do it.

We always create these equivalence classes and look only at the behavior with respect to the equivalence class, not the behavior with respect to The underlying thing and the speculation was that in mathematics the way we choose to do mathematics also does that type of grouping, probably through these axioms of extensionality, footnote because I don't know what the axioms of extensionality are, but yeah, okay, but I mean, they're just these axioms that say they're like the axiom of univalence and so on, they're axioms that They say that things that are equivalent can be treated as identical, so what's their face?

It is the identity of the Leibniz indiscernibles, is that right? I don't know, okay, yeah, okay, that makes sense. Well, I'm not surprised that Leibniz discovered this particular thing. I need to look for it. You know, I have the idea that that. The question is whether the philosophers who said things like that. Now they seem obvious. We were saying things that were always obvious, but you know, and that's why they're important. What's that? I mean, there are a lot of things that look like computational irreducibility. I think it's obvious now, but it wasn't when it was around.

I'm talking about it first, so it's um, so maybe I'll have my own um uh um, okay, anyway, um, by the way, by the way, I think it's a wonderful thing to think about and I've enjoyed it quite a bit. Thinking about it. a little bit that we all have our, I guess, intuitions and what are the things of um of uh, the Greek geometers, we were just looking at them, sorry, Euclid, yeah, yeah, Euclid, any principle or any concept the same, which postulates common notions, postulates common notions, yes. We all have our different versions of that and you can see, I guess you can see it as some kind of quantization, so things that are difficult for things that seem obvious to you might have been completely foreign to the previous generation of physicists or mathematicians. or whatever I want to say, it's an obvious statement, but no, no, I think it is too, but it's an interesting statement because that's the thing about alien intelligences and their view of physics, what you know with different , you know, but okay, my current one.

The logical thinking was that mathematics is feasible because we implicitly assume certain axioms that make us group things the same way we group things in physics and that lead us to things like relativity and quantum mechanics, so its basic point en Your basic point is fine, so I'm going to claim that the math is practically feasible and it's basically the same thing because you can reuse lemmas and so on that you've used before and you don't have to reinvent them. You don't have to reinvent everything every time you come to a new part of math. Your guest can use a lot of things you already knew to progress there, which I think is the same as it could be the case in every new place.

You get to kill the mathematical space demands its own unique coordination or set of lemmas or whatever, but without relation to anything else, without intuition to continue, you can't do any parallel transport of your ideas from the spaces where you came from. So that's a claim that you know mathematics is comparatively, so lemma reuse that you claim is a bit like parallel transportation, maybe it's not clear, but you know, I mean one, but there's a Interesting point Stephen makes, but this connects. back, I mean there's a good way to fill it back in all your super, which is that, um, it's just the parts of the math that we've had some ability to figure out, so people have been scared by everything that it did not. just impenetrable forest, right, and that impenetrable forest is, by definition, manifest computational irreducibility, right, yeah, and then there's this, there's this, it's a silly kind of um, the kind of argument where it's like, oh, We exist in the universe, yes, of course, it is an entropic argument applied to mathematics. true, of course, mathematics has been a successful enterprise and it is, by definition, that the only puzzles in which some parts were reducible, I know, but that's the claim, I mean, that's what I've been claiming for years, but the thing that I'm trying to understand now is if I mean the surprise, what I didn't know three or four months ago, six months ago, whatever, is that physics avoids computational irreducibility, that physics of the 20th century found a way to skate on irreducibility that is the surprise and so is mathematics in some way skating on irreducibility how could those things come from a common place where they seem to be and what is the clearing in the forest In both cases how could that clearing be derived from some fundamental principle, isn't it just an anthropic fact? true, no, it totally wouldn't be.

I claim that it is an anthropic fact, but I claim the reason why it is an anthropic fact is because we are computationally limited that the only thing you need to know, in other words, that the logic is that we are computationally limited implies that we construct a physical mathematical bar that we can do well, now it may not be possible, it may be that we are computationally limited and we are toast, it doesn't work. I can't figure out anything about what the universe is going to do, everything about what mathematics is going to do, but this fact that we can build, you know, you know this might not be possible, but it is, and the claim is that It is due to something.

It has to do with causal invariance, okay, it's the right to pay, so this might not be possible, but it's because of causal invariance and now the claim is, I mean, Jonathan has been claiming that everything flows from the empty infinite group that has certain, I don't know, it's uh no, but I think the infiniti groupoid is inevitably causally invariant, okay, so it could be a very elegant way of capturing something that can be developed in more English terminology, right, but, I mean, say that. He says that in the everything model it is causally invariant when we take sort of fibers of the everything model, there is a question of how much of this causal variance we inherit, but it could be that we always can, we always can. recover enough, so I think this is the logic where we are computationally limited and there is something that makes us look at only certain types of things in physics and mathematics.

I understand how that works in physics through course grades and so I understand less well how that works in mathematics and that's what I think this axiom of univalence, these principles of extensionality and so on are doing in mathematics is implementing that we're computationally limited and I think it's the analogue of that. I'm claiming my The simplistic version of this is in mathematics, all we keep are the theorems, we discard the proofs, yes, and it's somehow related to that, but you know, but this is the key point, this might not be possible, in other words, it could be the case that that.

There's no way for you to know that the mathematics that arises or the physics that arises when we sample things only in a computationally limited way could still have irreducibility, okay? That's exactly what I was about to modify from what you said or a Join this, that is, if you think of us as fundamentally following a hunch or instinct or whatever and you just think of it as a random search like effectively random , like we don't know any better when we start um causal and variation is what guarantees that random search will find pockets, that's a good point, yeah, that's a good point, right, causal variation guarantees that random search won't can be lost, yes, exactly like if you eventually find something good, we can't get lost, for example, by doing random search well that's interesting, then it means that in other words, you don't have to be that smart to get something to work, but we'll do it again to get back to the question of gravitational lensing if what we're doing is ultimately pretty stupid.

It is not intended to be an insult against the practice of mathematics, but if what we are doing isquite random and mechanical, ultimately, then we will thus perceive the undue influence of certain correct theorems that seem to have this effect. It's maybe this analogy is a little, there is a little, but yes, they bend us into causally invariant areas of metamathematical space, right, and we will simply come to observe these theorems as useful and magical, but that is a property of the curvature of not it. HE. Yes, of course, but I mean that the question then is whether, for example, one of the proposed results has not been adequately realized.

You know, non-constructive is on the border between constructive proofs and undecidability, which would be an example of a result of a general result about a type of metamathematics and you know, but again it will be that you know, what I'm still struggling with is what is the question, so to speak, in general relativity, the question is, do you know what the relationship is between mass and motion right, so the question here is what is the relationship between something like the accumulation of lemmas and proofs. I mean, because the strange thing is that, unlike what you know in physics, we see one of the things that is also quite strange in physics, at least we imagine that We are just setting up a configuration of masses and then we see what happens, we are doing an experiment, but in mathematics it is not exactly the same, I don't think so, or maybe it is, maybe we are writing down certain axioms, but I don't think it is like that because the axioms are like the laws of physics and there is something I want to say, yeah, it confuses me more like, we should probably break up, you're getting tired and I have things I have to do first.

Before I move on to some other event that I'm going to go to, but, um, uh, um, we're making progress, it's slow, but, um, uh, but in trying, I mean if I can summarize what I've been. particularly inspired by is that it's kind of nailed on to what I don't know what coordination could be like in a grammar that feels like something profitable to know models coordination systems that kind of thing um, uh um, you know and we haven't really. made. what I talked about, I mean things like undecidability etc., where we are dealing with infinity, I mean it's just an adult version of computational irreducibility, although I don't fully understand how you know that irreducibility has the consequence that makes math difficult to understand.

Undecidability has the consequence that it makes mathematics incomplete, so to speak, I mean, it's one thing to say we're doing this lemma, it extends, you know, we're taking this long sequence in this multi-way system or we. We're squashing it, but to say that there isn't necessarily, even you know we could have a thing of infinite length that, um, the thing we're asking about may not be of limited length is a slightly different topic, um, okay. it's um, we're slowly progressing, I'm, now I'm, uh, I was, I was all moving forward writing something about um, the physicalization of metamathematics, so to speak, but I'm, now I'm, um, uh, jason, yeah, yeah, basically.

I mean, you know it's one of these situations where I know I have a certain level of understanding, but I think there's a much higher level of understanding that can be achieved and it's not clear, it may be because of my process. of writing things which forces me to have a certain level of understanding, but basically it is not achievable, so to speak, you know, if I try to do something, you know, if I try to skate by writing what I know so far, everything that goes to pass. is that I'm just going to get stuck because there are going to be things that can't be scaled, so to speak, I'm sure there's an analogy here in what we've been doing, but what I want to say again is that, yeah, Well, another one. conclusion is that, um, this is rich, like there's a rich set of things going on, look, but I mean, in terms of mathematical stuff, one of the statements would be that okay, we know that mathematics is unlimited, but the The question is whether mathematics is feasible. unlimited or mathematics is going to hit a wall where it is no longer feasible and where most of the things in it you already know how uniformly feasible mathematics is.

That's a good metamathematical question because, for example, when studying cellular automata, you quickly hit walls in many directions, I mean, listen, all of this has led me to another question, you know? I've long believed that when studying things like cellular automata you hit a wall, but could it be the case that there is some sort of theory of things like types? of the theories we have now of physics or mathematics that overlook the apparent irreducibility of those systems, otherwise it hasn't seemed like you're deep into irreducibility or you've got nothing right, you should be aware of that. , I mean, you have to remember all the things you tried. with in nks with cas, but what comes to mind is something similar to what you do, it's like normalization, where I guess in the ca model you would have larger blocks of numbers and that doesn't work.

I tried it as a meta ca of some kind, that doesn't produce anything, I don't know, that produces something, I never got it to produce anything, I mean, that's something, eh, you know, basically, you know it's there, you know it's there . a way to deduce, I mean, is there a systematic way to extract reducibility? Yes, of these irreducible systems and the statement is yes, well, no, the statement is no, what is the statement? The claim is that in physics we have managed to find a way to do it. That's the achievement of 20th century physics, basically, is to extract reducibility from the right and we know we have a way to do it, we may not have found the only way to do it, we found one. way to do it based on our sensory data and whatever I mean, you know, extraterrestrial physics could be completely different, yes, but I mean I was going to suggest that as a potential irony of a 25th century computer scientist, no matter what you look back on. your treatises, you know, might say, "Well, if only Steven had known about 24th century computing, you know he would have cracked a lot of cas and it just required new structures that we haven't invented yet and that are very strange, right exactly?" you may have reached the forest, you may have changed a different type of vegetation that we simply are not equipped to do anything about, well, I know that is my statement about physics, that the physics that we have we have and that You can completely exist.

I know of disjoint theories of physics that simply look at completely different things. I mean, it's similar to my statement. You know the gas molecules in a room. You know we describe them in terms of pressure and temperature, but obviously there's a lot of additional information. which we just say, oh, that's kind of random and yeah, you're right, I mean, in some ways, some areas of science are a story of noticing things that have never been noticed before, I mean, you know, if you look, I don't. You don't know a random animal, you know and say it has this structure, but you're not looking at the molecular level.

You know the individual you know. Once you look at the molecular level, you see a completely different form of description that was. It is not possible before and I think you are absolutely right that there are forms of description that we do not know yet. There might be a relatively relativized version of computational irreducibility that simply says that there is a complicated graph of what kinds of computational processes. The analysis or system can break other types and you know, yes, there is a whole logic to it that we don't know yet, but it could have an intricate structure that could be quite fascinating, etc., right, no, I agree, I want I mean, I think so.

I think we know a certain part of it, I mean, you know, look, if we really want to go crazy about it, it's kind of the story of the hopelessness of extraterrestrial intelligence, so to speak, I mean, that's the part of things What do we know. I mean that we are completely turned in on ourselves from the things that we consider significant to the things that we recognize, etcetera, etcetera, etcetera, it's a story that you know, that we are seeing again in the case of this mathematics. um, uh um, some questions on our live stream, let's see, um, uh, would an irreducible lemon be analogous to the point of maximum entropy, so it can't be reduced without losing information?

Something like that is true, but entropy is a very complicated concept in this case. I mean, we don't have a notion of um yeah, I mean in mathematics, we don't have a notion of sets in metamathematics um, there's a point from José here that david deutsch's constructor theories are physics without probabilities, since you know that we need to understand constructive theory I sent an email to David actually recently I don't think he hasn't received a response yet basically more or less saying we need to understand constructive theory um what I like about constructive theory is that and this is more I think it's more general, it's very skeptical of probabilities being something really fundamental, at least non-determinism, well, and we have that situation too, I mean obviously in our multi-way systems there are no probabilities, it's just that it's a one thing and I think that um um, you know, I mean the other thing that's interesting about this approach to metamathematics is all this kind of invented versus discovered mathematics, this is like, you know, operationalizing that problem, there is a multi-way graph that continues. forever is what it is, we're exploring a piece and that piece is a piece that we're discovering, but I mean in um, but still, the choice of what peace we explore, yeah, I mean, it's a um, yeah from all modes.

I'm still, yeah, I think I think this point is a very circular exercise, which is one of the things that makes it confusing because it is, I mean, mathematics is in a sense narcissistic in its approach, pure mathematics. Yes, it makes it very difficult, but I think the point is, look, I mean, the fact is that to the extent that our physics project essentially reduces physics to mathematics, it simply says that this whole physical universe of ours is just certain rules and you apply them and that's how it is. In the universe we have an experience of physics to the extent that our universe is just this formal system, we have ways of describing how that formal system works that correspond to our physical experiences, so what I'm asking is what are the similar types? of descriptions we have. can give of metamathematics, which is structurally because metamathematics in this idea of ​​physics or computing, you know, the computationalism of everything, metamathematics is the same type of thing as the physical universe, so the question it's how we describe our experiences in metamathematics in the same kind of intuitive way in the sense that we're describing our experiences in physics and how we do the right thing and how we say um you know that um uh yeah, I mean, how do we set up, for For example, the analogue of reference frames?

That kind of thing I think I need to run away and it's too late for you, I know and we've been getting all kinds of interesting comments from our live stream, which we appreciate and we should probably wrap it up for today and move on to another one. It's time and I'll put this notebook in our main repository to show to you and everyone else um uh thank you certainly tomorrow um and uh yeah, that was fun and I know we have on the docket to talk about biological evolution as well and I look forward to doing so. in the next few days, yeah, that would be awesome, okay, okay, okay, friends, cheers.