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

okay hi everyone all right today it is uh taliban and me and uh we are going to be talking about mata mathematics and uh we might call jonathan if we have to but we're going to be exploring um in a sense the physicalization of matter mathematics and um uh partly i'm my test is can i explain to tally what i'm talking about um and uh that's that's the start of it okay so the idea is that uh you know we we think we have a theory of physics our theory of physics is computational the theory of mathematics the sort of fundamental theory of mathematics is also computational it says you take these axioms you use them to go from uh either expression to expression or you know proposition to proposition you build up this kind of network of of proofs and so on and so in a sense the the raw material of mathematics is has been since euclid basically been in some sense computational we now think the raw material physics is computational what can we learn from this commonality because it's a sort of a new fact that the raw material of physics is computational um and so kind of the directions is going is to say um uh you know from the things we know about physics how can we import those into mathematics in particular can we make a physicalization of matter mathematics so to speak is this making sense so far yeah the um yeah okay so and the most interesting thing is that this network of theorems idea is basically like our multi-way systems that we think are what are underneath physics and particularly underneath quantum mechanics um and so the question then is to what extent can we make uh you know to what extent can we make aggregate statements about mathematics so here's a way of thinking about it so imagine that we know the underlying axioms in mathematics let's say we we have um uh and you know in the nks book i have the summary of kind of a couple of pages that sort of show the um uh um underlying um uh kind of axioms of mathematics uh in this the sort of standard areas of mathematics so now the question is what uh you know if we imagine the infinite future of mathematics right so given an axiom system we can in principle grow this multi-way system that contains where pods in that multi-way system um is uh uh are um um where parts of the multi-wave system correspond to um the uh to proofs in um uh in in mathematics i have a question on our on our live stream from sam about whether this project is all about extending causal sets in a sense yes um that's a complicated story there's a pretty good q a answer on our website about it but it's a it's a it's a sort of a big extension hopefully we'll um um uh hopefully well maybe we'll make some other connections with it here um but uh so okay so a question then is so let's imagine that we have some um um you know we can make some typical let's let's just go ahead and do this um something simple here um let's just make some very simple things so we know what we're talking about let's imagine that we have an axiom system which is essentially just a commutativity axiom that just says a b goes to b a um oops goes to ba ba goes to a b then we can say [Music] take that and let's say we have something like something like this say eight steps or something let's say states graph okay that's a mess um all right so let's do this uh let's say graph layout oops i'm back then okay so this purports to be a little piece of this very simple version of mathematics right so any given actually this is a better example than one i've had before but anyway so any given so then a theorem here is there are many there are various theorems here like for example a theorem here is the theorem that b b a a a b a is equal to this thing down here right yes and so for example a proof of that theorem is the um so one proof would be this thing here where we say find shortest path of this comma bb aaaba two let's say that thing at the bottom a a b a b b um i think the vertices might be a little bit different you might have to look at them multi-way sometimes i think i just messed this up by just typing the wrong thing i think there's a much simpler problem for once yes much simpler problem okay so that is a path in this graph and we could highlight it and that is a proof one proof of this fact there may be many proofs of this fact right make sense i it does make sense i don't want to sidetrack you too much but one question i immediately have which is maybe too much in the details is what is the geometry of this particular graph um it's hard to tell because the you know these sort of somewhat redundant directed pairs of directed edges might be obscuring some symmetry here yeah there's probably there's all kinds of symmetry there's just a sorting rule so there's tons of symmetry in this thing i mean in the end it's a beautiful symmetrical group-like object but um i mean because because the axioms the implicit axioms of a string multi-way system are associativity axioms because string concatenation is associative so what we're adding here this is this is essentially an abelian semi group by adding this this sorting axiom we're saying it's an abelian semi group and what this object is is it it is it is something sort of underneath the caligraph of the abelian semi group right the caligraph would be let's say we take this for a group and we can do that in a minute we can take actual group axioms here where we have inverses and such like but for this this is still a semi group and for this the analog of the cali graph will be to take will be just to say what are the connected components each connected component is one element in the cali graph right because this is if we do this for a group okay so i have some code here let's see multi-way group here we go um so let's take this let's let's do this for a group all right just so we understand what's going on here but this is going to okay so this is this is one for a group so let's say multi-way group um and uh let's see what does this have this has generators relations the identity and inverses okay um all right so if we want to be really swank we can have our inverses with bars on top and things like that but let's say let's get a list of generators so let's say a and b and um let's say well let's the identity element well let's say uh a and b and let's say an identity element let's say lowercase e and inverses let's say capita lowercase a lowercase b okay and let's say relations let's have no relations here so this should be the free group ag and um now we want to start with some initial condition so i guess what we would do here is what we want to say is we could start from for example string two poles let's say five steps states graph oh what went wrong there um that's i think you actually need to give it an initial do you maybe i don't need an initial thing because the generators should imply that right yeah they okay let's try this oh my gosh 83 000 let's just try two steps here okay all right there's our free group okay let's take a look at the let's go only one step it's pathetic we only got one step oh look at that okay so this is the beginning of the free group and every one of those disconnected components should be actually you know what why don't we just take the identity element to be a null string is that going to work or is that going to confuse it should work so now let's say two steps here what a mess okay well let's try what let's see what happens if we just have one generator the free group with one generator is is going to be a rather unexciting thing okay will you explain this to me will you maybe once we've well i assume i'm serving as a proxy for the audience here that um well i'm trying to okay so what is this this is saying what this is doing is this this i hope this piece of code here is just implementing the relations in a group so what it's saying is for example a a inverse is the identity element okay now what i admit that i'm a little confused by here is there is a so this is saying that there's an element of this multi-way system it's going from the identity element this is i see so so this is what's happening is the generators in this multi-way system the generators are are being produced from the identity element by those two edges there okay so there's another identity here so this this so around if can i can i make some guesses and you tell me if they're right yeah this is an attempt to generate words in the yeah the different kinds of the different kinds of edges that are showing up here the different ways of getting edges so one will be to take any of the generators and apply it on the left or on the right to the particular vertex and we can see that happening if you just look at the empty box in the middle oh well on the left and the right they're the same thing so generator a going off to the left and also the inverse going off to the right but you can see that applying the generator to the left and to the right does yield two different things at the top and the bottom where we've got little a big a and bigger a little a on the on the top and the bottom so that's one kind of edge is just applying a generator on the left on the right and then there's another kind of edge which is applying a relation we don't have any relations here and then there's another kind of edge which is applying an inverse on the left and on the right i assume yes which is essentially a relation an implicit kind of relation do we have to have any inverses so if we if we left off little a well then it doesn't just well it would be a it would be a semi group i guess right yeah if it's a semi group then we'll have an analogous version of this picture i mean if we if we take the analogous thing here let's say i think i have code for semigroups as well um but before we go too deep into this i want to zoom out a little bit to understand what the point is and then we'll go back into this because we i really want to go through this in more detail um because this is going to be relevant i think to what we're trying to do um all right so here we've got generators we've got no it i don't think we have inverses here um and we don't have an identity okay so in this setup what this is doing is i'm not sure this is the way i would have done this actually i need to remind myself what i wrote years ago in the nks book about this very topic um let me just look here uh always a good source for to know at least what i at one time understood okay so a lot of what we're talking about here is actually what i discuss and i should i should actually bother to read what i wrote before always a good idea right after 25 years one tends to forget um i mean this is kind of the analog of one of those proofs but this is in the context not of strings but of tree-like systems right right so that's a that's a tree-like proof right where you've got an xor type operation in it it's the same idea it's it's not um um and let me see um what's this so maybe i should read that um oh wow okay that's always good huh that's a note i should actually read i mean this is this is talking about the correspondence to systems in which yeah right so this is that's a string and if we want to let me just make a note of where that is um so what is this i see i see this is giving the explicit rules that are needed to make a string based substitution system right it's it's just this is just the correspondence to to one of these systems with operators out this is just saying that the thing is uh that strings are implicitly have implicitly added an associativity that's not a remarkable fact um what i was looking for here was the correspondence to group theory um let's see oh boy okay i should read this stuff again um so this is about using lemmas which will be important later um i mean let me let me try to sketch the overall picture i'm just i'm just looking for um boy i understood this decently well 25 years ago now i just have to recover what i what i understood or thought i understood um the systems that you're looking at there in the book these operator systems are they um do you think they're the same as the as the multi-group system or not idea no not quite the operator system the point of the operating system is to have just a general expression a tree-like expression with a let's say a binary operator or an nre operator okay and that energy operator you can call it dot or something and what you're saying is you're defining the axioms defined transformations between trees just like in war from language patterns right and a difference between that and the hypographs of our physics models is that the hypergraphs are in a sense just two-level things that is the hypergraph is just a collection of relations between elements whereas the tree structure allows you to have an arbitrary depth but um where what's happening is um but you are also maintaining order right of um so in other words you have a tree and the tree is a binary tree um but you're maintaining the ordering of the tree makes sense right it has to be rooted so it's like with the hypographs that can be completely symmetric situation like a like a cycle there's no way of representing that as a tree because you'd have to chop it at some point to flatten it into the tree so this is so it's just a slightly different kind of thing that you're transforming but i don't think it makes a a huge difference to that i'm now curious what an earth i wrote in this i'm just um uh i i really need to read what i wrote before this is terrible um the uh but what i'm looking for right now is the relationship between um uh two groups let's see oh come on okay what i'm looking for is the um [Music] where i talk about uh where i talk about the correspondence between um oh boy so this is oh this is about quantifiers and whether i don't think this is relevant we shouldn't get too too wound up in this but i think we do need to understand this to understand those that way of generating this multi way um let me ask that let me ask the obvious question stephen would be um if we think of a multi-way system in which the rules are literally mathematical rules mathematica rewrite rules yep rule delays and the initial condition is an expression it's extremely well defined what that is that will be a multi-way system in general have we studied those not adequately i mean those are that is you know that's the story of arbitrary evaluation chains right so you know the evaluator does one traverse through that multi-way graph the evaluator is effectively doing i mean in a sense the evaluator is doing a single proof i mean this is you know i think the fancy version of the curry howard correspondents or whatever else you know that um this whole business about you know proofs of programs type thing that's really saying the evaluator takes a single traverse through this through this graph yeah right and and the question of what an arbitrary i mean so you know simplifying it to say only one operator let's say one binary operator no that has not been adequately studied and that is that is a um i just started studying these things as essentially multi-way generalizations as what i was calling symbolic systems which are kind of uh also analogous to combinators right because yeah because combinators are a special case of those they just have to be touring comp or some of them are touring complete instances of mathematical rewriting right right exactly but you can study the general case of that you can study the ones that aren't complete but you know i think the the big story of the multi-weight graph it's still the same and a lot of what i was going to talk about today is really just about a story oh well it starts with the story of multi-weight graphs then the multi-way graphs have to be interpreted for mathematics or for physics and that's where these kinds of issues are going to come in um but i'm still a little frustrated that i'm not finding my um my whole um discussion uh um you know it's really it's really upsetting to me how many things i i actually did understand 25 years ago that i've completely forgotten and this is one that jonathan rhee uh rediscussed recently and i had completely forgotten that i um but what i'm looking for is the discussion of how this relates to things like calligraphs um and uh um [Music] oh let me just do a search here uh oh here we go this is the discussion okay always good to actually take a look at this so right semi groups okay so so what we have in a multi-way system is a is a semi-semi group right so in a semi group one has some uh you know so what we're saying that um um okay are they called magmas or monoids or something like that which um when you relax the requirement of inverses no i think this so-called semi-tui systems i don't think they have a name in the traditional i don't think i mean monoids are just uh having an identity element um i don't think they have a name other than semi-tui system or production system so okay so let's just look at uh i mean here i i talk about okay given a particular representation of a group in terms of rules for a multi-way system often loose was the kelly graph okay so i think the caligraph is sort of a complementary thing to what we're getting in this representation here because what it's saying is you are identifying everything i mean you know i had a version of this that that was another piece of code i wrote where you're just applying the group relations you're not applying this additional weird thing that is generating elements right you're just applying group relations so that means that given a particular so so we could do that we could we could write something which just applies group relations so for example we might say um a a goes to nothing um well yeah a a goes to nothing a a goes to nothing um i think i had a resource function that actually did this um those those two relations then we want to say um uh what else else do we want um uh we want nothing goes to a a nothing goes to a a and that should be the free semi group on one element those are the relations for the free semi group on one element so if we say multi-way graph of that what we should get i mean it's not very exciting but what we should get is um if we now 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 three comma states graph oh gosh two comma states graph okay so these are the separate elements right this is these are the things which in the caligraph are all just turned into a single element right single node in the cali graph makes sense okay you understand what's going on here yeah i mean this is here let's take a simpler case let's take this case here right so these are these are each elements where right this these are all things that are just related by the by the relations in the group these are all words in the group related by the relations in the group right i mean and unless i got something wrong here oh i see oh this was kind of crazy of me right so these this particular walking through the group is going to be particularly sort of uh extreme because i'm i'm allowing identity going to a a for example and that's causing me to to go you know that that's that's generating lots of um uh lots of identities here makes sense yeah um if you wanted to only append because i mean the typical generator thing is you can you can pre-apply or post apply the generators right you don't put them in the middle of the word um which maybe you can do with like end of string arrow a beginning of string arrow a i mean those are string patterns yeah they are string patterns i mean you're just suggesting that we we should okay we should should avoid uh inserting uh identity elements in the middle of the string because i guess the fundamental point would be that there's some vertices of the graph that you produce that actually identical to other vertices under the group accents but you haven't given them enough time to settle out so sure right but the whole point is that this the whole point is every one of these consists of words that are equivalent under the group right every connected component is words that are equivalent according to the group okay yeah these are all the same group element actually which is the identity this this is that one is all the same group elements it's all identity and i i'm just trying to explain the relationship between this and a calligraph right the cayley graph is because that's going to be important to what we talk about in a minute i mean the the cayley graph it's sort of complementary to this to the view that we're taking the view that we're taking for this multi-way graph is given an element we can think of the multi-wave system as being the reductions of that element right and we can also try and have something where we're also injecting things into the system by adding i mean this is the most natural thing to do it's just given a given initial string we are just generating words that are equivalent to that initial string under the rules of some particular group for example make sense yep okay so let's go back to the big picture of what we're trying to do so so big picture is we've got you know we've got these kind of proof structures right okay so let's talk about what a few facts about mathematics are so one fact about mathematics is there's no upper bound necessarily on the length of the path you need to get from one string to another that's basically a statement of the undecidability of the word problem in the case of a group that's a statement of uh the existence of undecidable propositions in you know that's the existence of undecidability in j random mathematical axiom system right so that's so that's that story now the question is in you know what i'm trying to understand is if we uh so so one of the mysteries of mathematics is that the typical questions you ask don't involve those arbitrarily long proofs that is that mathematics is sort of doable so let's give an analogy right in in physics it could be the case that everything you care about requires going down to the most microscopic level and doing every looking at every update you want to look at right every every you know that's the story of computational irreducibility that it could be the case that everything in you know that to know what happens after one second in the history of the universe you have to do ten to the one thousand updates because you have to follow every individual update to know what's going to happen that's the sort of story of computational irreducibility but in fact the big surprise of the physics project is that you don't need to go down to that level of detail because floating on top of that level of detail are things like general relativity and quantum mechanics which are generic facts that come out from looking at the generic features of this system independent of all its microscopic details does that make sense okay so the challenge of the day is what is the analog for mathematics or meta mathematics of the bulk statements that general relativity and quantum mechanics make about the physicalized version of these multi-way graphs if if any i mean it'd be really cool if there are some but well i think that there are that's why that's why i'm doing this discussion right is um i think there can't fail to be some because i think that the raw material is the same as the raw material of physics so so in a sense so let's do another analogy so another point is in the physical world we can imagine the whole history of the universe is just some giant multi-way graph right the universe as it was in the past the universe as it is now the universe says it will be into the infinite future it 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 right yeah so similarly in mathematics we can say the ultimate platonic mathematics is just this whole giant multi-way graph right but we in in the human mathematics that we've done we've sampled only a piece of that multi-weight graph makes sense okay so the question is just like in physics we can say you know we sampled only the stuff around you know the earth or something but yet there may be laws that apply to everything we can say the same thing about mathematics that is we've sampled a few million theorems of mathematics but maybe there are general principles of how of general principles about what happens that apply across sort of all mathematics not just the part we've sampled so the question is what might there be um uh well i'm struggling to i'm starting to understand something which is the fact that we can prove sort of general abstract things you know like you you know you prove things about graphs right or groups um and it doesn't matter what the group is um how does that fit into this picture of little bubbles of computational reducibility in the what would otherwise be the hopeless tangle of physics right of microscopic closures right so so i think the answer is that a particular group and this is where i was wanted to do a bunch of specific examples a particular group is a model of the general axioms of group theory right so this particular thing here well this is this particular picture is the general axioms of abelian semi-group theory right this is this 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 semi groups right okay so if we have a particular abelian semi group that's we are two ways we can describe a particular abelian semi group we can either say we're going to add a bunch more relations to fill in the relations for the obelian semi group or we can say we actually have a multiplication table for the ability and semi group and i suppose these are equivalent things but we can we can imagine and this is where you know we can imagine essentially turning we can imagine sort of defining a model that corresponds to that particular abelian semi group and the claim from previous discussions that that we had is that we can think of a model as being like making foliations in this picture okay because a model basically is saying we are in a model one of these strings might have a value a coordinate position that's equal to another one of these strings because the actual multiplication table is some particular thing right and so what we're saying is that that in a model we're making foliations here and in the model to know whether some uh some two things are are equal we are just going to have to ask well and this is this is where i need to to tighten this up a bit but you know we're basically asking in in this case we're asking in the underlying rules for the system what follows from what okay and in other words does this this does this down here follow from this thing up here then we'll say for example that they're equal right but another way we can know that this follows from this is to say we've got some kind of foliation of this thing in which this is in a later time this is a following thing from this so in other words this set of relations here defines some kind of partial order we can try to make a um we can for example make uh foliations that that okay so there's a the claim is that there's sort of a trade-off there's either you can say to find whether this is derived from this you can either go find the collection of arrows or we can say we've pre-made some kind of model in which we know that these things occur in slices and then we just have to look at which slice this is in that make sense maybe need to more concrete example i guess okay well let's try and do a more concrete example um i'm still i'm still i'm still because radiation is pretty non-trivial right i'm still trying to think about what foliations tell you when the edges have this particular meaning of you know application of axioms of some algebraic system well so one possibility will be let's do an example where the foliations are just a count where we coordinate eyes this by counting the number of a's and b's um okay that may not that may not work very well i mean what we want to do well hold on so so in that particular example all of these are equal because the yes the rules don't change the number so yeah they're all equal so which is not a very interesting case no but if we had more rules so if we introduced generators if we introduced a's and b's on the left and on the right we would be changing the things so the point would be that if you have a set of different rules it could well be that there's some quantization that counts effectively how many times you applied one of a family of rules so these two rules don't change the a b counts but the generators that introduce new a's and b's would change the ap cons right so then it becomes a non-trivial coordinate scheme when it's actually yes then i don't think that's any more a model for standard you know what's happening here is this multi-way system is sort of modeling the standard operation of axiom systems whereas as soon as we're introducing new generators i don't think we've got quite the same scheme going on well we don't have any generators at the moment we just stuck without the number of a's and b's that you started with in the word that's correct that's correct but that's what that's what you do in you know when you prove that something is equal to something in you know in a mathematical system in universal algebra for example you're not saying oh and let's introduce a new thing because then you get something which isn't equal i mean um right so so i think the thing we have to think about here is um you know okay so one thing we can clearly do here is we can add to this some completion so to speak which says let's jump ahead in this picture right so for example here if we if we take this thing and let's add a um you know let's add a lemma okay so we've got this and now let's add uh let's see this thing here a b b a b okay so now we'll add that lemma okay so now certain proofs that we had before will have gotten shorter okay so the question is how do we think about um well surely you've introduced um some homotopy into this picture right yes because now you can you can have or homology because you can have a hole you can have a path that takes you the long way around and then the short way around via that shortcut that you introduced and you can't shrink that path anymore why not you can in this case you can shrink the path because this thing is just a speed up it's not changing where you can get to but instead what this is doing is it's re i mean thinking about it in terms of this foliation idea it's looking at it in a different frame because what we're doing here let's imagine that we have a um um i'm making sense so if i if i remove that it's just it's very hard you happen to have chosen a complicated enough system that this book i have no visual intuition let's make it simpler let's make it simpler make one b use an initial word that has exactly one b in it because then that'll introduce quite a lot of symmetry okay well first of all let's let's just look we've got multiple complicated things going on here which are unnecessary okay so let's just say we have a b b well okay aba okay okay that's it that's probably too trivial so let's say aaba let's say okay there we go there's that's one of decent complexity i think okay so this now is it com is it complete if you make it go for 20 would it be any different no that's complete okay okay all right so now okay so this is saying um okay so in a sense we are in one particular frame right now where we can say this you know let's imagine that we aggregate the one what's special about each layer here how do we characterize the layers here if i can rephrase that how do we quantize yes um to bring out some kind of symmetries or some kind of structure right well i mean one coordination is just to say the you know the time value of this thing is the number of number of updates you have to do from here to get to that thing right okay so let's say we add another rule here which is consistent with those rules so let's say we add the rule i don't know a a b a a b goes to a b a okay which is clearly consistent with the rules that we have okay so now boring why didn't that do anything i think you should go with one i think you should go with one b because it's incredibly regular and then you can make more a's so that the regularity will become really clear no but that means that it won't yeah okay just can you try it you go okay okay go back to this good so harmless okay what are you suggesting a a lots of lots of a's and one b just put a b at the end i like that because now i can understand i can understand the system all right okay okay so then let's add to that system something which is another rule right [Music] so for example aab goes to aba well the obvious one stephen is that the one with the b at the end goes to the one with the b at the front because you're just closing the loop okay okay there we go so aab goes to baa okay so now we've got a comparison between those two things and what's happened is we've traded off the intrinsic rules in the underlying system with having more complicated rules here and we've that's allowed us to shortcut the process of going from aab to be i don't even get oh i see in this one it's yeah that that particular thing is a two-step process there right yeah it would have it seems more symmetrical to have done a a a b to b a a a the full length case you know four a's okay i didn't do that just because those are the two ends of the yeah yeah i mean so that's just showing there's a direct path there as opposed to going around the big long path we've pre-computed this particular axiom this particular lemma right yeah okay fine okay so look the thing i'm trying to get to is you know is there an understanding of some analog of reference frames in this meta mathematical space by using models that's step one and then try to understand what's the analog of causal graphs here and then the you know the goal is to understand um essentially the the goal is to try and derive something uh first of all relativistic results and second of all kind of generalistic results from this okay that makes sense because the the claim is that there is a certain sense in which you know the underlying physics here is independent if models are thought of as foliations then the statement that um uh you know that this the graph is the same underneath is some statement of model independence of certain results can you explain the claim about models being thought of as foliations yeah well let's go through that claim i mean that claim is still a little bit vague right that claim is the claim is okay what is a model a model let's go through some some explicit examples of what we mean by models right so a model example of a model you know a particular group versus groups you know groups in general right yeah okay so how do we get a particular group well there are two ways we could do that one way we could do that is we could add um one approach add relations to the generic axioms to force us to have a particular group right make sense okay another approach would be to say we have a representation right and in that representation another approach is an explicit multiplication table ie representation make sense okay so let's do an example here of what we mean by that right so so when we have an explicit multiplication table that means that one of these words i think i'm losing you here but i mean one of these one of these words is you know the word has is is some kind of um you know we can just compute for every pair we can compute what the result was from the multiplication table yes yes yep okay i'm just thinking like computationally you know one yeah one one way as you said one way to have a model is you know here's a program and the behavior of the program implements the the behavior of the group right it represents elements of the output of the program correspond to group elements applying the program twice is how i multiply you know that kind of mapping it's like a complement not sure that question works because because what we're saying is look in this case an explicit multiplication table here um you know there is there are a set of inequivalent words on which this all operates am i making sense if we're going to represent in terms of words like this that's what we have to do we have to we we could as well represent it in terms of group elements right but you could also use for example like matrixes matrices as being yeah representations and that's that's totally yeah it's totally legitimate way to do it so what's the general pattern behind these models of a of that so what i'm saying is what you can do is this here is writing out i think you know we're writing out words we're writing out elements of the group we have a word represented by a sequence of generators right here okay so some of those words are identical by the relations of the group right without any group relations none of these words are identical yep that's right group right well it's yes i mean the yes or free semi group or whatever right i mean in in general with strings it will be a free semi group makes sense um and uh um i'm just i'm just noting the the inverse square lore of tallies that you're you're now further away from your camera so you're much more you you subtend a much smaller uh solid angle which makes it hard to tell what um uh yeah right um i might just be riffing here but it's always felt like groups are really about action about time right about like doing a sequence of things and the result being the same as if you did a different sequence of things that's where the relations would come in right like a structure of a particular group tells you how actions compose yes because fundamentally time is there like the words that you're building represent a sequence of actions of some kind i mean that's well just one way of thinking about groups but it's how i like to think about them and of course inverses correspond to undoing something or going back in time right what's up so but i mean so one one sense is in a group you can be you know adding you know what one notion of group one notion of time in a group which isn't the notion of time in matter mathematics by the way um involves basically appending generators one at a time that that's that's kind of does that make sense i mean that that's a i'm going to explore this group i'm going to find out what's here by adding generators to words i mean that's the very definition of a generator is the generators are the things that allow you to access any element of the group by just doing that and that's what makes them generators right so yes i agree right um you know i.e this is this is a way to construct an object that corresponds to the group right in other words if what we do is i think that's what that multi-way group thing is doing that's saying that we can construct an object that is um and in the case of the free group that object i think we had some pictures up here of what that looks like in the case of the free group do we have that yes this was the one element free group so to speak right yeah yeah these are sequences of actions that you can reach after doing one two three et cetera things at a time right but one of those actions is so there are two kinds of actions one is the add a generator action and the other is the applier relation action right i suppose that's not really an action that's just well it depends how you think about it right depends how you think about it in this in this picture of the multi-wave system it is much more granular than what you normally think of in a group i mean in a group as soon as you made a generator you know this is how you make a calligraph is you just say apply these generators and then everything all of this stuff here is squashed to a point everything or all of those edges aren't aren't there it's all just modded out yeah exactly and so that's why it's important i think for these things to emphasize that the edges are of different types i mean they're not colored but they could be to illustrate that some of those edges are the application of generators and other edges are the application of one of the relations and if you mod out by one color of that thing you'll get the the cayley graph right if you mod off by the relations you'll get the chaos um some some i just correspond to appending the generator others to applying a relation i agree right okay all right so let's let's go back to i i just want to paint the big picture here and then and we'll try and go to the smaller pieces okay so i mean the big picture is trying to understand you know what's i'm trying to understand meta mathematics in bulk if that makes sense because normally in mathematics you are understanding you know every theorem is a unique thing so to speak the goal of meta mathematics or this kind of continuum meta mathematics is to understand mathematics in bulk just like we understand space time in bulk that is we could take the point of view that you know this particular place in space has a name it's called bob or something and that's what we want to concentrate on but we don't do that we think of space in bulk right um the um well well maybe some of the dictionary is already clear to you so for example um the role of geodesics like what their shortest proofs okay um in this picture what's that proper time along a geodesic is measuring step by step how long the proof takes you to do is that is that roughly right and and the idea is that you can make a change of frame by the claim is and that's this that's the same about models is that there are two alternative ways to figure out whether something is okay so this is this is an interesting claim that there are two ways to figure out whether something is true in mathematics so to speak one is to symbolically follow the proof and the other is to say i know what thing that is in terms of a model and to conclude something just from the model from a fact about the model okay so the concept would be and let's again go go back to the question of groups right and you know a model of the abstract concept of a group is a particular group right which might be finite it might not be finite whatever it's it's some any any group obtained by adding relations to the free group is going to be in a sense a model you can think of as some kind of model of the free group a model model of groups in general um the uh yeah we're having various people on on our live stream are pointing out all sorts of things like a group can have multiple calligraphs depending on the generators you select yeah totally sure um but but if i can if i can rephrase what you've just said because i think i get it and maybe if i say it in a slightly different way you'll agree and then i'll know we have the same idea it would be that there's some truths that are evident from that are going to be true of any group and so will be true of a particular group and you could demonstrate them by doing calculations in that particular group or by just saying oh but that's an axiom of group i mean that's a that's a you know general theorem of group theory that we know for all groups and therefore it's true of this group of this particular model right that might not even you might not even think of that thing as a group it might just be the integers or whatever yeah and then they're going to be particular truths that are only true of the detailed structure that arises from some particular group some particular model and there's no real there's no theorem of group theory that comes from that it's just an accident that it's true for one particular thing right but for a particular truth you could get access to it those two different ways in some cases that's correct that's correct you could you could say something you could you could prove some general result of group theory by instantiating it in a particular model of of of group theory that corresponds to that particular group right okay so the claim is going to be that when looked at in bulk okay this is this is the attempted claim when looked at in bulk this notion of models is like the notion of reference frames aka foliations in these multi-way graphs can you say that again i'm sorry okay so the claim is that the notion of models and again i this is what i want to tighten up the notion of models is related to what we have previously thought of in the in the space time case as the notion of reference frames okay okay so what is a reference frame a reference frame is a way of making an equivalence class of uh we could say i mean if this was in space-time which it isn't but we can consider the space-time case um i'm just thinking how to what extent we can view this okay let's let's ignore that okay what we're effectively doing is we're saying we're making an equivalence class of states here think of these as states these nodes right yes an equivalence class of nodes that corresponds to the things that we will consider to be quote simultaneous if we were thinking about this in space time makes sense okay so and normally when we invent simultaneity it is a convenient way to make sense of space-time that is we could just say for every point in space and time you know these are things which follow from that point but it is convenient for us to say no you know if it happened now somewhere then and it happened that i'm still i don't think i'm explaining this as well as i as well as i would like to be able to be um but you know the whole point is that making foliations is a way to make sense of space-time is a reduced description of space-time in which we're not having to say every point has its own separate history we're able to say this slice of space time has a you know can have an effect on the subsequent slice of space time well i would can i can i suggest tightening the phrase making foliations to coordinating right because it's a bit stronger than making foliations they just introduce a time coordinate that's not the only kind of coordinate you could you could have multiple importance um and maybe a good analogy that would help me is with ev was with the things the project that me and antonia did on evolution in which you can say that you know the mutation graph or the the species graph i guess can produce every possible biological organism of course almost all of them would die or would never be born in the first place um and you can capture that fact just by foliation you say that those things do occur but at infinite time right so foliation can represent natural selection it can represent a preference for certain things to occur and others not to occur or relative frequencies um even though in theory everything is treated out at some point and and maybe there's a similar thing here right yeah let's understand that um you're saying okay so let's understand what you said there so you're saying the mutation graph of the dna mutation graph contains everything but it's it's the library of babel right it's in the borje every book is present it's not interesting and it contains no information right but then what you're saying is the fitness landscape of the world you say causes you to say that that particular mutation you want to foliate as being as occurring only at infinite time so it's it's like there's nothing new under the sun but you know like the trilobite occurred early but you know something else could have occurred early by mutation but didn't i mean is that basically your your statement i mean sort of yeah i mean it would say that the humans could have occurred a billion years ago in principle by virtue of but but i think it's the case that see one of the things that tends to happen and one of the things that's interesting is these light cones that you get which relate sort of progression and time with relationship in some version of space and that's i think where really non-trivial things start to happen right and so the question is what's the analog of the light cone in that evolutionary case well i mean there's it's a funny thing i suppose i mean and the in the context of meta mathematics it might be that that the that the analog of of natural selection or the fitness landscape is some sort of human preference for aesthetic qualities of the particular theorems right or particular um yeah particular theorems i don't see what the choice is really sure all of yeah that's right i mean ultimately platonically all of mathematics already exists like this library of babel right but we are merely just like in the physical universe we're merely exploring certain parts of you know we have lived through a certain time and you know we're also exploring well i mean it's a little different because because i mean we could pick a it would get really kind of weird if we said we just don't care what happened in this part of the universe we'd increasingly get incompatibility by saying that part of the universe hasn't evolved and that's where the light cones come in we can't maintain that consistently for very long we could say um but but okay let's let's but by the way somebody's asking how the monster group fits into this i just just for fun i can point that out i mean it is simply a set of relations i mean we could we could write it down there's the icosahedral group um and uh i don't know how many relations the monster group has it isn't very many um and what that's saying is that what one is saying is that if we were to construct if we were to enumerate all possible the statement that the monster group is a finite group is the statement that if we look at all possible sequences go in a particular represent a particular way of setting up generators if we looked at all possible sequences of generators all possible words there are only a finite number of equivalence classes of those under the reductions corresponding to those relations in other words that the i mean in term now i don't know what the what the statement that something is a finite group if we allow this possibility of appending uh group elements here what does it mean that something is a finite group it means that when we append group elements we'll always get thrown back into the thing that has um what does it mean appending the group elements doesn't really get you to anywhere new because it's a finite group and so the number of inequivalent unreachable you're not you're not you know you're no longer looking at new territory so to speak the multi-way system would still be infinite right um that is correct yeah i think that's correct and and because you're adding longer and longer words you're injecting more and more uh generators to add longer longer words but those words will always have paths back to somewhere else so it's not like you could imagine that there's a prong where you never get back there's a one-way prong so to speak but that could not happen how do you control that well then it feels like a bit of a weakness of this way of thinking about this is it sort of like veers off into these infinite no no that's only in the case where that's only in the case i think it's jonathan's code that makes what he was calling a multi-way group where where it's simply you know willy-nilly adding generators okay in this way of doing it where where all you're doing is to look at the relations that doesn't happen you're ju you're just saying when are two words the same answer there's a theorem that says they're the same when there is a path that goes you know from one word to the other word right so so just to understand i mean by the way the the sort of there are homotopies here that correspond to the equivalent proofs you know there's a homotopic between different proofs of the same theorem right can we understand that a bit more yes i mean i i find that a fast it's the thing that i first left to too and i just kind of much beyond what you just said in my head well okay so i mean all we're saying is there's a way of you know there can be two different paths that um the um uh you know two different paths that um uh prove the same theorem right in the sense that they have the same starting point and ending points now and a lot of those paths will be only superficially different right they'll differ by a small little delta that's explained by one of the group axioms sure we can always make we can we can deform one path into the other by adding um completions aka group axioms any path can get deformed to another path by just adding more relations that simply map the elements from one path to the elements of the other path okay um but if i have if i have total freedom to add those those axioms then i can just make any path the same as any other path so there must be some i don't understand there's when are two parts fundamentally different like what are the obstructions to the trivial homotopy well i think what a lot of what is discussed in you know homotopic type theory and things like this has to do with the actual transformations that go from one path to an equivalent path that picture like this is it obvious what those trivial things are yeah those things are the yeah yes it is obvious in in in the theorem proving approach it's saying you're adding completions a completion says there is a branch you know you start from one node and it has a branch pair that can go in two different directions right if you want to conflate those two directions you need a completion which says the two elements of the the two things that come out in that branch pair are taken to be equivalent in other words you add a relation that conflates those two elements in the branch pair okay okay so um that's you know that's what it means that that's how we implement you know sort of going from one um from one path to the other and that's why you know in the homotopy theory okay so in the category theory interpretation right just to just to go over that i mean that you know these would be isomorphisms in the category theory interpretation if they're just one-way arrows they'd be like morphisms so in the category theory interpretation of this we have to understand you know category theory is to what's the right analogy i mean you know the physics project is sort of um expression rewriting with expressions that don't mean anything right where all of the you know where all the actual identities of the heads have been removed so to speak that make sense and and so similarly it's i mean what we're talking about here in bulk meta mathematics is category theory well and in the physics project in general is category theory where the where the objects in the categories mean nothing right where it's purely the superstructure of category theory it's purely you know we have um know we have these objects and we have morphisms and so on and um the morphisms are just arrows and uh and all we're looking at is the structure of those arrows and so on right kind of like what wittgenstein did to philosophy but to mathematics i mean word games is not that far or from well yes it's it's a it's the yes that's the meta in meta mathematics is what we're doing is um the um uh okay so so in any case let's let's go back to this this so the question here is um if we have so we have this thing i mean we can talk about the category theory interpretation if we want to maybe we could say something about that i mean the whole point is that that the the just the graph level of this we can think of as being like a one category at least if we have transitivity yes there's a one category a category in the ordinary category yeah it's an ordinary category right so the only difference here is that in a in a full one category you have i mean i don't know i don't know what the best example of these things is that they're horribly complicated most of the examples of category theory there's got to be a really elementary example involving just you know integers and integers mod something or other something like that i need to i need to find what the the very most elementary maybe somebody on our live stream knows this the very very most elementary not requiring any advanced math uh version of of um um uh something with um um uh that's what is a nice one yeah nice categories with just being more sorry i didn't mean it's wrapped go ahead kind of categories with a bunch of morphisms yeah yeah well linear algebra is a nice one so that's already kind of complicated but go ahead tell them objects are vector spaces of whatever dimension yeah and and morphisms are linear maps between those vector spaces and what's nice about that is that like obviously composition works right if you have something from rn to rm let's an experiment rp obviously you can compose them and you'll get a linear map from rn to rp sure and then you have things like the initial object would be i guess the empty vector space the zero vector space i don't know if there's a final object it's probably not a final object and products i'm sure are things like potential products in the obvious way yeah you can certainly do that but you don't need that for ordinary category theory you're just looking at you know the sequence of morphisms yeah and what we're saying here is that the analogous thing in our multi-way system there's a fine sequence of morphisms that allows one to think of this thing like as as being like a one category and as we start thinking about these transformations between proofs effectively those are like two categories okay why is it a one category because i don't see how morphism is composed in that picture we had before so it's almost one category it's a week does that mean it means it doesn't have a transitivity property okay i mean it's just a name i mean yes no i mean you need you need to add transitivity which it does not have um the uh i mean the the thing that um you know jonathan has been excited about and xerxes have been excited about is this thing that the limit of uh when you take both you know mapping from proofs to proofs and the mapping of mappings of proofs to proofs and so on when you take the limit of all those things you get this rulial multi-way graph that i started looking at remember the one for turing machines and so the claim is that that rulial multi-way graph is an infinity groupoid you're not supposed to laugh about that i'm sure it's very cool it's just i always say explain yeah sure go ahead okay so the whole point is that what's happening is to make a mapping from proof to proof you're adding certain completions right you're adding certain additional rules okay that's how you're making that mapping okay okay so imagine that you add all possible rules you just say any rule that's conceivable any rule that you could write down is applicable that's what the rulial multi-way system is yeah right but that is also something where those those all possible rules will be the things that get you from proof to proof from proof of proof to proof of proof and so on okay right so inevitably sort of almost by definition the rule multi-way graph is the infinity group void what is an infinity group point so it's the thing that you get by taking a category okay and you take you you take this you you make um and then you're making you know a two category up to an n category by taking instead of instead of just morphisms you take the mappings you know these functors from one one category to the other you're going and then you take the the um uh so maybe you can just help maybe you can just help me understand a two category so category um objects and morphisms i'm happy yeah i know what functions are um they're the things so that the diagram commutes yes but do you now use those as now being objects in some higher yes yes yes those then become right and then you you're using those themselves so so in our case that will be the thing that would take this proof here into this proof here so that's effectively mapping from morphism to morphism it's mapping from morphism to morphism okay that's mapping from that whole chain of morphisms yeah in this particular case to that one down to one one morphism okay right and so the idea is that that the thing you get by doing that uh i mean this is i'm no expert on this stuff i mean i i but but um i believe is that you know is is what's considered to be the two category and and then as you keep going you're generating an end category where you where you just keep doing that mapping you taking the you know these uh these sequences are mapping these morphisms are mapping them to other ones you keep doing that and eventually when you've done that an infinite number of times you will get this infinity groupoid which is kind of unsurprising because the infinity group okay why is it a groupoid the it's a it's a groupoid because um once you've got all possible rules you also have every rule and its inverse and so everything which might have been a one-way morphism now becomes a uh you know an isomorphism makes sense i didn't follow that last part so so just so everyone versus semi yeah right so a a groupoid is simply something that you get by having a um uh um instead of just morphisms you have i think you have every morphism is a two-way thing so an isomorphism and also it has an identity element each each each object in the groupoid has an identity morphism which corresponds to an arrow going back to the thing itself right that's true of ordinary categories but i suppose with a groupoid you also have that every morphism can be composed with another it's in inverse such that you yield the identity for that object that's that's then a group word um no because the the thing is going from from one from one object to it you know there's a there's a mapping from one object to another object and from that object back again okay and then i guess it has to be both ways both ways around right so so and the point of a groupoid i guess is that in an ordinary group if you think about an ordinary group categorically it's only one object and it just has a bunch of morphisms that map back to that object yeah yeah right whereas a groupoid there are many objects and you have these morphisms that map between objects yeah exactly okay okay so this infinite so this infinity group point captures all this this is weird i'm just trying to wrap my hormorphisms between morphisms and so on okay and and so the point here um you know does the infinity does the infinity category contain all the other smaller categories as subcategories as objects within it or something it contains them as some kind of vibrations i think oh god oh okay and um okay so i mean the the why does one care one cares because of this growth indeed hypothesis that says that once you have an infinity groupoid then it necessarily has certain topological or perhaps geometric properties that's the claim and that in a sense you know this infinity group white is like a renormalization group fixed point in physics where by you know by going sort of and by the way okay what is the analogue of mathematics in metamathematics the infinity groupoid is the mathematics of all possible axiom systems right so you can imagine enumerating possible axiom systems each axiom system corresponds to like a field of mathematics in this infinity group word you're just throwing in all axiom systems right so that you have all transformations corresponding to any set of axioms and then to get any particular field of mathematics that's some kind of fiber inside this this infinity groupoid because what you get by following only those paths that correspond to a particular set of axioms that were a subset of the infinite set of axioms that you put into the infinity group void yeah i get that part um and that's why i think coordinatization of even these simpler multi-way groups um could be quite interesting to look at so no i know and that's why especially if the coordinates correspond to which particular subsets of the rules you know those edges come from yeah right so we want to look at coordinates but i'm trying to i'm trying to set out the kind of the big picture here um and uh because you know what then like non-trivial but powerful lemmas or any kind of theorem really would represent unexpected relationships between coordinates right they'd be like you do this three times you do that four times and you wouldn't expect it but it's the same as doing this other thing once right it's like a little bit of of of torsion in the geometry of applying not torsion curvature why aren't they can't you see them as just aspects of the same thing which tends to be you know that's asymmetric metric tenses and stuff like that the that's different from saying that i mean what you're talking about is the failure of parallel transport right which is curvature i actually mean going north one kilometer east one kilometer south and then west and then you're not back where you started which is torsion but there can also be a consequence of curvature i think for like discrete things it's a little bit fuzzy what the difference is but i'm not there so you're probably right actually you're probably right that those two things merge into each other for in the discrete case but in any case i mean so so the idea would be that you're right that the presence of of shortcuts is in a sense if everything was just a grid and to get from one uh expression to another there was just one minimal path yeah that's one thing but the fact that that isn't the case is a reflection i mean that's a reflection of essentially curvature in matter mathematical space right that's what i'm kind of getting at yeah another way of putting it is that is that if things were really boring it would you could just keep track of how many times you've done you've applied this axiom that axiom and you would have a quantization of theorem space um and that would just everything would be very dull because like there would be no way you could fully describe how to get anywhere else nobody would be proud of their mathematics because they wouldn't ever get you just you just be plodding through it you know you would have found a powerful theorem so to speak um yeah but but um right i mean so so in a sense i mean okay so so one way to think about it is there's a sort of inexorable progress of mathematics which is what you get by just following every step here right i mean what's weird okay what is mathematics what do people actually do in mathematics what they actually do in mathematics is they prove theorems which basically say you can now add to this picture an additional relation which then transforms this picture by you know completing as you can think of it as a completion it will it will conflate two things here it will it will crush up crush this picture down every time you add a a lemma that's effectively what you're doing makes sense so in some sense then so what is our picture i mean the history of mathematics we could think of as being i mean from that point of view and i'm trying to understand what what um you know i feel like the thing the thing that would bring it down to earth for because i think there are different styles of how to think about this kind of thing and mine is mine is quite i do enjoy the abstraction but i also like to see it proved out with really simple examples yes examples of the they're the grist that like makes my mental machinery run there's examples finite examples and no we need some examples we're going to get some examples don't worry we're going to get examples i i just i'm trying to make sure we understand what direction we're going in because the thing that you know the thing that i think we have been discussing previously is this idea um somehow the presence of lemmas is the presence of lemmas is really a story of curvature in that mathematical space a question it's presumably also a question it's also a story of what human beings have found like why would humans choose certain things to be lemons anything could be a lemma right well there's an intrinsically true thing no but but given a particular field of mathematics like arithmetic or something there are you know there are lemmas that correspond to paths in this you know in the system that were squashed up to you know to length one right now you can say well which lemmas do humans choose to to put in there that's a different question and that's a question of i mean that's you know the planets continue to orbit whether whether spacecraft reach them or not and you know i think it's an interesting question what the effect you know there is an abstract metamathematics out there and abstract mathematics as well that exists independent of whether humans reach pieces of it yeah but what you're saying is that um the uh um you're saying that we are distorting um that what we humans choose to do see i claim that's going to be like this foliation story that we can represent the things that we humans choose to do by the foliations which we use to understand this abstract space that is the inexorable course of mathematics and then you would make certain predictions so one prediction you would make is that the the the lemmas or theorems that are chosen to be to be particularly beautiful are those are the ones that kind of function like an like an older serial drive or whatever it's called once it's like induce lots of curvature that's useful for taking shortcuts in theorem space right well um capture a lot of curvature you know i had i had made this list of um uh let's see um let's see i'm just um yeah i'm sure you said something similar to this no no but i had an interesting thing because i i had um uh a list of types of theorems that people give and um um oh gosh what the heck would i have called this this is terrible i'm i'm so oh that's an interesting one forcing operators by axiom systems um yeah that's this question of whether you can use axioms under what circumstances you this is this question of given a set of axioms are they about a particular thing or do they admit multiple models still so for example if you do boolean algebra you can make certain constraints and eventually it will be that the only multiplication table consistent with those constraints is nand or nor in other words previously okay anyway that's a different different thing but i'm i'm looking at oh drat what it's almost that's almost the inverse right because if you yeah i don't know um i'm just i'm looking for for the the place where i discuss uh i have this kind of list of what counts as a powerful theorem what counts as a i mean what what those things mean it's empirical matter mathematics basically yeah oh i wonder whether i've got that listed in um empirical look at that that's a good sign ah terrific look at this okay so these are claims about what i don't know these are correct but but a difficult theorem a theorem having a long proof okay so these are interesting claims an elegant theorem a theorem whose statement is short and somewhat unique i know whether that's correct theorem that cannot be readily deduced from earlier theorems but is well connected i don't know if that's right either i mean these were just speculations about what um about what the kind of uh essentially graph theoretical significance of these things that we these impressions we have in mathematics um well you have this nice idea of like a wavefront of proof complexity right and if you terminate it early you'll see theorems of certain sizes and you might have to wait a really long time and then you get a really short theorem out but it took a long time to get there and that would count as an elegant theorem i think so or difficult well i see i see an elegant theorem is one way it took a long time but it ended up being short maybe registered to its proof length right or perhaps that's a powerful theorem i'm not sure maybe that's a powerful theorem um we need a we need a toy domain that is rich enough that there will be a lot of these things in practice that will pop out we'll be able to like draw some networks of theorems i think theory is the most promising i mean i think that the two theorem networks that we have we have euclid we have the theorem network of euclid um which is less exciting than you might think um oops why that's surprising i thought it would be pretty cool i'll i'll i'll show it to you uh hold on just oh it's on this page it's somewhere in this picture yeah i mean it's on that page stephen scroll down there it is okay simple enough okay so that is the that's the theorem network of euclidean we have this in the function in the um uh in the data repository so we can actually play with this thing and actually we now have because we now have actual capability to do proofs of this type in wolfram language we can see everything about these and i think we have a um uh let me just find this for a second um uh let's see mathematics oh boy these are in alphabetical order what do you know okay this is another version of that the theorem network from euclid's elements um that is a really pathetic looking object what is that i mean that's a so what we need to do what that let's just put this in here um okay so here it is um okay so let's see that that is the theorem network so now let's at least make a layered graph plot of this come on what's it doing why is that taking so long there must be something complicated about this oh there we go okay what do you conclude from this i mean i know that the proof that takes well let's find out what the proof that takes the longest to to arise is the proof of the verified platonic solids so one thing we can ask is um the uh oh yeah there's a question here what are the two clusters that is a good question i wonder whether those correspond to different books let's see we could we could label the books of euclid by colors here um we could also uh i mean maybe we could just look at a particular book um okay so those are the common notions and postulates let's see my favorite common notion i think is common notion one which is the statement that space is continuous i believe unless that's a postulate i believe that's a common notion um but those should be the things without degree it better be the case let's find out let's um uh select from the vertex list of euclid uh vertex out degree sorry vertex in degree of zero now this is going to be embarrassing if this is so the vertex end degree of zero better be what the heck what am i getting wrong here how could there be theorems whose in degree is zero and why are the common notions not of in degree zero are you sure that the edges point and the way you think you're not the opposite way that's a good question all right let's let's find that out that's some look at the out degree ah you were absolutely right um well that's that's encouraging okay that's kind of silly and we should add that to the um uh the documentation for that um for that euclid okay so there we've got the common notions so let's find out actually now i'm curious how much of euclid depends on common notion one which is my favorite non-favorite common notion so we could find out what the light cone basically of common notion one is in euclid yeah graph highlight of whatever it is odd component blah blah blah okay so let's say um well let's do let's do this and in the original euclid there um a highlight graph of the original euclid which is rather big comma and then uh what do i want to say i just want to say sub graph of euclid comma out a vertex out component of euclid comma and then that common notion is that gonna be everything do you think oh look let's do this just for fun let's take euclid's fifth posture and let's see what depends on euclid's fifth postulate did i get this wrong is it vertex in component is this backwards um yeah it's vertical and component you're right also you don't need sub graph because highlight graph accepts a list of vertices no i know it does but i want to make it look nicer by having by having everything okay so those are the things that's actually pretty interesting so those are the things that depend on the fifth postulate do a table of them one two three four five you mean just the vertex zone components so the no the highlight graph why not just show oh the different postulates well that's kind of weird oh yeah that is odd oh okay this is actually jose here is is um um maybe these are the arithmetic and the geometry of euclid maybe this is geometry maybe this is all geometry but the postulates have let's do the common notions just to let's do the same thing for the common notions how many common notions are there i should know that five okay um but by the way what's what's fun about what we're doing here is that to go back to well so they're different things so these different common notions so the first common notion about points seems to affect those pieces yeah everything that we could color differently but that they're going to overlap a lot um even yeah this this is a really fun example for a fun opportunity to think about quantization because if we think about distance from the ith common notion we have a five vector which is i mean it's good to think about time but these are other these are five parallel versions of time um and it would just be fun to think about what i don't know what what that tells us yes right so okay so one possibility one coordination is distance from different common notions and what you're saying here in general i mean there is a judicial distance in in general but let's go back to this for coordinating this thing right in this case there is a geodesic distance from that we could pick two points here basically and we can coordinate eyes by just saying there's a vector that corresponds to the gd6 distance from those two points right again given given two points here we'll give him one point doesn't matter i mean okay so look this here this picture that we have here is a organization by just asking how far do we have to go what is the geodesic distance from that point to any one of these points yeah exactly yeah right so if we wanted to we could position this we could pick two points here and we could position we could find where everything is on the plane based on coordinates from the the geodesic distances from two points okay right so and we could actually do that let's just do it i mean we could say for this let's pick one of these slightly more civilized ones let's pick let's pick this one here okay okay so now let's say that what we're going to do here is um okay so here's here's our thing and we're going to say let's pick uh so judy sick distance is graph distance from let's call this graph ggg or something right so we'll say graph distance for every for everything we're going to say we're going to get two things we're going to say graph distance in ggg from let's say a a bba to uh uh element e or something um well should we just say just say this let's say this is what we're going to do so forever the graph distances right yeah i want graph distance for every point yes yeah graph distance to every point no no drop drop the third argument you don't need that it already gives you a list of distances if you just only have two arguments so that'll give you a list of the of the one coordinate and then you'll have the list of the other one oh okay and then you just try again stephen use those as the x and y coordinates for graph layout vertex coordinates i know i was on top i was on top of that okay so let's use this one down here b a a b a a b there okay so now what we have now we're going to take those two and we're going to transpose those and those will become the um uh let's just take the transpose of those things please please make this into a function you you so often in these lab experiments you you avoid making things to functions until the very end right okay okay okay okay what do you want to do you want to say graph coordinate ties graph quantize exactly takes the graph takes the two vertices no it takes n vertices sure but we're going to want to put them in vertex coordinates i know that that could be a separator let's take n vertices um and this and what we're going to do then is is that will give us a mapping and what i want to return here is a mapping from vertex list to those sets of coordinates okay so this is going to be basically this thing is going to be this hold on so it's graph distance in g over that mapped over vertices um that thing transpose and then that thing threaded into vertex list of g well the other way would be to directly set an option on the graph using the option vertex coordinates right no i mean that's exactly what i'm going to do that's what i'm going to say is graph coordinate eyes this graph ggg with vertices a a b b a b a a b oh for goodness sake what did i do wrong list and list the okay there we go so now my claim is that all i have to do is to say graph of ggg comma vertex coordinates arrow this there we go okay so what happened here so we've got several points that were not distinguished this is actually kind of interesting we've got several points here that were in an equivalence class that had the exact same coordinate positions yeah right so to avoid that we're going to do a total absolute disgusting hack which is we're going to add a random we're going to put here random reel like minus 0.1 to 0.1 um to plus hash that over graph coordinate eyes of this this is a total hack but it should work ah what did i get wrong here graph coordinator is that no i'm going to write a function that does this properly as well why you do that what do you mean by properly i mean this is oh this is horrifying so you can use group by to just all the ones that are in the same equivalence class just they just get collapsed yeah but that's not going to help us i mean that that that will give us oh i see and then you just you why offset them so the ones that are in the same class you just add a small point one offset range let's do it let's do it let's do it okay so this is so um but the main point is okay i just want to think through what we're going to get here so what we're going to get this is a coordination by virtue of distance from given vertices which is one form of coordination um how general is that form of coordination i mean because what i'm thinking about is in um uh what i was saying there's a dual thing just briefly the other obvious one is the number of times you applied a given um relation right yes and similarly the number of times you applied a given generator if you want to go all the way back to that picture um yeah so it will be interesting just to connect them but whatever for now okay fine but i mean the whole point of coordination let's just review for a second models more traditional notions of models like we're just going to a model is a group you know as a particular group that particular group can be identified in these two ways one is by making a particular multiplication table the other is by adding relations to to produce that right okay so this is not about any relations this is closer to filling in the coordinate the filling in the multiplication table i think i mean i don't know if we do you want to think of it like that i mean i just like the idea that there's a very general way we can imagine any group any algebraic rewrite system um by by using a bunch of anchors and i agree i think that's good but i want to understand how that corresponds to what one normally thinks of in mathematics and this is a weird thing it's word distance right it's distance between words which is not i think a very common type of thing i mean there is a um but so uh you know because what i want to get to is thinking about these equivalence classes that we are getting by i mean here we've got a coordination that is completely different from our previous one our previous one let's do the coordination let's just do kind of silly coordination okay let's have two identical copies of the same thing okay so now what this is gonna do oh i see there those are just um i'm a little confused by that but basically what this is going to do if you use 0 and 1 instead of a and b it will actually be pretty clear well to be clearer because at least we'll be able to see i don't know yes we might be able to see that yeah right if you if we use 0 one um then this will be some kind of hamming distance i mean it's probably already some kind of edit distance or something yeah in this particular case because this is just the rewrite i mean there's just um reordering it's just gonna be a count of the number of well the whole thing is just is are you about to write a version of this that is uh um like well here that let's let's write the proper version okay so you say what we want to say here is um so let me let me feed you the right computational primitives so it's not actually grouped by it's i think it's um position index so here's the first point to make is that you don't actually need the vertices so vertex coordinates can just accept a list in the same order as the vertex list okay that will help it will help us a little bit then then the next function you want to use is position index because what that will do is it will find all the duplicates and give you a list of where they occur so if you just give them a list of coordinates so 0 0 1 1 2 1 1 1 again for example well here let's just take this set of coordinates here let's take um let's take one of these i mean so so you say that the vertex list is irrelevant anyway so yeah just the transfers for now okay if you do position in position index it'll give you access to the whole thing just that yeah just do that so that's telling you each key is a coordinate we didn't remember this function when we put this function in i actually proposed this function way back when it would be more useful with a second argument which i've annoyed that i never suggested but anyway um so the the values that tell you which indices that coordinate occurred in right so what we can then do is with key value map you can get access hash one will give you the key ht will give you the value and then we'll take we'll just take the key and we'll repeat it several times but with a little y offset each time okay fine okay so you're proposing but then key value map but it's got to do some kind of folding thing because it's got to remember what the how many times it's seen that particular key i don't think that's necessarily the right way to do it i mean i think another way to do it will be to say here to just take this um look actually i mean let me suggest a different possibility okay so let's take this here and then let's say here grouped by loss last come last comment first yeah or last um because you want to drop you don't need to remember the coordinates in the second thing no just remember whatever yeah well no but but this thing here right you only need to remember the the um so this is effectively values isn't that gathered by let's just gather gather will be gather will be fine or gather by last or whatever but yeah i see your point um it's just fitting i think no everything will be fiddly yeah let's just do it why didn't that get what i thought it would get oh this graph coordinates okay what's going on here are there no duplicates here yes there is a duplicate gather i did what you want look it put a a b a b okay so now gather by does that so now what we want to do is for the gathered ones um we want to for those that are gathered um we want to take yeah another thing and we wanted to take all yeah oh yeah back into xdr we want to say map uh what do you want to do change the y coordinate now let's change the y coordinates map index of something at level it might even be level three we could do level three but i was thinking doing level two because it's a bit weird to do level three at level two we want to say it is oh god we need another inner map inside here just make a function i mean because then you can use pet matching and it's so much clearer what it's doing fair enough okay all right fine so let's take this gather by i mean that map index was good but i'm saying apply a function that's nick yeah yeah i know so what i want to say is is um to each of these we want to say well let's call it munge for now we want to say munge of each one of these will be of the form um [Music] well it'll be key arrow x comma y comma yeah all right and then the index right from the map indexed yep and that wants to go to key arrow x comma y plus 0.05 um minus 0.05 i the i has to be um in a in a list on this on the left hand side on the uh yes yes yes why not well that's not going to work anyway because it's got to be the second level map indexed it'll be the second level so then blank comma okay yeah oh we'll just do it this way okay so now what we want to say is here we want to say our mapindexed of munge comma mange of okay i have to do this um last of two comma two if i'm not mistaken nice okay now we just flatten that and that's our thing so now let's let's do um let's call this okay so then this here let's call that graph coordinate i zero i don't think this one is going to be a winner here let's say graph coordinates i i i know i'm not good about these naming things but graph coordinates um x or something for extended see it's like it's like product naming when people it's 1980s style product naming support to say that's a really stuff program um it's it's um uh okay so now we want to take this and this becomes graph coordinator zero and ggg becomes g and that becomes verts and you should do one more thing once all of this is working is make a function that embeds it into the vertex coordinates as well in one go because we're going to want to play with this for a different bunch of different cases yeah yeah right okay so let's do this so graph coordinator is x um so let's just check this you know what i want to collect this code um let's put let's just have a little section here called code and more and our code is the brilliantly named munge that that that thing is 1970s style programming um uh coordinator zero coordinators x okay so here we want to say coordinate eyes x of this well that's really convincing actually we probably want to put in here a delta d y with default value uh let's say 0.1 something um and that means you have to pass that d y through t we'll just multiply that last by d y and then drop the 0.5 from i yeah and then can i suggest two more functions they're super obvious so this graph coordinates 2d which just takes graph quantities x and attaches graph you know vertex coordinates whatever and that takes yeah it obviously takes two vertices yep if you want to if you want to bother with that and then the 3d one as well because why not okay so let's say verts colon um blank comma blank um and then we might as well have a dy just for good measure here okay so this is graph coordinate as x of the verts this is graph of g comma graph coordinate is x of g verts d y um and that but that is once that's vertex coordinates arrow that right okay okay so now you suggest we make 3d version of this all right let's try running these okay so what we want to do here is we want to say that's where is ggg ggg is this thing here actually we don't care about the layered golf embedding we might do but let's just do this here um okay ggg is this okay so now we want to say graph coordinatize 2d of ggg comma that the natural thing to pick would be i mean you can pick that it's pretty random oh that's nice more offset maybe yeah well here let's just see what that looks like for okay so let's say okay interesting um so i'm going to make a prediction which is if you pick the natural anchor points which is the two b's on the left and the two b's on the right things will make more sense but you might also have to choose an initial condition that makes more sense as well yeah okay so that successfully kind of foliated this thing what is that doing now that what that's effectively doing um i think make the offset bigger stephen otherwise it's really hard to tell if those guys interact or not do they interrupt i don't know the problem is that these these bi-directional edges really don't add anything and they just make it harder to see what's going on um well we can how do we get rid of the bi-directional edges we can just do um we can do some kind of simple graph thing on this yeah simple graph and then is that enough no what do we want under undirected graph it's called undirected graph yeah i understand but then we also want to do a simple graph of the undirected graph because that will take the double edges and turn them into a single edge okay so there is actually interaction between them yes there is that's interesting well i mean this is so much fun though i mean we into a very experimental terrain like the obvious thing is just crank up the number of a's or b's right um yeah but so so let's just understand what we're doing here what we're doing here is we are forming a you know a foliation of some kind a coordination that we could have done by taking our original picture and drawing all kinds of coordinate grid lines on it right that's equivalent to what we're doing here this is a coordination of that okay so let's take um and more than that it's a continuous quadratization in the sense that um neighboring vertices distance one vertices become distance one under this quadratization so it's whatever whatever descritization of continuousness is the natural one i mean it is a natural one isn't it the underlying multi-weight graph right yeah um it's not quite in the cemetery but it's sort of it's something like that lipsticks continuous or something like that right but but so what we what we're thinking about here is let's think this is um hmm well okay what are you suggesting you're suggesting we should do some some bigger cases we should definitely do some bigger cases well yeah there's something that very natural is going to happen here which is the um because the rules that you've got just move b's bees around right so you can have what one b or two b's or three b's oh so let's just do a a b like this that's totally boring yeah and however we coordinate that let's just try let me just try to understand let's try 20 steps here and let's just try lots and lots of a's here okay so that's a one-dimensional object right as soon as we have two b's we'll have a two-dimensional object so let's take this object here and let's coordinate that and in general you're going to start with the initial condition will be one of the coordinates and the string reverse of the initial condition will be the other coordinate okay so that is that's just doing the obvious thing right okay so now the claim would be if we take the initial condition to be something with two b's ah there's no distance to a a b because you can't delete a b you've got to modify turn this into a function it's just a once all function but the point is the initial condition and the anchors are related so yeah okay but let's just let's just put string reversal let's just do this this will be again so this i claim will be let's just crank that up yeah make it big it's a grid i think some kind of grid because we see we don't want to make it too big because otherwise we're confusing ourselves by what the distances are actually we don't know what the distance we don't know what the other natural distances are so let's say we say oh boy 0.5 i'll tell you what what we can do here is say states graph structure at least then we'll see the structure of the thing oh nice it looks very much like um it's like every step it alternates which neighbors it connects to which looks like a hex grid in fact isn't wait a minute i mean isn't that this looks like the branchial graphs that you showed with uh with a's and b's it was also with a's and b's yeah remember yeah but this will also be the i mean this is ultimately the graph that you get look it's something related to that isn't it that's the graph that's just the structure i think it has to be related to this okay well then the symmetrical anchor points i mean we just happened to pick two anchor points that were obvious but they're two other anchor points which are obvious which are the ones in the middle at opposite ends right let's try that okay so which i think opposite it's like there would be opposite parity i guess they would be can you just look in that picture that you had there in the just above yeah i mean you did structure so we didn't see exactly what they were but it would be what are you suggesting you're suggesting these ones in the middle yeah no well good good sorry just go down the structure graph that you plotted yeah this one here yeah yeah so in the middle the top vertex and the bottom vertex those are also the natural i see natural anchors and i don't think that any there are any other natural anchors ah b two b's in the middle and two b's on the sides okay i mean that's obvious oh yeah b's in the middle and b's on the ends okay hold on so these in the middle is aaa bbaa and then oops okay what's going on there all right let's not do the states graph structure let's just do states graph okay that's fascinating so this is so this is distances from the the two b's are together and this is going to be distances from that guy there what about two b's on the far left i'm not seeing that anywhere where is that oh it's right underneath the two b's on the far right oh yeah i see but but it's not really i mean it's right underneath because it's a i mean that's because it's degenerate with that i mean that is it's generous yeah and it's and fundamentally this is telling you something that graph distance will never understand which is that they're actually two opposite directions here but the distance increases positively in both right so it's zero one one two two three three four but if it knew well that's because it's a directed this this happens to be undirected because we've got arrows going both ways but let's understand here if this is our coordination what theorems are obvious from this coordination right so in this coordination um you know there are things which are related by the partial order string reversal by the way gives us the two the duplicates yes but look what i'm trying to understand is what can we learn by looking at coordinate positions so the claim would be and we have a choice we can either go prove a theorem by just tracing our way through the through this multi-ray graph right or we can prove the theorem by first setting up a coordination and then making and then just looking at that coordination right so what's an example of where there is an obvious theorem based on this coordination well here's an obvious thing which is that if two things are far away in this quantization they they have to be far away in um in the original graph yes that's true yeah well look one feature of the original graph wherever it was is yeah this graph is actually a lousy example because a more interesting case is let's see how do we get from i'm thinking about sort of the everything in this graph is equal to everything else there's a path from everything to everything yeah right which is in a sense not a particularly good model you know i'm trying to understand and maybe that's why i mean yeah if we want a bit of directedness well either that or we want something which isn't simply um you know is not simply making us identical things we want something where there is directedness that adds novelty in some way like just adding in generators making sense so if we just added in generators here okay what would happen if we just added generators to this then does that give us something where where in a sense the directed paths i think it does i think it does i think if we add those in then the directed paths become the then we're generating all possible yes i think that's right i think we can do that um then directed paths become the true theorem so to speak and these these undirected pieces are just equivalences between these that make sense so if we add to this the you know append the notion of appending elements to these to these strings right then the claim is and that's what um you know i think jonathan's code was doing um go back here wherever it was well let's see do you want to do let's do multi-way semi-group um okay so the claim is that here okay so this is with the novelty generator so there's a semi group now let's see so for example our abelian semi group which is what we're looking at here includes the relations a b goes to b a b a goes to a b okay so this is correctly observed these are really they're really two kinds of arrows here which we really should be helpful too yeah exactly is there an obvious way to do that um well the original you have the original code right it might be i should i do let's go change it um uh let's see multi-way i've got the original code here um okay multi-way summing group there we go okay all right so let's say oh this is completely crazy there's two stringing stuff let's just get rid of the two strings well we're just going to assume that everything is a string doesn't matter okay so here generator rules relation rules so the problem itself is that multi-way system can't tag i mean that seems like a decent feature for multi-way system to have but some does but we can do it look we can easily do a post-process thing can't we um how would you know which one was used what is edge list of this thing it's just the edges are they're not labeled ah let's think how to do this um [Music] well i mean as a hack in this particular case anything that increases the length of the string is a generator rule i mean that's total hack no that'll you can do an edge shape function that just looks for that that will be easy and it'll draw it'll draw differently okay can we do that what do you know how to do that yeah yeah so it's just um so you're gonna yeah you're gonna take that and it'll be easier to do it as like a little post-processing function rather than redefine this whole function so it would just be takes the graph calls graph again to overload to change an option and the option wants to change is edge shape function i thought that was a deprecated okay it's not a deprecated function and then function again capital f function uh and it takes three arguments i think one is the let me just double check edge shape function um yeah so the first thing is a list of coordinates so coords and then the second thing is that is v directed edge doubling like pattern so you can't use you couldn't you can't destructure it inside the function because function doesn't support destructuring for some reason yeah okay so you're talking about edge put edge there yeah and then you need to only say yeah if string length first edge what's the third argument of function there's no third argument i was wrong okay so then just say if string length first edge greater than string like the second edge or different from i guess well let's say is if string like the first edge is less than string length of last of edge and this is a heck of a problem the problem is that there's three cases there's if they equal it's the one kind of relation and then for one side or the other side then you have to no no in this case for this case the only case of interest is it got longer which means yeah sorry my bad yeah okay so now what do i say here if this then what then arrow of codes so but you can pop the style on there right so what what do you mean so you the what this thing should return is an arrow of codes um but then you're just going to attach a style based on this property right so so it's just rf codes with style of arrow of codes or something style of error code so you could pull the error off the if statement for example yeah i know and then have the if yeah exactly that's perfect okay so style arrow chords f string length red then otherwise blue close the bracket for arrow close with the if close to the style close the function goes for the graph okay so that's saying that okay that looks fairly convincing so this is mostly a generator game in this case right this is mostly just lengthening things yeah but here oops so there's a there's an obvious feature that that multi-way should have i think which is to attach different weights to different rules and then the budget that you set is relative to a weighted total yeah that's good because for example because we want to focus really we don't mind having generators but we don't want them to predominate so we would prefer to wait up now actually we have that kind of thing in the wolfram model function and max's wolf model function has pretty elaborate termination conditions that are along those lines um okay so let's just let's just do um a color g color let's call it of g blank okay so now it's g color of this okay so the core of that thing is those relations and then there are a bunch of things okay so now let's let's make this a layered graph okay that's kind of nice actually so that what the layered graph is doing oh that's kind of weird look with no relations what is this doing with no relations if we had no relations here what is that that's just well all things are generated no i realized that all right but that object is i mean the fact that it's a it's a causal invariant creature here because adding things on the left and then things on the right you end up with the same thing oh that's a good point right but if we only add it on the left so we get this causal invariant structure because we're adding on both left and right yeah but we could but we got the same basic idea by just starting on the right i think in fact it seems it seems wasteful to add on both sides because um any sequence of a's and b's will eventually be created if you only add on the right which is sure you know you're just mixing things you're just being you will have twofold redundancy right if you do both well let's just let's just edit this code right so this code here let's call that in my 1980s way multi-way summon group x and let's say generator rules here okay there are the generators okay generator arrow that's joining on the left i think oh my god i don't find this code easy to read well let's just read it hold on one second concatenate i mean this is a table it's a two dimensional table it's table of gen goes to string join gen you know why is it going that way why is it doing it both ways around i mean it just has to append on the right yeah i don't know let's just call it right here um and uh okay look generator equals hash generator what yeah what is what is the difference in string generators oh i see oh this is doing something completely crazy here this is because he's got separate okay everything should be string generators here okay it's not one's anything that isn't a string so we're okay by just saying so generator rules i claim can you echo that so we can at least see what what it is yeah okay okay okay okay so group right now okay a goes to a a no that's way too uh that's it's incredibly redundant because all you'd want to do is just add it to the left of the entire word surely i think so but there's no way to do that with with um these generated relation setups no you can just say end of string arrow whatever that's a string pattern is that going to work in a multi-way system i mean if it doesn't then that's a bug right well okay we can let's try that first so let's say okay so let's say end of string goes to a i'd be amazed if this works i bet there's going to be error checking code that that that actually multi multi-way system seems to not check for errors it just doesn't evaluate um okay so try this thing here aab let's say two steps splatf okay would be nice if that worked if we could make that work then we can make this thing work with generators in a good way um because the thing with this is it explains why it will serve generator heavy because because i i guess to work around this thing you know right it's it's working around this problem it's just adding it's just having these relations that are just a very very you know inefficient way they're very promiscuous yeah they're matching everywhere they could everywhere that could possibly be that right okay but this so so but this layered graph is quite nice because this layered graph if we look at the bigger version of this layered graph um it's probably got a lot of um okay so the core of this is the actual relations oh nick on our live stream is suggesting that we put an x that's at the end of the string will that work the problem is well yes the generation rules would then just have to replace x with lx and i mean a x and b x that would be then we'd have x's all over the place but that's okay that's that's a that's a that's a harmless problem yeah that's not a bad problem to have um okay yeah that's a good idea so we can we can uh a hacky way to do this hacky approach just have an x at the end of each string why don't you do that i mean it's a all right it's fine okay so fine let's do it here okay so what are you suggesting we do we we you're suggesting that we put so step step one is that the multi-way system call at the end of the function right i want to rewrite this hold on one second i want to rewrite this to not have all this insanity with with um strings okay um let's just get rid of that whole idea there no it's just generators okay so there's no string generators here there's no string relations here everything is a string yeah and then the generator rules are merely thread x arrow generators well thread a little bit more a little bit more it's thread x arrow well rather do it as a map x arrow hash string catenate x you know what i'm saying hash um less than greater than x again x right map that over generators yeah and then thread that i think that's it actually you don't need anything here on that i think it doesn't so hold on and then another thing that's simpler too which is the first the initial condition for multi-layer system is just going to be x which is nice indeed and in fact don't use x use space because then we won't even see it we could use thin space you could use thin space there's probably some like invisible space or something there is an invisible space we could use invisible space that would work i mean it will confuse other things so let's not do that okay so here okay so now um what's what what do we do for relation rules here um i think that's fine that's it yeah that's the correct thing that's becomes just relations yeah and why do we need delete duplicates in case something is repeated there okay so let's try this now for our original guy here yep okay yeah it's gonna be a binary tree right so this is now the free well this is this is essentially the okay so this here is the free semi group right so we can go let's go three steps in the three semi group notice that this is actually also the calori caligraph of the free summing it's some kind of cayley graph like thing for the free semi group yeah and that's because the only edges um images yeah which is exactly what we want okay all right so now let's add some relations to this i think that gets handled by the way that redundancy where you do it both ways i think that's already happening in his catamate you see that it's doing the both ways there already so you can you don't have to type it out just for the record you can just do a b goes to ba and that's enough ah oh okay convenience feature okay okay okay okay okay okay so so is there a way using this x-ray is there a way to um deal with the coloring can we use the x does the x thing give us any clue about the coloring the space thing there's something clue about coloring no but the length trick will still work no i understand it will in this case right i want to point out and i want to point out that there's a graph theoretic object that's missing here from maybe not mathematica but it should be a resource function right which is we would definitely want to tag edges with the relations that produce them and that's something that multi-system should support directly right that it remembers which rule produced which edge but then we want something else we want to collapse a graph by modding out particular edges so we want to say we're going to take all edges of type x and mod arc vertices that connect yeah there is a tagging mechanism in for in twelve one there is pretty good tagging of edges um although i have to mod i haven't used i saw that but that would be nice it would be nice to take advantage of that for the modding operation right but the main point is that multi-way systems should be able to add edge tags okay so let's just do our coloring thing here so this is okay let's do a layered graph plot of that okay what are we learning here so this is now these arrows are rather ugly but let's let's try going five steps here why don't you do line rather than arrow because the truth is time already gives us we know that arrows point down no we don't except for the these arrows but the relations are symmetrical always so we don't need to know which direction they went all right fine um g color yeah i'm gonna do a cool well let's get let's do a structure states graph structure really what we probably want to do is to make actually let's do this let's make those dotted versus um let's see if string length is less than that then make it dotted otherwise make it red let's say well let's keep it blue do you know what would be fascinating for and would make all of this stuff quite trivial to do is if the metadata of which paths produced a given state was captured like which sequence of replacements produced a given state was captured in multi-system in the multi-wave system because then what we could do is for example the binary layout of this thing that should be the predominant layout and then the relations don't i mean that is the sequence of generators should give that is a coordinate scheme right away and it will make it nice and binding this object here and coordinates that using our coordinate system thing right so so that so we should be able to take our graph coordinates 2d right on there so graph coordinate is 2d of well let's call this gx1 no particularly good reason um gx1 and now so now what do we do to what do we want to do to coordinate this thing we could say let's take i don't know what we want but this won't necessarily even have a graph distance will it between one because this is a one-way graph so this coordination is no longer going to work i mean the thing that is appropriate is my original idea which was coordinates counting the number of generator applications in general any rule application but yeah right right right right right okay so okay but anyway could code coordinators by rule by number of rule applications um in fact we can recover that from the vertex it's just string count of the vertex and then a list a comma b because i think string card will list itself so sorry so that was what would you just saying um so if you say string count of the vertex which is a string comma a that'll tell you how many a's it has that's oh i see that's going to tell us how many well just the string length will tell us how deep we are in this picture oh yeah exactly yeah but look i want to come back to the original objective here so so this is this is a sort of x exploration mechanism so the theorems of mathematics this is a novelty generator for mathematics in addition to a theorem finder right which is something a little bit different i mean a theorem finder would just say in you know the theorems correspond to these correspond to paths in these components right and effectively what's happening here is if we were to uh sort of you know caligraphify this every one of these components will be crushed to a point yeah and what we get left with is the you know as the rest of the structure would then make the caligraph so for example we could look at the caligraph for an abelian group just for just for fun um and what we should be able to see in this thing here we should see these lumps of area which correspond to the relations in the group together with just sort of the the the generation of of um of novelty in the group but i'm still i mean i want to come back to the original objective here which was um you know the original question was okay so a model in these things would correspond to i mean th this is this is we didn't do it here but we could coordinate this that's what we did earlier yeah i'm still a little confused by this what would it mean so if we coordinate this and then what would the coordinates do that would allow us because because here's the the big picture the big picture is you have a choice you can deduce things from coordinates or you can deduce things from following edges in the original proof graph that's kind of the concept well the hope would be that and i guess the claim would be that coordinates always represent some kind of pocket of computational irreducibility that you've used i mean quadrants are just one kind of reduction right but they are a reduction and yeah they're explicitly in a group abelian group structure on some some slice of the structure yes this thing um and they allow you to shortcut things i mean they're not the only kind of shortcut but they are probably a very powerful and common kind right but another shortcut is one of these completions and that's another type of shortcut that is a particular you know a jump ahead lemma so to speak in this in the system so i mean again but but back to the sort of big picture of what one would like to understand about metal mathematics because that's that's kind of what um um you know part of part of the objective here is what is the uh you know the goal is you know what do einstein's equations say for example they say a gd sick is deflected by the presence of causal edges okay what is a causal edge in this case a causal edge is presumably that a particular lemma well a causal edge is is a relationship between um results that you got at different steps so to say that there's a causal edge well remember there's always the long way around of doing things we don't have any lemmas right but if you compress chunks of mathematics away using lemmas then you you necessarily introducing little shortcuts little wormholes um those causal edges introduce curvature in the mathematics that you experience right okay that's very vague but yeah i think that's right but it's fundamentally it's an observer effect it's not that this is really there it's that it came because you wanted to shortcut things because you wanted to compress your proofs well arguably that's the same thing as saying there's there's no you see but that's that's the problem there's there's there's things that you get from coordination and there's things that are intrinsically there and what's the trade-off between those and the answer is the answer has to be with some underlying axiom system there is intrinsically curvature in this mathematical space with another axiom system there isn't intrinsic curvature there is merely coordinate you know you can have uh you know you can have a coordinate system that doesn't have a flat metric so to speak yeah but that's but surely that's what you would expect because by introducing you can always introduce a a lemma or a completion or whatever i don't know no no but but wait a second i mean the the issue is what is the analog of um um do you get what i'm saying what the question is what's the analog of the result you know well there's a phenomenon that i know about from from black holes right where there's like a fake horizon that's not real yeah yeah that's coordinate singularity yeah so are you saying something that relates to that i'm saying that you can have all kinds of crazy coordinate systems but they don't have genuine curvature yeah the genuine curvature i mean we can perfectly well measure curvature hmm look an example of this okay if we take um i'm just i'm just looking up um oh gosh what is this now but but stephen so so so i mean general group let's say like the free group on whatever number of generators right um there's no unexpected connections there by definition that's what it means for it to be free yep um but then you have some model that's not the free group but the free group certainly maps onto it and then you do see weird identities that shouldn't be there and isn't that what we're talking about isn't that a very concrete instance of curvature meaning like i would say it is torsion like you go in this direction you go in that direction and you actually ended up at the same place even though you shouldn't have just from a pure coordinates point of view yes that's something real but that's that's produced by a particular group the pr the particular group that you chose not the general free group and in effect that's called curvature introduced by the relations that you added right that's exactly what we're talking about yes i think so so you're saying i mean that's even called torsion like a group with torsion yes that's a particular it's a particular kind of relation you can add right but so so your point is um your point is the presence of those extra axioms goes from having a flat space to having a non-flat space yeah when your coordinates are the generators the counts of the different generators right but the question is to what extent is that a quotes coordinate singularity and to what extent is something real and so so just to remind us in these proofs okay so this is an attempt to represent a single path proof the only difference here is that there are these dashed lines that represent the dependence of a lemma the reuse of a lemma so these the triangles are lemons the triangles are lemmas because the triangles are branch pairs that were turned into llamas okay so in other words this is a place if we look at the original multi-way system there will be some part of the multi-wave system that is just single way okay every time it might have branched this says i'm going to add a lemma to represent that branching why does one do that but this never made sense to me and jonathan's explanations i don't know why that's an important part of the technology of theorem improving because okay because remember well let's think about it what is the theorem prover trying to do a theorem prover is trying to find a path through this multi-way graph right so the question is how do you find a path through the multi-way graph and this is a trick for doing that because every time there might be a oh we could have gone one way or the other right add a lemma that says that says those two ways we could have gone are equivalent why do you get to do that because whatever the two branches were you know they're equivalent because let's take let's take two branches from one of these previous things right well from one of our one of our things where we're just looking at the the equivalence the case you get to do that because let's say this branch and this branch here they're equivalent because you just derive them both from the same thing so you know they're equal right you know that this is equal to that because both would arrive from this okay right so what that's doing is it's saying instead of you know instead of worrying about which branch to take just collapse the two branches together you do that immediately or do you wait no you do it immediately you do it immediately and then i don't know which one you then you do it immediately that's okay so what's happening here you collapse those branches and then um let's see given that you collapse the branches you then you keep going i mean there's something a little confusing about this because we need to i think you know these pictures were drawn long before you understood multi-way systems well actually actually they weren't they were drawn after i had understood multi-way systems but before we understood multi-way systems in the context of this this project um but the point is that each one of these is a branch you can follow either branch um and uh but then you have in your bag of tricks you have that lemma now and you reuse that lemma later on when it applies again now there's still a question okay so so maybe maybe an analogy that i mean it's just occurred to me but it's like kind of like spontaneous symmetry breaking you know that it's got to be something you haven't found the proof yet right you know that it's got to be something and there's like might be total symmetry in which thing you expand first and you just know that one of them is going to work you just don't know which one and you expand one of them and just assert the symmetry among all of them at that point as a lemma yeah with the hope that like that will you will be able to undo the symmetry breaking later via that lemma that you introduced that's as an analogy that might help me think about it right i mean i think this picture is essentially you know this would be one path through the multi-way system but for the fact that there are stubs here that are stubs of things going off in the essentially branchial direction this will be a single time-like curve with things you know plumbed into the multi-way system where these branch pairs correspond to alternative branches in the multi-race system i would love to understand this better because especially the boolean algebra quality of it seems like a powerful way of thinking about multi-way system branches right yes now i actually max had just just mentioned to me yesterday his realization that branch-like uh space-like and branch-like are like dnf and cnf so branch is like um ores cool right but so so in this picture you know so the question is in space-time effectively in our meta-mathematical space-time we are looking at a path we we're we're modeling mathematics as being a bunch of gd6 in meta mathematical space by modeling mathematics i mean we're assuming that mathematicians are maximally smart and get maximally short proofs which isn't correct but let's assume it was correct okay then the question would be you know what is the relationship for example between those proofs and sort of you know one of the possible ideas is there's a notion of accumulation of lemmas which come because of branchings well i'm not sure i mean there's an accumulation of lemmas that you're going to use later you could have a field of mathematics where there are no useful lemmas that get built up there's a field of mathematics where where every theorem i'm not sure if this is right i mean i 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 so you know so the the bigger picture potentially is you've got a field of mathematics where you have built up a bunch of accumulated lemmas i'm just trying to understand what is the form of you know the form of statement that we would expect assume there's an einstein's equation in matter mathematical space basically the statement is going to be geodesics in matter mathematical space are deflected by the presence of accumulated lemmas but i think this gets back to the struggle that we just had which was to what extent where's when is curvature intrinsic and when is it merely a reflection of the quarter a coordination right possibly so yes possibly so but i think the coordination you know what appears to be the case see the confusing thing here is yeah the coordination could be thought of as what is the relationship what's that i just had a funny i had a funny idea of like a powerful theorem as being like some very heavy objects that gravitationally lenses distant theorems right like it should be hard to see them they should yes that's that's tender okay all right that's that's a cute idea um powerful theorem uh corresponds to gravitational high mass gravitational lensing object right but the point being i guess that we can see further because of it right we can reach more distant theorems by virtue of the fact well in a sense it's reducing i don't know whether it's a that's very confusing no i think it's the opposite way around actually because because what you really want is you know any one of these look there's this notion of jumping as you add a lemma you get to jump through gosh this is confusing i mean look i i think but look as a model as a model for what makes paul like if you if you have less respect for mathematicians and you imagine them doing something that often amounts to a form of random search whether they realize it or not then really what makes good theorems is just that if you do random search near them you end up in useful places right like they take you further they make your random search more effective um i guess that's the connection of gravitational lensing it could be that like the the big important proofs that we come up with are often pretty arbitrary but because they exploited something powerful they they're kind of bent in the right direction to get to use the results but the thing i'm curious about is what is our conceptual way of thinking about so there is mathematics as it has been practiced there's you know that's the solar system that we've explored so to speak there's the complete universe of possible mathematics out there what kind of a statement can we make about the complete universe of mathematics that's out there that is analogous to statements about i mean it does help what do we get what's the cosmological constant yeah okay there's a wall of mathematics curved there's a there's an important point about the universe is that we have photons which have for which light for which time does not elapse but they you know propagate that they allow us to be sensitive to things that are happening elsewhere in the universe in a way that it's not clear there's any analogous thing in in mathematics we've explored we've only been see this is the claim this is the this is the sort of this partial claim that we're making about non-constructive proofs corresponding to light-like propagation that what is what is the claim the claim is that if you try to foliate one of these systems you can only do it with sort of finite slope with with not finer with with a slope less than the speed of light so there's a speed of proof right in any of these pictures there's a kind of notion of a speed of proof which is how fast the light cone of proof expands right i mean you you can't you can't reach things there's only a certain rate at which you can reach new new results new new expressions make sense well why is that not tautological i mean it's one edge length per edge length why is that not tautological because there's a notion of space as well because what's the national space because this knits you know like that guy there is not close to this guy here because there has been a i mean at least there's a branchial space here there's a notion of space in a branchial sense okay right so in other words it's saying that there's a maximum speed if if you're trying to get let's see if you wanted to know like a common successor of these two things would take a while these two theorems which are separate these two expressions separated in bronchial space will take a while to intersect right that's the statement that there's a maximum speed of proof which would also be you know in if we look just down a time-like direction we'd also have the same effect contact introduced an axiom or lemma that just says you know bb a b over there a b over here and then there's a zero distance you can but you can't introduce the lemma that's incompatible with the um uh with the original partial order defined by the original axioms right and that's that's the thing that one is saying is that one can't introduce that's that's why there's a limitation on what foliations models lemmas one can introduce the claim is the defamations one can make to this picture by adding lemmas by adding valid lemmas there are limited defamations one can make to this picture by adding valid lemmas and the claim is that there is a notion that for example if you try and add lemmas well what happens if you add lemmas okay if you add equivalences that are essentially space-like equivalences like you would do in simultaneity in in space-time like adding you know additional relations that go from general groups to a specific group yeah and that's a lemma you're adding that essentially is giving new information right that's the important point that's that's the important point that there's a that you can add a lemma that gives new information that you didn't have before that says this is actually equivalent to that right that's the important point i mean you can add lemmas slash relations that give new information but they have to be consistent with the underlying axiom system yeah which is another way of saying like you could say are these things called billion groups but it turns out that actually there are no groups you could imagine them but they don't exist right exactly of course we know that they are articulate groups right right so right so it's giving new information that wasn't there before so that's that's what it means to have a model is to make equivalences between things that weren't equivalent before now those equivalences could violate the underlying right the equivalences could could violate our underlying uh uh set of relations here now the claim is that this constructiveness of of i mean you know okay so the the potential claim is okay what is a model what's the point of a model the point of a model is to say you know i know there are all these constraints but the thing that these constraints are leading to is actually a a you know a thing that we can talk about so for example a um you know the integers or something right there's a set of constraints but the set of constraints is sufficiently rigid that it actually lets us talk specifically about the integers it actually forces us to be talking specifically about the integers or specifically about this particular group i mean i'm not really as familiar in group theory you know as you go from the main axioms from the abstract axioms of group theory and you start adding relations okay the thing people most obsess about is the finite groups yeah and then if you add more relations you'll get some subgroup of the finite groups etcetera etcetera etcetera but but i think what you're doing is yeah i mean essentially it's just saying you're it's going you know you're adding relations 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 whether you'd say it's about anything or not but but um i mean i had this plot in the ncaa's book um that showed um this was the extent to which an axiom system is about something so this shows the possible multiplication tables for like the axiom system b dot b equals a has no multiplication tables consistent with it so some axiom systems have like a dot b dot b equals a has these multiplication tables consistent with it of size 2 these ones of size 3 and so on that's cool so the argument could be that i mean it's a wrong argument i think that fields of mathematics are really about something when they when the when the set of possible multiplication tables is you know just one multiplication table for example right that's what it means for it to be about something and so but but so i mean again i just want to come back to this question because i think we're actually slightly close to being able to have a reasonable answer for this you know we've got the question is what statement could one imagine making about sort of infinite meta mathematics so for instance here's a type of statement one can make because this is the kind of thing we were going for a couple of a couple of sessions ago is this notion of constructive proofs being ones that were created by making models where the proof follows from a the proof follows just from knowing things about the model without you having to trace all the all the sort of app or all the individual pieces and okay so look the big claim i was going to make at the very very very beginning of this was the surprising thing about physics is that it's possible as in the surprising thing is that one can um that one doesn't have to follow every micro detail of the universe one can make these global statements that come from relativity and quantum mechanics and so the question is in mathematics what's the analogous statement the analysis statement would be you're not mired in you don't have to go down well mine and undecidability which is probably related to you're not you don't have to go down to i don't know how that's related to the question whether you have to go down to the sort of irreducible level of having to go sort of step by step by step unable to use lemmas so to speak i mean maybe maybe maybe the analog what the heck is the analog see see the claim would be that well can i take a can i take a quick crack so yeah and i'm also getting pretty sleepy so i'm probably not going so from like i'm quite keen on the idea of of quantization is like an important part of the puzzle um and in that picture it would be i guess the surprises that mathematics is not riddled with singularities like coordinate singularities where you just can't say anything beyond a very short distance away there's so much curvature that like your coordinates get scrambled and become meaningless right right but they're tracts that are useful and that maybe that there's some scale involved that you can zoom out a little bit and there's a coordinate change you can make and suddenly you can talk about a new kind of more abstract object 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 some kind of yeah the things limit to some kind of space and enough parts of mathematics that groups for example have examples that aren't just tautological that you find groups in other parts of mathematics i see what you're saying so you're saying that that the fact that this thing could limit to a space rather than being full of singularities all over the place well the claim is that group like for example the idea of a group is a particular kind of quantization that shows up in all kinds of different axiom systems in other words there are models of groups all over other parts of mathematics yeah and that phenomena of mathematics being able to describe itself is quite common that if you look at one part of mathematics you'll see other parts of mathematics in a sort of fractal like way and that is a claim about things not being so incredibly intricate and textured at any place in meta mathematics that there's just no quantization there that lasts for very long well you're claiming that there's a okay so the claim would be there is a reasonably uniform coordination or patches of them right okay well yeah okay right or patches in metamathematical space and the implication of that that you're drawing um is that well for example this computational reducibility sure that things like groups show up in other parts of mathematics and they're not just vacuous descriptions of themselves right but you can apply them elsewhere so i mean my logical thinking my logic for all of this is that was the following thing um okay in physics of all possible rule systems there's underlying irreducibility but the point is that the aspects of the behavior of those rules that we observe are ones that have been bucketed by the fact that we are computationally bounded that is we're not able to we we always create these equivalence classes and look only at the behavior with respect to the equivalence class not at the behavior with respect to the very most underlying thing and the speculation was that in mathematics the way that we choose to do mathematics also does that kind of bucketing probably through these extensionality axioms footnote because i don't know what that what extensionality axioms are but yeah okay but but i mean they're just these axioms that say that they're like the univalence axiom and so on they're axioms that say things that are equivalent can be treated as identical all right so what's his face is identity of indiscernibles leibniz is that right i don't know that okay yes okay that makes sense okay um i'm not surprised leibniz was on to this particular thing i need to look that up um you know i have this idea that that the question is whether philosophers who said things that that now seem obvious were saying things which which were always obvious but you know um and that's why they're significant what's that i mean there are plenty of things that look like computational irreducibility i think it's obvious now but it wasn't obvious when i was first yakking about it so it's um so maybe i've got my own um uh um okay in any case the um by the way by the way i i do think it's a wonderful thing to think about and i've enjoyed thinking about it a little bit that like we all have our own i guess intuitions and what are the things from um from uh the greek geometers we were just looking at them sorry euclid yeah yeah euclid euclid's whatever principles or whatever equal concept what postulates common notions postulate common notions yeah so like we all have our different versions of that and you can see i guess you can see those as some kind of quantization and so things that are hard for things that seem obvious to you might have been completely alien to the previous generation of physicists or mathematicians or whatever i mean it's an obvious statement but no no i think it's also but it's an interesting statement because that's the you know that's this whole issue about alien intelligences and their view of physics is what you know with different you know but my okay my current logical thinking was that mathematics is doable because we implicitly assume certain axioms that cause us to bucket things in the same way in the same kind of way that we bucket things in physics that lead us to things like relativity and quantum mechanics so your basic point look your basic point okay so i'm going to make a claim mathematics is is in practice doable um and it's basically the same because you can you can reuse lemmas and so on that you've used before that you don't have to reinvent that you don't have to reinvent everything every time you reach a new part of mathematics you guest can use a bunch of things you already knew to make progress there which is i think the same as i mean it could be the case that every new place you reach in mata mathematical space demands its own unique coordination or set of lemmas or whatever right but with no relation to anything else no intuition to go on you can't do any parallel transport of your ideas from spaces from which you you came right so so that is that is a statement that you know mathematics is is comparatively so the reusing of lemmas you you claim is a bit like parallel transport perhaps not clear but you know but i mean one but there's an interesting point that hold on stephen but this connects back i mean there's a nice way of completing it back into your whole uber which is that um that's just the parts of mathematics that we've had any ability to crack so like people have just been scared off from all the that didn't was just impenetrable forest right and that impenetrable forest is by definition computational irreducibility manifest right yes and so 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 yeah right it's an entropic argument applied to mathematics right like of course mathematics has been successful enterprise and it's it's that's just definitionally so the only puzzles that any parts of it were reducible at all well i know but that's the statement i mean that's the thing i've been claiming for ages but the thing that i'm trying to understand now is is it the case that i mean the surprise the thing that i didn't know three or four months ago six months ago whatever is that physics avoids computational irreducibility that the physics of the 20th century found a way to skate on top of irreducibility that's the surprise and so is mathematics also somehow skating on top of irreducibility how could those things come from a common place those seem to be in and what the clearing in the forest in both cases how could that clearing derive from some fundamental principle isn't it just an anthropic fact right no it wouldn't be totally i claim it is an anthropic fact but it's a i claim the reason it's a it's an anthropic fact because we are computationally bounded that the only thing you need to know in other words the logic is we are computationally bounded implies we build a physics slash mathematics that we can do okay now it might not be possible it might be that we're computationally bounded and we're toast it doesn't work we can't figure out anything about what the universe is going to do all 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 it is because of something to do with with causal invariance okay is the payoff right right so this might not be possible but it is because of causal invariance and now the claim is i mean so so jonathan has been making this claim that everything flows from the infinity group void which has a certain i don't know it's uh no but i think the infiniti groupoid is inevitably causal invariant okay so it might be a very elegant way of capturing something that can be developed in more english terminology right right but but i mean but to say that there's it's it says that in the that the everything model is causal invariant when we take sort of fibers from the everything model there's a question of how much of this causal on variance do we inherit but it could be that that we can always we can always get enough of it back so i mean i think this is the logic we're computationally bounded and there's a certain that causes us to look at only certain kinds of things in physics and in mathematics i understand how that works in physics through course grading and so on i understand less well how that works in mathematics and that's what i think this univalence axiom these extensionality principles and so on are doing in mathematics is implementing the we are computationally bounded and i think the the analog of that i i'm claiming my glib version of this is in mathematics all we keep are the theorems we throw away the proofs yeah and that somehow it's related to that but you know but this is the key point this might not be possible in other words it might be the case that that there's no way to you know the the mathematics that arises or the physics that arises when we sample things only in a computationally bounded way could still have irreducibility in it okay so that's where that's exactly what i was about to tweak of what you said or a join to it which is if you think of us as fundamentally just randomly going on hunch or instinct or whatever and you just think of it as random as effectively random search right like we don't know any better when we start um causal and variance is what guarantees that random search will find pockets that's a good point yeah that's a good point right i causal variance guarantees random search can't get lost yeah exactly like you'll eventually hit something good we can't get lost eg doing random search well that's interesting so that that means in other words you don't have to be that smart to succeed in getting something to work but we will but again this to go back to the gravitational lensing thing if what we're doing is ultimately quite stupid this is not meant to be an insult against the practice of mathematics but if what we're doing is quite quite random and mechanical ultimately um then we will perceive like this undue influence of certain theorems right that seem to have this effect that they i mean this is maybe this analogy is a bit there's a bit but like yeah they bend us into causally invariant areas of metamathematical space right and we will just come to observe these theorems as being useful and magical but that's property of the curvature of i don't know yeah right but i mean the question then is is you know for example one one proposed result is which again has not been properly nailed down you know non-constructive is on the border between constructive proofs and undecidability that would be an example of a result of a general result about kind of meta-mathematics and you know but again it will be you know the thing i'm still struggling with is what's the question so to speak like in general relativity the question is you know what is the relationship 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 what's weird is that unlike you know in physics see one of the things that's also quite strange in physics we at least imagine that we're just sort of putting down a configuration of masses and then we see what happens we're doing an experiment but in mathematics it's not quite the same way i don't think or maybe it is maybe we're putting down certain axioms but i don't think it is that way because axioms are like the laws of physics and there's something i mean we are yeah it confuses me rather um we should probably wrap up you're getting tired and and i have um things i have to do before i before i go on to some other event that i'm going to but but um uh um we're making progress it's slow but um uh but in trying to the um i mean the thing that if i can summarize what i've been particularly inspired by it's it's kind of nail what what i don't know what coordination might be like in a grammatical that feels like a profitable thing to know models coordinate systems those kinds of things um the uh um you know and we haven't really talked about i mean things like undecidability and so on where we where we're dealing with infinite i mean that's just a grown-up version of computational irreducibility although i don't fully understand how you know irreducibility has the consequence it makes mathematics hard to do undecidability has the consequence that it makes mathematics incompletable so to speak that is that is it is one thing to say we're making this lemma it stretches out you know we're taking this long sequence in this multi-way system or we're crushing it together but to say that there isn't necessarily even you know we could have an infinite length thing that we um the thing we're asking about may not be of of any bounded length is a slightly different issue um all right well it's um we're slowly making progress i'm i'm now uh i was i was all steaming ahead writing something about um the physicalization of metamathematics so to speak but i'm i'm now um uh jason yes yes yes basically i mean i you know it's one of these situations where i i know i have a certain level of understanding but i think that there is a much higher level of understanding that can be achieved and it's kind of it's not clear it may be that because of my process of writing things which forces me to have a certain level of understanding but basically it's it's not reachable so to speak that you know if i try and do a you know if i try and skate by writing what i know so far all that's going to happen is that i'm just going to get stuck because because there'll be things that are unscatable so to speak um i'm sure there's an analogy right here in what we've been doing but the thing i mean again the um yeah i mean well another another takeaway is just that um this is rich like there's a rich pool of things going on look but i mean in terms of matter mathematics one of the claims would be that okay we know mathematics is boundless but the question is is doable mathematics boundless or is mathematics going to hit a wall where it stops being doable and where most of the things in it you know how how uniformly doable is mathematics that's a good meta-mathematical question because for example in studying cellular automata you rapidly hit walls in many directions i mean listen this whole thing has led me to another question which is you know i have long believed that studying things like cellular automata you hit a wall but could it be the case that there is a type of theory of those things like the types of theories that we have of physics now or of mathematics that skate over the apparent irreducibility of those systems otherwise it hasn't seemed like it seemed like you're either deep down in the irreducibility or you've got nothing well you must you must have knowledge of i mean you must remember all the things that you tried with in nks with cas but the thing that comes to mind is something similar to what you do is like normalization where i guess in the ca model it would be you're just going to have blocks of larger numbers and that doesn't work and i tried that as a meta ca of some kind does that not yield anything i don't know that yields anything i never managed to make it yield out a thing i mean that that's some uh you know basically you know is there you know is there a way of deducing i mean is there a systematic way of extracting reducibility yeah from these irreducible systems and the claim is yeah well no is the claim no what's the claim um the claim is that in physics we've managed to find a way to do it that's the achievement of 20th century physics basically is to do that mining the the reducibility out of the right and and that we you know we've got one 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 our whatever i mean the you know the alien physics could be utterly different yeah but i mean i was going to suggest that as a as a potential irony of a 25th century computer scientist whatever looking back on your treaties you know they might they might say well if only steven had known 24th century computer science you know like would have cracked a lot of cas and it just required new structures that we haven't invented yet that are very alien right exactly you might you might have hit the the forest might have changed a different kind of vegetation that we're just not equipped to do anything about well i know that's that's my claim about physics that that the physics we have we have and that there can be completely you know disjoint theories of physics that simply look at completely different things i mean it's you know it's similar to my claim you know molecules of gas in a room you know we describe them in terms of pressure and temperature but there's obviously a huge amount of other information which we just say oh that's kind of random and yes you're right i mean the you know in in some respects some areas of science are a story of noticing things that were never noticed before i mean you know if you look at i don't know a random you know animal and you say well it has this structure but you're not looking down at the molecular level at you know the individual you know once you look at the molecular level you see a whole different form of description that wasn't possible before and i i think you're quite right that there's forms of description that we just don't know yet um there could be a relative a relativized version of computational irreducibility that just says there's a complicated graph of like what kinds of computational analysis or system can break other kinds and you you know yes there's just a whole logic of that that we don't know yet but that might be have might have intricate structure that could be quite fascinating etc right no i agree i mean i think i think that we know a certain slice i mean you know look if we really want to get crazy about it it's kind of the the story of the hopelessness of extraterrestrial intelligence so to speak i mean that is that that the slice of things that we know is i mean we are completely folded back on ourselves of the things that we consider significant of the things that we recognize et cetera et cetera et cetera it's it's a it's a story that there's you know which we're seeing again in the case of this mathematics um the uh um some questions on our live stream let's see um uh would an irreducible lemon be analogous to point of maximum entropy so you can't reduce it without losing information something like that is true but entropy is a very complicated concept in the case of i mean we don't have a notion of um yeah i meant to mathematics we don't have a notion of ensembles in metamathematics um there's a point from jose here that david deutsch's constructor theories physics without probabilities since i you know we got to understand constructive theory i sent david in mail actually recently i don't think i don't think i got 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 he's like he's very skeptical with probabilities that are real fundamental thing at least non-determinism well right and we have that situation as well i mean obviously in our multi-way systems there are no probabilities it's just um it is a it's a thing and i think that um um you know i mean the other thing that's interesting about this approach to metamathematics is this whole sort of mathematics invented versus discovered this is kind of you know operationalizing that issue there is a multi-way graph it goes on forever it is what it is we are exploring a piece of it and that piece is a piece that we are discovering but i mean in in um but yet the choice of what peace we explore yeah i mean is it is a is a um yeah anyway i'm i'm still yeah i think i think this point it's a very it's a very circular exercise which is one of the things that makes it confusing because it's such a i mean mathematics is so in a sense narcissistic right in its focus pure mathematics yes it makes it very difficult but i think the point is look i mean the fact is that insofar as our physics project is reducing essentially physics to mathematics it's just saying this whole physical universe of ours it's just certain rules and you apply them and it does the universe we have an experience of physics insofar as our universe is just this formal system we have ways of describing how that formal system works that correspond to our physical experiences right so what i'm asking is what are the similar kinds of descriptions that we can give of metamathematics which is structurally because meta mathematics in this idea of physic of of compute you know computationalism of everything the meta mathematics is the same kind of thing as the physical universe so the question is how do we describe our experiences in meta mathematics in the same kind of intuitive way in a sense that we're describing our experiences in physics and how do we right and how do we say um you know that um uh yeah i mean how do we for example set up the analog of reference frames all those kinds of things i think i need to rush off and it's really late for you i know and um we've been getting all kinds of interesting comments from our live stream which we appreciate um and we should probably wrap up for today and continue another time and i will put this notebook in our main repository so it will show up for you and everybody else um uh thanks certainly by tomorrow um and uh yeah that was fun and and i know tally i know we have on the docket to um uh talk about biological evolution as well and i look forward to doing that in the next couple of days yeah that would be that'd be awesome okay cool all right okay folks cheers

Channel: Wolfram

Views: 45,281

Keywords: Wolfram, Physics, Wolfram Physics, Wolfram Physics Project, Stephen Wolfram, Science, Technology, Wolfram Language, Mathematica, Programming, Engineering, Math, Mathematics, Nature, A New Kind of Science, NKS, Computer Science, Philosophy

Id: VlqerIL2kl8

Length: 237min 16sec (14236 seconds)

Published: Tue Aug 04 2020