Matt: 0:14

Hello everyone And welcome to the switch statement podcast It's a podcast for investigations into miscellaneous tech topics Hey, John, how are you doing?

Jon: 0:34

Hey Matt, how are you?

Matt: 0:36

I am doing all right.

Jon: 0:38

Are you infuriated by this Mew puzzle?

Matt: 0:41

I am just seething right now because think we were misled.

Jon: 0:46

We were trolled.

Matt: 0:47

he told us,

Jon: 0:49

70s Hofstetter trolled us in 2024.

Matt: 0:54

yeah, dude, and, and will long into the future, So what we're talking about is the Mew puzzle. This is the name of this chapter. I think, I think he does a good job here easing us into the world of formal systems.

Jon: 1:08

Yes. Yeah.

Matt: 1:10

uh, the whole, yeah, the whole point of this chapter is to lay out this very small universe, almost like the minimal universe where there is an interesting question you can ask about it. and he calls that the mu puzzle.

Jon: 1:23

And he kicks off the chapter, so I guess this'll be the thing in this book where he'll have these like, um, What do they call them? What does he call them? The, uh, dialogues or something? he has a word for them, which I don't want to look up right now, but he kicks off each chapter with kind of this weird parable type thing, and this one was kind of a, I don't, I don't know if I want to use the word funny, version of Zeno's Paradox, where it was like this dialogue between Achilles and the tortoise, and they were talking about doing a race. and there's a thing called Zeno's Paradox where if you keep moving halfway to a point, you will never get there. It's kind of a paradox that disproves that motion is even possible.

Matt: 2:10

Right.

Jon: 2:10

which I feel like is very, you know, on brand for this book. Like kind of disproving things that are clearly real by twisting words around.

Matt: 2:21

Um, do you know, do you know the resolution to Zeno's paradox?

Jon: 2:26

The resolution that, like, makes it false?

Matt: 2:29

Well, cause clearly, like, I mean, the thing that makes Zeno's paradox a paradox is that clearly Things move.

Jon: 2:36

Right.

Matt: 2:37

Um, cause, cause like, so basically I think what, what, what is, you know, this paradox says is, you know, Achilles and the tortoise are racing. Right. So the tortoise starts off with a headstart once Achilles runs to where the tortoise was, the tortoise will have moved.

Jon: 2:54

Right.

Matt: 2:55

And then you can do that again and do that again, but the tortoise is always going to be ahead of Achilles, like, because you can keep on doing that, you know, ad infinitum

Jon: 3:04

Which is completely absurd.

Matt: 3:06

but like, clearly in the real world, like, eventually Achilles will pass the tortoise. So it's like, what's the resolution to the paradox? And, and so I guess my question is, do you, have you heard, like, I, I didn't figure this out myself. I watched a number file video about it, but,

Jon: 3:21

Oh, I see what you're asking. Like, there's actually, like, a mathematical disproof or something. Of Oh, no, I'm not aware of this. Um, I just thought it was, like, one of those things that was clearly not true. Oh.

Matt: 3:36

It's funny because nothing in the presentation Xenos paradox is false. It's just mis representative. So. The resolution of the paradox is that, yes, if you keep on doing those additions, yeah, you'll, uh, Achilles will never pass it, but those, those time steps become infinitesimally small to the point where the amount of time converges towards a finite amount. So basically that, that series only ever will sum up to be the point where they cross. But it's, it's only a small, like the, the trick that the paradox plays on your mind is you kind of imagine each one of these time steps as being roughly equal in time. So eventually if you add a, if you add them all up, like it'll be infinitely long in time

Jon: 4:27

Yeah.

Matt: 4:27

and they'll never cross. But the point is it's the distance is bounded and the time is bounded of that summation. So it's just not modeling, uh, anything past. The time or the space of Achilles crossing the tortoise.

Jon: 4:43

Yeah. Ah, I think it makes sense. I think this is gonna be an issue for me with this book, where I was never one to, like, really explore these types of, like, Like, I almost think of these as, like, nonsensical word puzzles, where you're just, like, You know, you're, you're describing something in a way that kind of breaks reality. And I, I've, the way my brain has always worked is like reality is reality. And sure, you can like describe it in any way, you know, some, some of which might break reality, but can't actually break reality with words. And I, I feel like I have this thing where my brain just kind of like, Turns off when this type of thing is being discussed. I think I'm just, um,

Matt: 5:33

you're breaking out of the system, it sounds like. I,

Jon: 5:36

I'm breaking out of the system. he started the chapter and I, I really perked up because he basically introduced formal systems. Which you and I have spent most of our lives dealing with formal systems.

Matt: 5:57

so funny that you say that because any programmer who has learned about like searching or, It has taken a class in algorithms. Like they will feel very at home because it feels like I'm just like, okay, this is another algorithms problem. Or I'm like searching through a graph or, you know,

Jon: 6:17

Yeah. It's funny because in this chapter, there were so many things that my, my brain is like so trained to, to just immediately internalize, you know, like he, he mentions the rules of this mu, you system and immediately my brain is like, okay, these are the rules and it will perform the calculations and not, you know, keep the rules intact. But then there were things in this chapter that my brain is not trained to do. And I was like, Oh, this is very cool. Like, I hope he goes into more detail on this. Cause like, this is a skill that I would like to have. Um, and anyway, maybe we just start jumping in and describing what the system is.

Matt: 7:00

yeah, let's, let's talk about it. So the, the mu puzzle is fundamentally it's a string manipulation puzzle. So. You have, you start with a string of letters and then you are given a series of rules about how you can modify those letters, sometimes under certain circumstances. so basically they say, okay, well, if you start with the string M I, is it possible to, with, you know, just by rigorously applying the rules to wind up with the string M U? So that's kind of like the way the puzzle is proposed. Um,

Jon: 7:41

front of you by any chance? I, didn't write them down in my

Matt: 7:43

yeah, I have them here so I can, I can just go, go through them quickly. So, um, rule one is if your string ends in an I, you are allowed to add a U at the end of it. So that one's pretty, pretty straightforward.

Jon: 7:59

So if you start with M I, you can convert that to M I U.

Matt: 8:02

boom. M I U. Yeah. So if you have the string M X, and now we should say the only letters, the only literal letters you're actually allowed to have in your string is M, I, and U. Uh, so, um, if you have the string M X, you're allowed to produce the string M X X.

Jon: 8:27

Yeah, and X represents everything after M. So if you have, if you have M I, you can create M I I. But then you can create M I I I I. Because you basically have to repeat everything after the M.

Matt: 8:46

So I think of this as just like the doubling rule. So like, you know, you have the M and then you could just like double everything after the M. Um, and now rule three is if you have, I, I, I in your string, you can turn that I, I, I into a U.

Jon: 9:05

Right. So if you, so if you start with M I, you can create M I I. Then you can create M I, I, I, I, and then you can convert any of those blocks of three eyes into a U so you can create M. I. U. or M. U. I.

Matt: 9:23

Which, and we already generated, uh, MIU, right? Through another, through another route, right? last rule, uh, pretty straightforward. If you have UU, two consecutive U's, you're allowed to squish them down into nothing. You can just obliterate those U's.

Jon: 9:41

Right. Yeah. So those are the rules of the mu system. He then goes on to just explain more broadly like formal systems and he discusses theorems, axioms and rules. Yeah. Where a theorem is any string producible in a system. So we just gave a bunch of examples like MIU, MUI, MII, all those. Axioms are free theorems. So basically when you're like introducing the system, like the Mute system, you sometimes also introduce these like starting theorems, like in the Mute system, the starting theorem is MI. but then the rules are just those things that you just described. It's basically like how you can take existing theorems and produce new theorems. Um, and there's two types of rules. There's rules of production and rules of inference. And I guess, I, rules of production are where you're just adding stuff to theorems, right? Like converting M I to M I I. Um, what's a rule of inference?

Matt: 10:48

I don't think that. the mu system has any rules of inference. a rule of inference may be like a conditional rule where it's like, if you have this, then you have that, I don't think we have any of those rules here.

Jon: 11:02

Okay, yeah, I mean the Mu system is like kind of this dead simple formal system, so it probably lacks a lot of these sophisticated things.

Matt: 11:12

One of the things that I didn't like, it sounds like a theorem, like, I guess in my kind of casual brain, I think of a theorem as something that may or may not be true, but it sounds like in this, like a theorem is true. It's something that has been logically derived from. Something else. So should I treat a theorem as true?

Jon: 11:33

Well, it's interesting because I think we hear the word theorem in math, and we think to ourselves, like, we don't know if that's true or not. Or, you know, there's some theorems that everyone thinks are true, but they haven't been, like, definitively proven to be true. And I take, I took it after reading this as, You know, brilliant mathematicians are sort of using their intuition to produce these theorems that they think will eventually be derivable in some formal system. but they're not sure. You know what I mean? So, so it actually does fall, you know, he says a string producible in a formal system, you know, math itself is a formal system. Um, And theorems in math are strings that can be produced in that formal system. But I think a lot of these theorems that we don't know are true or not, they're almost like guesses, you know, it's like some mathematician is guessing that this is a theorem.

Matt: 12:31

So is this as if you came up with a string I'm like, Hey, John, like, I just discovered M U I, I, I, U I, U I, I, I, U I, like, this is my theorem.

Jon: 12:42

exactly.

Matt: 12:43

That's kind of the essence of my question here. It's not a capitalized essence, but it's just a regular old essence. Uh, but of, of my question is, is that string of M I's M and U's and I's. a theorem? Or does it only become a theorem once I've found it through, like, a systematic search of this, of this space?

Jon: 13:05

yeah. I mean, he does say this is a string producible in a formal system. So by that definition, I would think it would only truly be a theorem once it's proven. To be able to be produced. Um, but I do think that in math, like parlance or whatever, uh, there are many theorems that we like don't know are definitively proven, um, but we think are true. And I wish I had some examples, actually.

Matt: 13:36

Pythagorean theorem, right?

Jon: 13:37

Yeah, yeah, Pythagorean theorem.

Matt: 13:40

he actually says this, actually. A theorem, capital T, is a statement in ordinary language which somebody once proved to be true by some sort of logical argument.

Jon: 13:53

Oh, right, yeah, he

Matt: 13:53

crazy, because I guess I always thought theorem, like, I think of theorem and theory as like, kind of similar, but I guess a theory is also much more rigorous than people use it generally,

Jon: 14:07

Yeah.

Matt: 14:07

you know, in common parlance. But anyway, so a theorem is something that, according to some formal system, we, we kind of know to be true.

Jon: 14:19

Yeah, but aren't there some theorems that were, like, not 100 percent sure are true?

Matt: 14:24

Well, aren't those called, like, Conjectures.

Jon: 14:27

Maybe.

Matt: 14:28

cause what, there's that, like the Goldbach conjecture, right.

Jon: 14:31

Yeah, yeah, yeah. Um, okay, but anyway, so he goes on So the whole Topic of this chapter is this mu formal system and the mu puzzle, which is, can you start with mu, or sorry, can you start with MI and eventually produce MU by using all of those rules that you just mentioned and both of us. You know what? The way this podcast works is we both privately read the chapter and then we just meet. on a day and like discuss the chapter. We don't have any pre planning. It's very kind of shot from the hip, but both of us wrote programs to try to brute force, solve this puzzle.

Matt: 15:14

I spent more time than I would like to admit just going through as many of these as I, I had these completely disorganized arrays of like strings and like arrows and what have you. And I very out space. I went back and I realized that he didn't phrase it in such a way that. Actually tipped his hand as to whether or not it was possible. But he says, can you produce mew?

Jon: 15:40

Mm.

Matt: 15:42

And I think it's not quite as bad as like, how do you produce mew? Cause that would indicate to me that there is

Jon: 15:50

that it's possible. Yeah.

Matt: 15:51

But can you produce mew? I feel like it's kind of a gray area because there's an interpretation where it's like, Oh, like can you get me a glass of water? and then you find out that the glass of water is, at the end of infinity,

Jon: 16:02

So this is why I am infuriated because I wrote this terrible brute force algorithm, which by the way, I have a couple factoids about the M puzzle. Uh, well, I guess just one interesting factoid, I'm not gonna bury the lead. On the 11th iteration of the brute force version of the mu puzzle, there are 28 million different. Theorems that have been produced so based on what I mean by the 11th iteration, because we haven't discussed decision trees yet. But what I mean by the 11th iteration is like you start with M I and from M I you can produce M I you like we said earlier and you can produce M I I. And I think that's it, right? It's just those two. But then from those two you can then produce. M I U I U, right? I'm gonna screw this up. Um, and,

Matt: 17:05

M I I I

Jon: 17:07

oh, right, right, yeah, cause M I I, M I I can become M I I I I.

Matt: 17:13

that's it too, like both, that, there's only one, I think, from each of those. Which is the double, you can always apply the doubling rule.

Jon: 17:21

right. And then there's also M I I U, right? Because M I I ends in an I, so you can add a U to it.

Matt: 17:28

Oh, right, yeah, that's a good call, that's a good call.

Jon: 17:31

So, so you can think of it like a tree. That's why they call them decision trees where the, you know, the, the apex of the tree, like the star on the Christmas tree is MI. And then you have a row of two, MII and MIU. And then you have a row of three on the 11th row of that Christmas tree. You have 28 million nodes, which is why I let this program run for like 15 minutes. And then I just turned it off and decided it was impossible to produce MU.

Matt: 17:57

Right. Yeah, I did a very similar thing, I didn't do, I didn't do it quite as rigorously in terms of defining, layers of a tree. but, I just said, okay, once you generate 100, 000 of these things, like just, you know, just bail. he hasn't tipped his hand But uh, I I am of the opinion that it is not possible to produce mu in this system

Jon: 18:20

Yeah, I agree too. He said he would give the answer, but he has not given the answer yet. So we remain in suspense, and I guess we'll let the listener know later whether this is possible

Matt: 18:32

So what is hofstadter trying to teach us with the mu puzzle Oh Yeah

Jon: 18:42

I mean, I think for one thing, he's just trying to introduce this notion of a formal system. Uh, but I think he's trying to do something more interesting too, which is like, Learning how to move through a formal system by using these rules. Um, and we will probably use the example of programming nonstop because that's what we do. Um, you know, with programming, you're in a formal system. Like you can only write certain combinations of words and characters. And at, throughout your programming career, you get better and better at navigating this formal system and representing these more and more sophisticated things. Um, when you get old, you start getting worse at it. That's kind of where I'm at, but, uh, it's kind of this amazing skill to be able to like, you know, take these rigorous rules and use them to like bend the universe to your will. Um, and that's kind of what mathematicians do. It's what physicists do. And it's sort of what programmers do to a certain extent.

Matt: 19:48

He uses this as an example to draw a distinction between a machine and a human. And it's funny because in your example, you're talking about how for a human, it's an achievement for them to be able to work in the formal system. Yeah.

Jon: 20:09

Yeah.

Matt: 20:09

But he, he almost is more like, well, the, the cooler thing about humans is that they can't not like consider outside of the system. Like they can't not think of, or learn things that aren't explicitly stated in the rules of the system.

Jon: 20:28

Yeah. Yeah. And it's almost, it's almost difficult for a human to like fully be in a formal system. Whereas a computer is like by definition, like stuck in a formal system. And it's only in very super recent history that we have developed a Computational systems that sort of feel like they're not locked in a formal system, even though, even though they really are, when you, when you really, really break it down and now it's becoming this interesting, you know, philosophical debate of like, what even is intelligence?

Matt: 21:01

Yeah. Is it, is it breaking out of the system or not? speaking of which, one really, um, minor point about like LLMs or what have you is what I use. I use co pilot. It's this thing from GitHub that, that like tries to auto complete your code with an LLM. When I started to write this, I, I wrote like mu rules. Boom. It, it, it misremembered them, but it knew exactly what I was doing. So it created like a rough approximation of, of the rules when I went to, to write the program out, which was like wild to me. Uh, so, yeah,

Jon: 21:49

Uh, the chapter where he mentioned that humans have this weird ability to kind of have insights about a system, whereas computers can't have insights about anything, or at least they didn't used to be able to do that back in the 70s when he was writing this book, but he mentions how a human will quickly realize that there is always going to be an M at the front of any theorem.

Matt: 22:12

right.

Jon: 22:13

But a computer, you know, a computer doesn't even have a concept of like realizing that there's an M at the beginning. Um, although I think if you asked GPT today, like if you fed GPT, these rules into chat GPT and was like, draw some insights from these set of rules, it would probably tell you that, you know, there's always going to be an M at the front. So I think there's going to be a lot of material in this book. Uh, where he's, you know, kind of mentioning the limitations of computers and it's just not going to be true anymore at all. And it's kind of a testament to how far we've come.

Matt: 22:53

He talks a little bit about, um, M mode, you mode, I mode, this is like, it's funny because up until this point in the chapter, he's using M I and U as just these blank, like tokens that don't mean anything in themselves. But then he, he has this section where he talks about M mode, I mode and U mode. And then he says, M mode is. The, mechanical mode, where you're just, you're operating kind of like a computer and you're just like mechanistically applying these rules without observing things.

Jon: 23:27

Yeah.

Matt: 23:28

And then there's I mode, which is intelligence mode, which is like, now you're considering like things outside of the system. And then he has the, he teases this third mode, which is, mode, the you mode. And he doesn't tell us what he says. It's the Zen way of approaching things. Uh, but he doesn't, uh, tell us what that, what that means.

Jon: 23:49

And, and I think this is sort of the way of thinking that I don't do. This last, you know, zen mode or whatever. And I'm hoping that this book will sort of describe a mental framework. For intuiting that it's impossible to produce mu, uh, you know, from the mu puzzle, obviously you can intuit that it's super easy to produce MII because you're literally just applying a single rule to the initial axiom, but I think there's probably also this way of intuiting that, like, you can't produce MU. Um, and I don't have that ability. Like I still. You know, I still look at this puzzle and I can't, I can't definitively say whether it's possible or not. I can just write a brute force program and like, you know, believe that it's not possible.

Matt: 24:38

it.

Jon: 24:42

Decent sized section about that, uh, and I, and I thought it was interesting because he sort of kicked the section off describing exiting from a formal system, um, and, and then he sort of went on to describe, like, society itself, you know, he was describing like, oh, we live in this, that, and I can't remember, it's been a decent chunk of time since I read the chapter, but it was almost like he was describing Uh, you know, the, the sort of capitalist system that we live in. And then he went on to say, some people break out of that system. And I don't know, like, it almost sounded like he was describing people who like go live off the grid or something and like write manifestos in a shed somewhere. one section I thought was funny was he, and this was actually part of exiting from a system, but he mentioned this Canadian chess program. Like there was this long era where, uh, you know, they would have chess programs compete against humans and they would have chess programs compete against each other. These days, any crummy chess program can completely annihilate any, even the best chess programs. human, you know, Magnus Carlsen will get beaten a thousand times out of a thousand by even the most basic chess program. Uh, but back in the day, Grandmasters could beat chess programs and he, he discusses this Canadian chess program that I guess would like resign early. Like it would be in these positions that aren't necessarily losing positions and it would just resign like almost midway through a game. Um, and evidently that was You know, uh, an interesting thing in the world of chess, like just this weird program that would exit from the system, be like, ah, I'm done. I thought that was interesting. And then the last thing I have in my notes is just decision trees, which we described a little bit, um, earlier. So maybe we don't have to rehash it, but, um, decision trees are a super powerful thing. Um, it's a thing that I actually learned in AI class. Like I took an AI class in college and there's a very famous problem called missionaries and cannibals, which is where you start with three missionaries and three cannibals, and you're trying to get everyone to the other side of the river. in missionaries and cannibals, you can't ever have the cannibals outnumber the missionaries. Um, and so, you know, you, you basically do this thing where like, okay, I'm going to send two cannibals over, one cannibal back, then I'll send a cannibal and a missionary. Oh, but now the cannibals outnumber the missionaries on this side, so they eat the missionary. Um, but anyway, the way that a problem like that can be solved is through these decision trees where you basically just do every single possible thing in a huge tree. And then once you find a solution node, you kind of backtrack up the tree and that's your path. And a lot of AIs use this chess, AIs famously use this. They have tons of super sophisticated optimizations on this. Um, but at their heart, they're still using this kind of, you know, decision tree type algorithm. So just a very powerful kind of, um, you know, If you're, if you're in software engineering, like, this is a good tool to have in your tool chest.

Matt: 28:09

It's funny because you know in the case of the cannibal and the missionary it's trivially discoverable like whether or not each position is like still valid or not, right um I guess Let's say, you know, I think one problem you run into chess is just the explosion of the space, right? It's just too large of a space to discover. But like Is it the case that? If you could explore the entire space of chess you Would always know which move to make

Jon: 28:41

Yeah, I mean, if it was feasible to generate every possible board within, you know, the known time that the universe will exist, then yeah, I suppose you could just literally generate the entire tree of chests. And just calculate the best possible move at any given moment. But like you're saying, I mean, you brought up a super interesting point, which is like, missionaries and cannibals, it's trivial. It's like, if number of cannibals greater than number of missionaries, bad. But in chess, that's extremely difficult to calculate. And it's called a heuristic function. It's basically the function that you run on each node in a decision tree to tell. You know, if that note is good or bad. Um, but in chess, you know, you have a few signals. Like you have material value, which is like the point value of all of your pieces. You know, a queen is nine, a bishop is three, a knight is three, a rook is five. That type of thing. But material value isn't everything because you will often sacrifice pieces in order to do what's called a combination where you do kind of this sequence of moves. Um, so you'll be down material for several moves because you're doing this like forcing combination. And there's also these like tactics, uh, like pins where, you know, you, basically if you can attack the king through another piece. You're pinning that piece. Like, that piece can't move because then the king would be in check. So that's called a pin. So in your heuristic function, you might give a pin some point value. Um, so anyway, it's just, uh, I think like you were alluding to, it's just, um, It's not just the decision tree that, that can get very sophisticated. It's like that heuristic algorithm itself.

Matt: 30:30

Right, right, um All right, well I think That was all that I had for the mu puzzle. Uh, what uh, what about you did you have anything else?

Jon: 30:42

Yeah, that exhausts my notes, uh, but I will just end by saying, like, I'm pretty into this book. Like, the dialogue was super silly, and I was like, oh my god. But then the chapter started and it was like, okay, you're talking my language, Douglas.

Matt: 30:58

Yeah, this is feeling really like a computer science textbook. Definitely. Um,

Jon: 31:04

Like I am going to get slightly smarter by reading this book, very exciting to me. Thank you.

Matt: 31:10

All right. Well, I will see you for the next chapter, John.

Jon: 31:15

See you next time, Matt.