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 you doing?

Jon: 0:32

Hey, Matt, I'm doing well. How are you doing?

Matt: 0:34

I am doing all right. I'm ready to, ready to just dive in bare chested into this, whirlwind tour of, uh, discrete mathematics and logic.

Jon: 0:45

I feel like this is even more the deep end than this series has already been like this book already feels like every single sentence and paragraph can be analyzed infinitely. And now here we are taking three, three chapters and trying to do some episodes about those three chapters. Like it's going to be tough.

Matt: 1:07

I mean, I'm ready for Douglas Hofstadter to like say, Oh, now read the whole book backwards. And that's actually a whole other thing about some other cool topic.

Jon: 1:17

Yeah, man, that wouldn't surprise me at all. If the whole, if the book itself was like structurally, yeah, yeah. Had some, he met, he had a joke about that. I think it was in the last chapter of the three. Or no, it was in typographical number theory where like basically the whole entire dialogue, wait, is that, is that what the things are called?

Matt: 1:39

Yeah. I think they call them dialogues. Yeah.

Jon: 1:41

Like the whole entire dialogue was like palindromic conceptually and also literally like a lot of the sentences were the same and he made a joke. Like, I couldn't believe it when I noticed that I had written this palindrome. It's like obvious that he spent hours and hours like piecing this thing together. So I thought that was funny.

Matt: 1:59

I feel like I picked up pretty early on. There was like one, this weird, like transition between the two. And it's like, okay, there's something stilted. And it's like, you just start to read the last few sentences the other way. And it's like, okay, like it's one of those like backwards and forwards,

Jon: 2:13

Yeah. Yeah.

Matt: 2:14

but so this episode where we're doing things slightly differently or we're like, what we realized is I think there's a ton in this book. And if we do everything at the finest level of detail, we will be spending kind of an infinite amount of time doing it. So, um, so we're going to cover what's that?

Jon: 2:34

I also, I like, I think it's almost better for us to cover this. At a higher level too, because for one thing, like, if you're interested in this material, you should read this book. Like, I think this book is very, it, it, I don't know. It's kind of an amazing

Matt: 2:54

a book is almost not correct. It's cause it's like, there's exercises in there. It's, it's, it's kind of a cross between like a novel and a textbook basically.

Jon: 3:07

It is. And it's also so unique in its, or at least from, from books I've read, it's so unique in that it is like. I want to say meta, like, or maybe interdisciplinary is a better word where, yeah, a lot of the book is talking about like logic and math and, you know, this chapter is called propositional calculus, I think, but it's also talks about music and talks about just thinking and there was a whole chapter about Zen and how that sort of. It ties in with, uh, you know, Gödel's Incompleteness. And it's, it's just kind of this book that's like simultaneously insane, but also like highly dense with knowledge and, these amazing sort of logical nuggets. Uh, so it's, I don't know, it's a very cool read. It's very different from most reading experiences, I would say.

Matt: 3:57

Oh yeah, oh yeah. but so these, yeah, so these chapters are, we're going over chapters 7 and 8, and this is the Propositional Calculus and Typographical Number Theory. And, it's funny because like, to your point, it feels like up until this point, while we were reading them, it felt like super dense, and like super tough.

Jon: 4:18

Yeah.

Matt: 4:18

And we get to these chapters and it's like, Oh, okay. Those were all toys. Those were all little, uh, you know, play school, uh, things so that we can, like, our brains were primed for like the actual knowledge that he's trying to dispense,

Jon: 4:35

shifted into Overdrive. It's, it's like he's described how formal systems work, and now he's telling us like, this is the formal system that represents human knowledge, which is this kind of crazy leap. Um, and then you start to see the power of why, um, Who are the two guys who wrote the Principia Mathematica? Yeah, like, why Russell and Whitehead and so many mathematicians of that era were so obsessed with this concept? Because it's, it's so incredibly powerful to be able to represent knowledge with, you know, symbols and formulas, and then be able to, like, basically generate new knowledge by applying existing rules to those, theorems, basically. Right.

Matt: 5:23

He does here. What Hofstadter does here is he, and with these two chapters, I kind of, by the end of the second chapter, we wind up with a system that is equivalently expressive. My is my understanding to the system that, uh, Principia laid out.

Jon: 5:41

Yeah. And he does a few exercises with the system. One of which was kind of funny where he's trying to figure out whether this guy Ganto will chop off these monks heads.

Matt: 5:53

I hated this so much, dude, I'm just going to come out and say, I hated this so much.

Jon: 5:58

That's fair. Yeah, no, it was kind of idiotic, but it was also kind of awesome because he basically used this logical system to deduce that Ganto was like about to chop these monks heads off. And I just found it amusing.

Matt: 6:11

Well, let's, uh, I should have the, I should have the, uh, the thing up here. Uh, let me see if we can, if I can read this out. So, uh, This is a, this is a Zen koan, which we're going to get into a lot more detail in the next episode, but, um, so it says, one day Toku san told his student Ganto, I have two monks who have been here for many years. Go and examine them. Ganto picked up an axe and went to the hut where the two monks were meditating. He raised the axe saying, if you say a word, I will cut off your heads. And if you do not say a word, I will also cut off your heads. Okay. And so, so of course, uh, Hofstadter breaks that down into a series of, uh, logical statements. And this is this, and he he's expressing it in this, um, kind of proto system before we get to his typographical number, uh, theory, is it? and, uh, and so like, obviously, you know, the, Our, our, uh, what is it? Like intelligent mode mind is saying like, okay, well, it doesn't matter whether or not they speak. The, the, the reality is like, he's going to cut off their heads. Um, but so like the conclusion is both monks continued their meditation as if he had not spoken. Ganto dropped the ax and said, you are true Zen students. He returned to Tokusan and related the incident. I see your side. Well, whatever, blah, blah, blah. So anyway, he does not cut off their heads. It's like.

Jon: 7:43

Yeah. It's like you had to cut off their heads based on propositional calculus,

Matt: 7:49

Yeah, it's like, aren't you being like, you're supposed to be completely consistent, but I mean, I, I guess not, um,

Jon: 7:58

But yeah, my take on propositional calculus was it was sort of this introduction of logical sentences from scratch that basically contain truth. Uh, and typographical number theory was almost like a full, rigorous definition of a system that uses numbers. Um, and I guess the, or, well, I guess it's still use symbols, but it was like, you could do math on, on these like, Number, well, do math on these symbols. Yeah, exactly. Which are called theorems, I guess.

Matt: 8:35

Yeah. Or do they, there was another word they use, which was, I think formulas, um, which they're, they're equivalent though. Um,

Jon: 8:44

And he, he introduced a couple new symbols for the typographical number theory to represent things like for all, like you could say something like for all x, x plus zero equals x. Which trivially true thing. But he just introduced these new symbols so that you could represent that statement very tersely.

Matt: 9:05

It's, it's interesting, um, yeah, so in, in the first chapter, he kind of just lays out like, and not, or, um, and then also like implies relationship. So you can basically, you know, he sets up the framework where it says like, okay, can make an expression, like if X is true, then Y is true. And that's kind of like the core of the, um, you know, of the propositional calculus. He also. Provides a way to like prove one of those statements, like assume X, like, and then I'm going to show you that this other thing is true. And then you, that he allows you to kind of like, Come back from that hypothetical world. And this goes back to the pushing and popping.

Jon: 9:52

Yes. Yeah. I had

Matt: 9:54

were basically, yeah, go for it.

Jon: 9:55

I was just going to say, I had not, uh, seen that. I thought that was very interesting. Like I want to say he called it maybe the, uh, or the fantasy rule and the, and the carry over rule where basically you, you'd start with a logical premise, And then just like you're saying, you'd sort of push into like a nested set of, of statements, but within those nested set of statements, you could carry over any of the logical premises from like the outside, you know, the outside world. Uh, and in this way you can sort of like, uh, you know, do a little bit of logical deduction based on something you've already proven and then pop back out and like use that final logical deduction. You know, within the outside world as well. So it was kind of this way that you can like get deeper and deeper into knowledge, but then apply that knowledge.

Matt: 10:47

Yeah, it's funny. Cause as you're reading this so much, like it's funny, cause there's kind of a chicken and egg question. Like which came first did was, is he, deriving inspiration from computer science or is it vice versa? Is computer science kind of like, cause so much of this feels familiar, like it's, it's just a function. You're like, you have a thing in there. You have a, you know, in this outer scope. You can reference it and then you can kind of return something back from it. Um, and so Yeah, it's and I just don't know because this book was written like in 1979 or something. So like Before most of the modern programming language were which languages were already written. So,

Jon: 11:35

Yeah. Yeah. Um, it also introduces this other concept that I don't know if he like explicitly stated this anywhere, but I feel like the, the mental leap made sense to me because of so many of the other things he's talked about. Like for instance, he talked briefly about chess. And how you can, or maybe, maybe he just talked about like game systems, but basically in chess, you can take an existing chess position and you can determine all the legal moves and just sort of apply all of those legal moves to get any of the next chess positions. Similarly to how you can take some piece of knowledge with propositional calculus and apply any of the known rules. and get like a new piece of knowledge that may or may not be some like novel piece of knowledge that's, you know, completely unknown. Um, and it's, it's very reminiscent of Euclid's elements, which was also touched on in this book where Euclid sort of started with these, I think it was five postulates and then like built the entirety of geometry using only those five postulates and basically pushing deeper and deeper into like a logical deductive reasoning. And it's just, I don't know, like it struck me as this amazing idea that if you have a formal system and a set of rules for working with statements in that system, you can almost like generate new knowledge by just applying these rules to existing statements.

Matt: 13:11

but And and we're gonna touch on this a little bit in the next episode but Isn't that still true with the system that we already have? Like we, you know, this whole book is really a way to, to understand Godel's theory of incompleteness. And like, I don't know if that was really clear to me at the outset. I know he talked a lot about that. Um, but the whole, the singular purpose is really that the reader understands Godel's theory of incompleteness. So, um, but. It's unclear to me, like, can't you still do that same thing with the current system and like, find new, like, the only thing that girdle theory of incompleteness says is that there are some statements that are true that aren't theorems in the system,

Jon: 14:04

right.

Matt: 14:04

but aren't there, aren't there still, like, given the fact, given that we can express a bunch of these, like, useful mathematical constructs, like, Can't we still do that search and find a useful, uh, mathematical things?

Jon: 14:19

Well, and that's what I am finding funny about this book is. This, this book is almost, uh, like each chapter has like a basic formula where like he introduces some, you know, premise, like it might be a logical framework and then at, towards the end of the chapter, he'll sort of talk about how the premise breaks down, you know, sort of these, these cracks in the armor of like logic and reasoning. But when I'm reading about these logic and reasoning tools, I'm just sort of seeing how useful they are. And, and I think that maybe this is because I am a programmer where, you know, in programming, there's just so much like, it's hard to explain, but in programming, there's just so much jank. Like if you're working in like a large software system, you're so used to seeing these like nice little nuggets of code that are kind of perfect and functional and like, they feel like they perfectly capture the model of a problem. You know, and it's sort of this really elegant thing, but then there's also these other parts of the code that are just like duct tape together, garbage and, and you're just sort of used to these systems that have both perfection and jank simultaneously.

Matt: 15:32

yeah, it's like all of computing is these like beautiful pieces of code that have been like just completely Jerry rigged and duct tape, duct tape together, uh, to actually like get something real done because like, just with that beautiful, like isolated thing, like you can't actually do anything that useful.

Jon: 15:52

Yeah, dude. And I'm so glad I feel like those words you use are so perfect because it's almost like making something useful. By definition is like an interruption of perfection. You know, it's like, it's

Matt: 16:06

Talk to Haskell programmers.

Jon: 16:09

right, right. Well, and that's another thing in programming that I always find amusing is every programmer feels like there's this ideal way of doing something. And, you know, when you sit down to like work on a problem, like that's what you're trying to achieve is this ideal thing. But, but there's always a threshold where you break it, you know? And for some programmers, like I'm a pretty mediocre programmer. So my threshold is like, you know, pretty soon into my work day, I start breaking down and doing things that are suboptimal, I think some programmers can get much further in their work day where everything is utterly elegant, but there's even a point where they break down and yeah, it's just, it's kind of like what you're saying. It's like, if you want to do something useful, like something's going to be janky.

Matt: 16:56

It's all, it's all a spectrum. Yeah. And like, yeah, I've, I've worked with programmers who. They, yeah, they really feel. And, and I'm, I'm more on this side, I would say like they really need to fully consume the universe before they start working on their apple pie. You know, like they just, um, I'm kind of mixing metaphors here, but like the, like, Like. Before they can take a step, they need to really understand like the full system. And I don't know. I'm like, I can get like that sometimes, but I fight, I fight that. I fight that urge or try to at least.

Jon: 17:37

Well, and this is one of the things I love about working with you is I think we do occupy two, you know, fairly different spots on that spectrum, but we're both, I think both of us are still far into the zone of like practicality. Like we're both, we're both pragmatic at heart, um, and, and which I think is also important because I think you can also reach a point where you're just no longer being practical like you're. You're chasing perfection to the extent that it's not productive.

Matt: 18:05

Right. Right. Exactly. Um, just like Russell and Whitehead with their, uh, with their Principia Mathematica and Gertl had to come along and say that, stop it. no perfection. One thing, one thing I did want to talk about is actually induction, just because like, it's a personal, like, I think is, is really cool. So they, they raised this issue where the system is able to, you can kind of infinitely generate all of these roles from the, like from the rules. Like you can generate any like zero plus some number equals that number. Like you can generate that all day long. And then as an intelligent person, you can look at that and you can be like, Oh, okay, well it can generate any number. But then. He, uh, you know, Hofstadter kind of raises a red flag and says, well, it's important to note that like, that's, you're kind of stepping outside of the system. You're just using your intelligent mind to do that. And, uh, but what you really want is something where the, the string itself. And we, you know, you talked about this, these quantifiers, there's this universal quantifier, which says like for every number, you know, X. This thing is true and the system can't do that, uh, as it currently stands, even though you could generate all of them. Um, and we actually need this, uh, special trick of induction. So if you've never taken like a logic class, the way that it works is if you can prove it for the base case, which is like zero and all of these things, and you can prove for like a hypothetical X. And X plus one.

Jon: 19:59

right,

Matt: 20:00

Um, then, you know, it to be true for the, for all numbers, because like, and you think of it like, like a ladder, like that's always the metaphor where it's like, all you need to know, it prove is that like, you can take one rung and the bottom rung is there. And then, uh, and then, you know, it's true for all numbers.

Jon: 20:23

right. Yeah.

Matt: 20:24

which. I don't know. It's just, it's just a very powerful tool.

Jon: 20:30

Very cool. Um, but yeah, maybe we take a break at this point. Cause I feel like we've sort of set the stage. and next we'll talk about how formal systems can be mapped back to typographical number theory, which is a very powerful concept. Uh, and we'll also talk about Zen.

Matt: 20:48

talk about Zen. Yeah. Take a little Zen, uh, a moment of Zen in this, uh, in this book. So, all right, well, I will see you there next time.

Jon: 20:57

See you next time, Matt.