2 - Church's Thesis (Not that one)

## Church's Thesis (Not that one) ### Or: Church's Exodus from Standard Foundations ### Or: Constructive Criticism ### Or: Church vs Choice ### Or: The C in ZFC ### Or: ZFC w/o the C ### Or: Church's two cents ### Or: Ȼurȼ's 2Ȼ ### Or: AC on AC 0: This part isn't about the Church's Thesis you may have heard of. This is about the other Church's Thesis. 1: I don't know about anything called "Church's Thesis." 0: Ok so there's something else called Church's Thesis that we'll get to later. For now, we're not talking about that. We're talking about his PhD Thesis. This is the other Church's Thesis. 1: Why does everything related to Alonzo Church have multiple names for the same thing? 0: You mean multiple things for the same name? 1: Yeah that. What's with that? 0: It's just how Alonzo Churches work. 1: Seems to be. 0: So Church's other thesis (his PhD Thesis) was on the Axiom of choice. 1: What's that? 0: It's the C in ZFC. It's part of standard foundations. The machine code of mathematics. The Axiom of Choice is a sort of "constructor" for sentences that look like $\exists x P(x)$ that doesn't require you to provide an example of an $x$ that makes it true. 1: I know what a constructor is. What's the $\exists$ thing? 0: That means "There exists." Think of the Axiom of Choice as a function that you can call in standard mathematics. That function returns a sentence that says "Something exists." And you're allowed to take that sentence that says "Something exists" and use that sentence in your proofs. It's controversial because you can call that function without passing in an example of an actual Something that makes the sentence true. 1: I'm like 50% following. Rephrase? 0: It lets you prove that something exists without requiring you to give any examples. 1: WHAT?! 0: Yep. Sketchy right? 1: Well I'm not entirely following the mathematics but that definitely sounds sketchy. 0: Yep, that's what Church did his Thesis on. 1: Which Church's Thesis. 0: The PhD one. He was criticizing the Axiom of choice. 1: Seems like a good idea for a thesis. 0: So Church writes his PhD thesis being like "Maybe we can delete this code guys, it's kinda sketchy." ![[church-04.png]] 1: Why are we talking about the Axiom of choice? 0: Well remember, by this time, it's been about 50 years since Cantor, and almost 30 years since 1900 when Hilbert announced his list of problems. So there's been a reasonable amount of work on the foundations of mathematics since then. ![[church-38.png]] 1: What was going on during the 30 years before Church's thesis (the PhD one)? 0: Well there had been some work on axiomatic set theory. Mostly on this system I mentioned up above called ZFC, or Zermelo Fraenkel (with the Axiom of) Choice. That system is still considered the "official" foundations of mathematics by mathematicians today. 1: So what's the problem? --- ## Standard Foundations ### Or: Can Mathematics be Formalized (Friedman, 1997) ### Or: Does mathematics need new axioms (Feferman, 2000) ### Or: Less painful than hell (Hirst, 2000, slightly misquoted) ### Or: These Hell Torments ### Or: The official doctrine of mathematics ### Or: Very few people seem to have a problem with that ### Or: The ~~Current~~ Old Foundations ### Or: Numbers are sets ### Or: Booleans are sets ### Or: Functions are sets ### Or: ZFC > _These axioms are the official doctrine - Remarkably, this is not just the official doctrine for set theory, it turns out that this is the official doctrine for mathematics! - Very few people seem to have a problem with that which I find quite remarkable._ > -NJ Wildberger 0: Well ZFC has never really been _used_ as foundations in any real sense. 1: What do you mean "used as foundations." 0: I mean nobody uses it. 1: What?! 0: Or almost nobody. They usually just talk about it or assert that ZFC proves such-and-such. It's extremely rare to see mathematicians actually working _within_ ZFC as a formal system. 1: That doesn't seem so bad. I mean we programmers don't really write in machine code, like ever. But it's sort of the "foundations" of any language that compiles to it, in a sense. 0: No no, I mean even books about ZFC don't work within ZFC. 1: WHAT?! 1: Why would books on ZFC not work within ZFC? 0: Mathematicians don't like to. 1: Even the ones who choose to write books about it? 0: Especially those ones. Here look. This is from a book published in the year 2000 by an extremely accomplished logician. Brilliant guy named Jeff Hirst. Someone who chose to go into foundations and did some damn good work there. So you might expect he'd be working inside the formal system. Here's what actually happens. Now this is one of the best presentations of ZFC in my opinion, but it's also an example of how ZFC isn't exactly "used as foundations." Come read it with me. ![[zfc-hirst-01.jpg]] 1: "These hell torments"? 0: Yeah that's axiomatic set theory. 1: What's this book about? 0: Axiomatic set theory. 1: What?! 0: That's the point. No one within mathematics really "likes" ZFC. Not foundational people like Hirst who chose foundations as their favorite area. Not even set theorists like Thomas Jech who chose set theory specifically as their favorite area. Now to be fair, the Hirst book here isn't entirely about ZFC. But a third of it is devoted to set theory and "standard foundations." Hirst isn't acting unusual here. Like I said, this book is one of the best presentations of this stuff at an undergrad level in my opinon. This is just sort of how ZFC is viewed and how it's used. The "paradise" in that quote is pretty clearly "the paradise Cantor created," the one David Hilbert is always quoted as talking about: informal set theory, the kind that uses standard mathematical reasoning and eventually leads to paradoxes. In contrast to that paradise are "these Hell torments," which is naturally, well, axiomatic set theory. 1: And this is a book _about axiomatic set theory?_ 0: Yep. At least this part is. This book is extremely good at choosing quotes for section headings. A lot of the quotes in this section are about hell. Or L, which is a thing Gödel invented in the course of studying, well, axiomatic set theory. ![[zfc-hirst-07.jpg]] 1: Damn, seems like mathematicians really don't like axiomatic set theory. 0: Yeah, there are a bunch of funny dog whistles throughout this part of the book about how mathematics probably needs some new foundations. Can't disagree. ![[zfc-hirst-10.jpg]] 1: Why not just come up with new foundations? 0: People have. This guy Harvey Friedman, the one Hirst is quoting in the image below, he kicked off a revolution that completely changed our understanding of what mathematics is at the most fundamental level. ![[zfc-hirst-13.jpg]] 1: What kind of revolution? 0: It turns out most of mathematics is equivalent to one of five sentences. 1: Most of mathematics is WHAT?! 0: Equivalent to one of five sentences. 1: HOLY F--- 0: Yeah I know. 1: What did mathematicians do when they heard this? 0: Nothing. 1: What?! 0: Mostly nobody noticed. At least not many mathematicians. 1: How did most mathematicians not notice that most of their field is one of five sentences? 0: Mathematicians mostly don't pay a lot of attention to Foundations. 1: Good lord. What are the five sentences? 0: Not now. We'll get there eventually. We're still at Church. 1: I thought this was Hirst. 0: Everything's connected. Ok so Hirst's doctoral advisor, one of his two advisors, was Friedman. 1: Same Friedman? 0: Same one. Here's Friedman in 1997. ![[friedman-1997-the-formalization-of-mathematics-01.png|350]] 0: Here's the first line of that paper: ![[friedman-1997-the-formalization-of-mathematics-02.png|300]] 1: I thought they formalized mathematics with ZFC. 0: Well, that's the standard story. 1: When did ZFC come out again? 0: Before Church. Remember how ZFC was what Church wrote his PhD thesis on? 1: Oh right. 0: But you're right to be confused. See in principle we supposedly "formalized mathematics" back before 1927 when Church finished his PhD thesis. But in practice, here's Harvey Friedman in 1997. ![[friedman-1997-the-formalization-of-mathematics-03.png]] 1: Is he gonna say "Everyone's wrong"? 0: No, he's gonna say they're basically correct. 1: What?! ![[friedman-1997-the-formalization-of-mathematics-04.png]] 1: What's the point here? 0: ZFC isn't _wrong._ And it's not technically _not foundations._ But it's almost certainly _the wrong foundations._ 1: No idea what you mean by that. 0: Let's keep reading. ![[friedman-1997-the-formalization-of-mathematics-05.png]] 1: Grossly inconvenient? 0: He's acknowledging the same thing Hirst acknowledged. Nobody _likes_ using ZFC, and basically nobody does, if by "using" it we mean "working inside it to do mathematics," or even "working inside it to do foundations," or even (most surprisingly) "working inside it to do set theory." Grossly inconvenient is an understatement. 1: Ok so what's Friedman's suggesting? 0: Let's see. ![[friedman-1997-the-formalization-of-mathematics-06.png]] 1: "Obtain detailed information about the logical structure of mathematical concepts"? 0: What's the question? 1: MATHEMATICIANS DON'T ALREADY HAVE THAT INFORMATION?! 0: Well in a lot of ways they do. Friedman's talking about something much more precise. Remember, he's the guy who kicked off the research program that eventually showed that most of mathematics is equivalent to one of five sentences. By "logical structure" here I assume he means something much more like a generalization or extension of Reverse Mathematics. 1: What's Reverse Mathematics? 0: The research program that eventually showed that most of mathematics is equivalent to one of five sentences. 1: Damn. Can we read some reverse mathematics eventually? 0: It can be pretty technical, but absolutely, we'll get there. Not in this era, but a couple eras down the road. 1: What's this era? 0: The 1930s. 1: We're in the 1930s? 0: Well remember we're still at Church. 1: I thought this was Friedman in 1997. 0: It is. But we're still at Church. I'm just explaining that Church was dissatisfied with the standard foundations in his day for a reason, and those reasons haven't gone away in 100+ years since then. But right now, the era we're in is the one that started with Cantor's Paradise and Russell's Paradox and Hilbert's program and which led to three characters in the 1930s giving three different definitions of computation that turned out to be equivalent. We might call this era, say, "Testament (-1)". So we won't be covering Reverse Mathematics yet. But some time in Testament 0, when we get to Ken and Unix and C, and computing changes forever, a few years after that, Harvey Friedman shows up and changes mathematics forever. 1: I thought you said mostly nobody noticed Friedman's stuff. 0: The mathematicians didn't. At least not as much as they should have. But the foundational people noticed. And eventually we'll see that the mathematicians start to get converted by the foundational people, but we won't get there until some time around 20XY. 1: 20XY? That's now! 0: Exactly. It'll take a while to get there. Let's not jump ahead. For now, we're still at Church. So as Harvey was saying back in 1997... ![[friedman-1997-the-formalization-of-mathematics-07.png]] 1: I feel like programmers think about the notation thing more than mathematicians do. 0: Of course! We have to implement everything we do. And our codebases actually have to compile and execute. Notation is way more important when you can't skip steps. 1: For real. ![[friedman-1997-the-formalization-of-mathematics-08.png]] 1: _Mathematicians don't even have a database of mathematical information yet?_ 0: Well in a sense they do. There's the academic literature. 1: _(Eyes wide in disbelief.)_ So, papers? 0: Well y'know, PDFs. But yeah. 1: That's not exactly a database. 0: Well there's also the arXiv. 1: What's that? 0: Sort of a "github for PDFs", minus the git part. 1: What? 0: It's a place where mathematicians and other academics can publish papers to get their peers to review them, which normally isn't possible for months or years with the normal academic publishing system. 1: What's the normal academic publishing system? 0: They call it "peer review." 1: _(Squinting)_ There's an entire system that exists "so your peers can review things" because "having your peers review things" isn't possible with "peer review"? 0: It's still possible. Just not for months or years. 1: What happens during "peer review"? 0: That's the part where your peers can't review things. 1: _(Turning red)_ My head hurts. 0: Good. Don't think about it too hard. Academia is basically dead. But it wasn't dead at all back in the 1930s where we currently are. And it wasn't entirely dead in 1997 when Friedman's writing this. So back to Church. Here's Friedman in 1997: ![[friedman-1997-the-formalization-of-mathematics-09.png]] 1: What does he mean "The more ambitious concept of formalization includes proofs"? 0: Right, so if you look back through the conversation to where Friedman said "the formalization of mathematics is extraordinarily inconvenient in any of the current formalisms," back then he said (in slightly different words) that there are two things we want in a formalization of mathematics: 1. At minimum, a formalization of mathematics where we can just write down our definitions and the statements of theorems, and not even try to do proofs. 2. More ambitious, a formalization of mathematics where we can actually do proofs. "These are even more inconvenient in present formalisms"? 1: _(Horrified)_ Hold on hold on hold. Let me get this straight. It's been a century since ZFC. 0: More than a century. 1: And this guy is saying that ZFC can't even write down the basic definitions and theorems of mathematics? 0: Well it _could_ in princ--- 1: But nobody has. 0: Basically. 1: So nobody does that. The basic stuff. Definitions. Theorems. Like if mathematics was a C program, they're not even writing the header files in ZFC. 0: Good analogy! And yes. 1: Yes? 0: Yes as in no. They don't do that. 1: And then actually proving stuff in this system is a whole different story. As in, if header files are too hard to implement, then C files are out of the question because doing the actual implementation would be much harder. 0: Good analogy again! 1: So yes? 0: Yeah that's basically the situation. 1: _(Staring at the ground)_ Look I know you say things like "Everybody's wrong about everything," and I know usually that's just you exaggerating. 0: I never exaggera--- 1: Yes you do. 0: Ok yes I exaggerate all the ti--- 1: How did this happen? 0: I dunno, I guess it's just how I tal--- 1: No I mean mathematics. 0: What about it? 1: _(Gazing into the abyss)_ I mean I don't know that much mathematics. I'm a programmer. But I always had this feeling that mathematics knew what it was doing. 0: It usually works pretty ok--- 1: That they had their shit together over there better than we do. I mean they're supposed to be the foundations of all knowledge. 0: Mathematicians don't really think much about foundat--- 1: Or at least the foundations of the hard sciences. 0: Again, foundations isn't really their thin--- 1: And I don't think I'm the only One who's felt a bit inadequate in the past when I approached some piece of math and couldn't understand what was going on. 0: That's not your fault. It also doesn't mean the math is wrong. Most of mathematics is perfectly fine. 1: Fine how? 0: Fine as in it's probably right. 1: _Probably?_ 0: I mean yeah. 1: How is _probably_ good enough? 0: I mean that issue runs deeper than just math. It hits foundations too. Remember Church's first version of lambda calculus turned out to be inconsistent. Haskell Curry's combinatory logic turned out to be inconsistent too. So did Frege's system where Russell learned logic and found his paradox. And don't get me started on the Kunen inconsistency, the large cardinals people are basically a relig--- 1: So that many logics turned out to have contradictions. 0: Yep. 1: And basically _none_ of modern mathematics is written down in ZFC. 0: Correct. 1: In the system that claims to be its foundations. 0: Accurate. 1: Or in any other formal language. 0: Basically. Though that's been changing recen--- 1: I think I need to sit down. 0: You are sitting down. 1: Ok I'll just shut up and listen and see if this existential crisis goes away. 0: It's ok! Don't try to make it go away. This existential crisis is something every one has to go through if you eventually want to understand our field. 1: Which field? 0: Computing. 1: I though we were the foundational people. 0: Well, maybe the reason I called us that is so you'd eventually start to see the the point of all this. 1: Point of what? 0: That your field -- our field -- computing I mean. We may come to be responsible for things we hadn't expected to be put in charge of. 1: Such as? 0: We'll get there. Before we get to the new foundations, we've got to cover the old ones. Ready to get back to Church and the 1930s? 1: Yeah, let's get back to that. 0: Ok, starting from what Friedman was saying in 1997, let's rewind the clock... ![[friedman-1997-the-formalization-of-mathematics-10.png]] 0: Logic and mathematics have remained largely separate, with mathematics remaining almost entirely unformalized and without any practically useful foundations. ![[friedman-1997-the-formalization-of-mathematics-11.png]] 0: I would be nice if mathematics was stored in something other than PDFs. 1: Ya think? 0: I know it seems obvious to us, but outside of developers not everyone thinks that way. But Friedman's basically saying here that it would be nice if mathematics was stored in a format that's both human readable and machine readable. ![[friedman-1997-the-formalization-of-mathematics-12.png]] 0: Then he goes into standard formal set theory. 1: Wait let me stop you there. Can we actually see this "formal set theory"? We've been talking about it for a while but I don't think I've actually seen the language or its axioms, except for a few lines in that Hirst book up above. 0: Perfect timing. As I was saying, that's what Friedman's getting to right now. ![[friedman-1997-the-formalization-of-mathematics-13.png]] 1: What does this mean? 0: The formal language of ZFC has these symbols: - $\lnot$ : The "NOT" symbol. If $A$ is a sentence, then $\lnot A$ means "not A" or "the negation of A." 1: Can you be more formal and not use words like "sentence"? 0: Sentence is a formal term in logic! But good question. Here's the definition. ![[meaning-of-sentence-in-logic.png]] 1: Hah it says "For a less technical introduction, see Statement." 0: Why is that funny? 1: I dunno, I feel like "Statement" sounds more technical than "Sentence." 0: Fair. Either way, "sentence" is a standard term in logic, and if $A$ is a sentence, then $\lnot A$ means "not A" or "the negation of A." 1: So if is true, then $\lnot A$ is false? 0: Yep. Ok next one: - $\rightarrow$ : The "IF THEN" symbol. If $A$ and $B$ are sentences, then $A \rightarrow B$ means "A implies B" or "if $A$ then $Bquot;. Now in natural language, "if then" is used in lots of ways. In standard logic it's only used in one specific way, which is that $A \rightarrow B$ can only be false in the specific case when $A$ is true and $B$ is false. In all other situations we say $A \rightarrow B$ is true. 1: So if $A$ and $B$ are both false then $A \rightarrow B$ is true? 0: Yep. Feels a bit weird at first but it doesn't cause too many problems. Plus, the other ways of defining the conditional are a bit of a rabbit hole, and they're not relevant for us here. If you're curious, look up "Material conditional" and poke around for any mention of alternative definitions. For now, that's implication. 1: Got it. What's next? 0: - $\land$ : The "AND" symbol. You can guess when $A \land B$ is true and when it's not. There's no philosophical subtlety to and. 1: Thank god. 0: - $\lor$ : The "OR" symbol. $A \lor B$ is only false when both $A$ and $B$ are false. In all other cases, whether one or the other or both are true, then $A \lor B$ is true. 1: Ok I know I asked for this, but I'm starting to realize I already know this stuff. 0: Do you? 1: Boolean logic? I'd sure hope so. I'm a professional devel--- 0: So no philosophical subtlety to "OR" either? 1: Zero c'mon, let's keep moving. 0: I was about to keep moving, but since you're sure you understand OR--- 1: _I UNDERSTAND OR!_ ## Constructive Criticism ### Or: OR 0: Exactly. But it turns out there are some questions I have, questions that are related to Church's thesis (the PhD one) and also to the axiom of choice. But my questions are more basic than that. Just some simple questions about "or." So since you're sure you understand "or," then maybe you can teach me some things about which I'm not sure. 1: Is this a game? 0: No, I'm serious. 1: I don't believe you. 0: Ok so, for any sentence $A$, is the following always true? $A \lor \lnot A$ 1: Is this a trick? 0: Not a trick. 1: And these are booleans? 0: Let's call them "propositions." 1: Is that a fancy word for boolean? 0: Sort of. A proposition is a bit more like a pre-boolean. 1: Wtf is a "pre-boolean"? 0: I mean $A$ is a sentence that can either be true or false, and it can't be half-true and half-false. 1: How is that not a boolean? 0: Well, suppose we don't know its value. 1: So we know $A$ is of type $Bool$, but we don't know its value? 0: Basically. 1: Zero that's a boolean, don't be stupid. 0: I'm trying as hard as I can not to be stupid, but I'm still not convinced it's a boolean. 1: You said this wasn't a game. 0: It's not! 1: Then what's your hang-up? 0: Well look, we're programmers, and if we were programming in a typical language, I'd have zero hang-ups and no worries. 1: So how is this different? 0: This is mathematics. 1: Fair. I mean I'm as convinced as ever that mathematics is a bit wacky. But how is OR tripping you up exactly? 0: Not OR per se. Just this: $A \lor \lnot A$ 1: So you're fine with that sentence in programming? 0: Of course. 1: How is that sentence any different in math? 0: Well, I have a strange feeling that it requires... how can I put this... omniscience. 1: Omniscience?! 0: Omniscience. And I'm not god, so I'm not sure I can handle it. 1: Is this just an excuse to bring up bible stuff again? 0: Not at all. 1: Then explain why you're being weird. 0: Suppose I hand you a sequence $a_n$ of natural numbers. For simplicity, let's say they're all $0$ and $1$. 1: Define your terms so I know this isn't a trick. 0: I just mean a function from $\mathbb{N}$ to $\{0, 1\}$. 1: I get the idea but I need more details because I'm assuming this is a trick. 0: Ok, good point. Math terminology is nowhere near precise enough to explain what information you actually have and don't have. Let's be precise. Imagine it's a python generator. 1: Ok. 0: And further, imagine I don't give you the source code to the generator. 1: What do I get? 0: All I give you is the ability to call `next()` on the generator. 1: Ok, how's this related to the thing where you're pretending not to understand "OR"? 0: Well, I've been thinking about what happens when $A$ is a sentence like this: > $A$ = The python generator I just handed you always yields $0$, and will never yield $1$, no matter how many times you call `next()`. or equivalently > $A$ = The sequence $a_n$ is always zero. or equivalently $A \; \equiv \; \forall n \in \mathbb{N}, \; a_n = 0$ 1: What's your problem with that sentence? 0: Nothing. My problem is with this sentence: $A \lor \lnot A$ 1: You have a problem with the sentence "A or not A"? 0: Not for all sentences. Just for sentences like that one. 1: I'm still not following. 0: Ok, suppose you think $A$ is false, and I think it's true. How would you convince me you're right? 1: $A$ being false means what again? 0: $A$ being false means that eventually the generator will spit out a $1$. 1: Well obviously in that case I'd just keep calling `next()` until I got a $1$. Then I'd show you the $1$ and that would prove I was right. 0: Good point. What about the other case? Like what if our beliefs were swapped, but you were still right? 1: You mean what if I think $A$ is true, and you think $A$ is false? 0: Right. 1: And $A$ is actually true, so I'm right? 0: Right. How would you convince me then? 1: _(Looking back over the definitions.)_ Ok so if $A$ is true then the sequence is always zero. Or the generator keeps yielding zero whenever I call `next()`. 0: But I don't believe that. 1: Right. And I do. 0: I need to be convinced. 1: And I don't. But I'm right. 0: Right. 1: So what's the question? 0: How would you convince me? 1: I don't know. 0: Well I've given you an awful lot to work with. 1: Have you? 0: Absolutely? I've been more than generous here. We've assumed that you're _actually_ correct and I'm incorrect. We've assumed that $A$ will always return $0$ no matter how many times we call `next()` to see what the next number in the sequence is. And we've assumed you believe that. And we've assumed I don't believe that. I'm just some ignoramus who has trouble with "OR", at least in this particular manifestation. Surely that's more than enough for a proof that I'm wrong. 1: I'm having trouble, can you give me a hint? 0: No. 1: Zerooo. 0: I'm not in a position to offer hints. I'm the confused one here. Plus I'm also incorrect. And worst of all, I'm finite. That's what I was saying before about $A \lor \lnot A$. 1: What's what you were saying before about $A \lor \lnot A$? 0: Omniscience. I'm not god, so I'm not sure I can handle it. And I'm not sure you can handle it either. 1: What does not being god have to do with $A \lor \lnot A$? 0: Well not in every case, but at least in the case of our sequence above, I'm not sure how you'll ever convince me. 1: Are you being dense on purpose? 0: No, I'm being a mathematician. But that's a fair point. If I was being a programmer, or a statistician, or a normal human being, I'd definitely be more and more convinced as we saw more zeros and gathered more evidence. But if I'm being a mathematician, then I would object and say no amount of evidence counts as a proof. 1: Ok I'm not sure what just happened, but I feel like it's more about the sequence being infinnite than it is about "OR". 0: In mathematics, those are the same thing. 1: HOW ARE THOSE THE SAME THING? 0: Well if you tell me you believe the statement: $A \lor \lnot A$ is always true, for any well-formed mathematical sentence $A$, then all I'll say is that a very large fraction of all mathematical sentences that $A$ might stand for, when unwrapped, look something like $\forall x P(x)$. 1: So? 0: And if that $\forall$ is quantifying over an infinite set, which (again) is the case for a very large fraction of all mathematical sentences, then I'm just saying I'm not sure how I feel about the claim that $A \lor \lnot A$ 1: Ok well even if convincing a skeptic works different in the two cases above, the sentence's possible truth values are still just booleans right? 0: I'd call them propositions. 1: What was the point of calling them propositions again? 0: I just felt that they're a bit more like pre-booleans. 1: I don't understand the distinction. 0: Well if they were booleans, then as a programmer, you should be able to write code like this: ```python if A: do thing 1 else: do thing 0 ``` 1: Why can't I write code like that? 0: Well, we've assumed A is true, correct? 1: Right. 0: But you don't have the source code to the generator $a_n$. 1: I wasn't super clear on the reason for that assumption. 0: I mean you can't do some fancy static analysis or metaprogramming or introspection to determine how the code for $a_n$ works from the outside. You can only run $a_n$ and use its outputs to determine the truth value of the (pre-)boolean $A$. 1: I still think "pre-boolean" in an unnecessary term. 0: Ok, then, tell me what happens in the code block above. 1: This one? ```python if A: do thing 1 else: do thing 0 ``` 0: Right. 1: Well if we call `next()` in a loop and eventually get a $1$, then we know $A$ is false, so we take the `else` branch and do thing 0. 0: Right. 1: And if we never get a $1$, then we take the `if` branch and do thing 1. 0: So you never do thing 1. 1: Why? 0: Because you never get a 1. 1: Oh Christ, I feel dumb. I see the problem now. 0: Don't. Most mathematicians agree. 1: I must be getting sick or something. Why didn't I see the problem before? Agree with what? 0: That there's absolutely no problem with the statement $A \lor \lnot A$ under any circumstances. 1: There's OBVIOUSLY a problem! 0: Obviously? Just two minutes ago you were arguing there wasn't. 1: Sure but I had the wrong mental model. 0: How so? 1: I assumed that because these sentence things were boolean valued that they were... well... booleans. 0: Aren't they? 1: Yes! But not yet. 0: Yet? Is their type a function of time? 1: No! But I mean if your sentence is about an infinite set and you don't have the source code, or if you don't have any information that lets you reduce it to something simpler, or just in the general case I guess, if your sentence says "For all x" and you have to evaluate that boolean by checking all the x, then even if your sentence is true, you can't take the "true" code path. 0: Is it always a problem with "For all" type sentences. 1: I think so. The branch that worked was when a "1" existed somewhere in the sequence. If it exists we can find it, so we can eventually take that branch. 0: What about situations like this? Suppose A is the sentence "There exists a 1 in this sequence", or equivalently, "This generator will eventually yield 1. 1: Isn't that the first example up above? The one that didn't have problems? 0: Right, same example. 1: So what's the problem? 0: I want to write this code: ```python if A: do thing 1 else: do thing 0 ``` 1: Are we assuming A is true or false? 0: Do both cases. 1: Ok if A is true, then there's a 1 in the sequence eventually, so eventually we find it, and then A turns from a pre-boolean to a boolean and we can take the first branch and do thing 1. 0: You're using the term pre-boolean now? 1: I understand the problem now. 0: Great. Then you can do case two. 1: Ok if A is false, then there doesn't exist a 1 in the sequence, so we're back in the case of all zeros, and the pre-boolean never becomes a boolean and we can never take branch two. Damn this is a serious problem. How did I not see this before? 0: Now that you get the idea, mind summarizing it for me? 1: Ok so... - Both "For all" sentences and "There exists" sentences have a good path and a bad path. - The good path of "For all" sentences occurs when they're false. - The good path of "There exists" sentences occurs when they're true. - The bad path of "For all" sentences occurs when they're true. - The bad path of "There exists" sentences occurs when they're false. - The good path is always executable, whether the domain is finite or infinite, no matter how much information we have about the domain being quantified over. - The bad path _may_ be executable in certain highly structured special cases when we have enough information to infer something about the whole domain at once. - If we have enough information that we can handle a "For all" sentence when it's true, or a "There exists" sentence when it's false, then we can use something like a "proof" to make the bad path executable. - In all other cases, the only way to turn these propositions into booleans is to use the information we have. - In those cases, if we only have finite means at our disposal, like checking values and iterating, then bad paths are bad, and generally will not be executable. - In other words, whenever we can't reduce a statement about an infinite set to a finite sequence of steps, "For all" statements require omniscience to execute when they're true, and "There exists" statements require omniscience to execute when they're false. 0: _(Applause)_ 1: Is that sarcastic applause? 0: No! That was fantastic. 1: I forget how we got here. 0: You said you understand "OR." 1: Jesus. I'm never gonna say I understand anything ever again. 0: Please do! You understand a lot. 1: Where were we? 0: We were covering this: ![[friedman-1997-the-formalization-of-mathematics-13.png]] 1: We're still on this? 0: It's ok, let's be quick. So ZFC has "not", "implies", "and", "or" 1: I'm now traumatized by "or". 0: It's also got "If and only if" which is just two "implies" in opposite directions with an "and" between them. Then it's got variables. It's for "For all" and "There exists." 1: With one bad path each. 0: It's got a set membership symbol $\in$ so we can say $this \in that$ to mean "this" is an element of "that", and it's got an equals sign that we use to mean "these two sets have the same elements." 1: That's it? 0: Well that's the language. On top of that there's ZFC. 1: I thought this was ZFC. 0: That's the language of ZFC. The theory of ZFC is all that, plus ten commandments. ![[friedman-1997-the-formalization-of-mathematics-14.png]] ![[friedman-1997-the-formalization-of-mathematics-15.png]] 1: That was nine. 0: Hard problems of computing. Off by one errors. There's usually ten. 1: What does it mean up there where it says "infinitely many axioms"? 0: Those are sentences that can't actually be expressed in the language of ZFC. 1: What? Why not? 0: See how Axiom 3 and Axiom 7 say "For any formula in our language"? 1: Yeah. 0: Well the language of ZFC can't quantify over sentences in ZFC. 1: What does that mean? 0: It can only say "For all x" and "There exists x" when x is a set. It can't say "For all sentences" or "There exists a sentence." 1: Ok. But Axioms 3 and 7 aren't talking about sentences, they're talking about formulas. What's a formula? 0: A sentence. 1: WHAT?! 0: Right. ZFC can't say "For all sentences." But the mathematicians want to say that anyway. And they don't want to change the language to give it quantifiers that range over sentences. So instead they just sort of cheat and squeeze these two axioms into a language that can't express them by saying "We'll add infinitely many axioms for Axiom 3, one for each possible formula in the language." Then for Axiom 7 they do the same thing and add another infinity of axioms again. 1: Math is completely unhinged. 0: In this case it's not technically that bad. It's not too different from if they had implemented a parser that could parse valid formulas of ZFC. Then for any of the infinitely many axioms above, they could have the parser tell you whether or not a given sentence was an axiom that was talking about some specific formula using the axiom schema of 3 or 7. 1: Did they implement that parser? 0: No. But they imagine they could. 1: This makes me dizzy. 0: Well you asked to see the details of ZFC. 1: Nevermind, let's go back and talk about something else. 0: Ok so, the mathematicians' experience with ZFC is pretty similar to yours. They don't really like it. They don't really like talking about it. And they REALLY don't like working within it. 1: So why do they call it foundations? 0: Because they don't really like talking about foundations either. 1: Rock and a hard place. 0: So because of that, ZFC sort of ended up as an impotent figurehead type of ruler. 1: Impotent figure what? 0: Like a king with no power. Everyone points to ZFC and says "That's the foundations," but no one likes it, no one uses it, and it's basically just been sitting there for a century plus with a big crown on that says "I'm the foundations of mathematics and mathematics is the foundation of everything." Like this guy from the memes. ![[theoden-is-zfc.jpg]] 1: Damn, that sucks. 0: Fortunately that's been changing recently though. 1: How so? 0: We'll get there eventually. For now, pop the stack back to the Hirst book. Because mathematicians don't like ZFC, they tend to talk about it rather than working within it. Like this: ![[zfc-hirst-04.jpg]] 0: Feels like normal math right? 1: I guess? Not really sure. 0: That's the point. It's mostly words. Here's another example. ![[zfc-hirst-02.jpg]] 1: "We could"? 0: Yep. That's the standard mathematical approach to ZFC. They're not actually working inside the formal system. They're just sort of writing pseudo-code and English that talks about what the proof would be like if we actually did it. They call it "foundations," but they basically always keep it at arms length. Even the logicians and set theorists. There are a few solid exceptions though. For example: ![[zfc-hirst-03.jpg]] 0: Mendelson and Kleene. They do the formal stuff. 1: Who are they? 0: Mendelson is the book we saw earlier in /opt/art. 1: No way! The bit with the "hell code"? 0: Exactly. That's Mendelson's _Introduction to Mathematical Logic_. It's a pretty approachable introduction to the actually formal side of foundations. 1: The second book sounds fun! 0: The Kleene one? 1: Yeah! Is that the same Kleene? 0: Same guy! Why does it sound fun? 1:I mean if that "hell code" book was the easy one, I can't imagine what the one for "readers with a frighteningly technical bent" is like. Makes me want to read it. ![[zfc-hirst-06.jpg]] 0: Yeah Kleene's book is pretty great. 1: What's it actually called? 0: This: ![[zfc-hirst-15.jpg]] 1: What's so frightening about it? 0: It's code. 1: What's so frightening about code? 0: I mean, the book is from 1952, based on work from the 1930s and 1940s. So there's no "computer code" in there in the usual sense. 1: So how's it code? 0: Because Kleene doesn't skip steps or hand-wave or say "it can be shown." He works inside the formal system. He adds a ton of documentation -- English explanations of what's happening -- but the way he behaves as the author of that book is exactly how you'd behave if you were a programmer. 1: I am a programme--- 0: I know. But that's an extremely unusual way to behave in a math book, when you're the author. I mean he behaves as if everything he claims actually has to be implemented. He doesn't write as if he's trying to convince a human mind where you can just handwave or say "obviously" or "exercise for the reader." He writes as if he's trying to convince a machine, and then documenting heavily so humans can read the code too. Kleene was pretty clearly the first programmer. 1: Wait, I thought the first programmer was Church and Gödel and Turing? 0: Exactly. They're the first. And Kleene is the glue. Like this. $3 = \{ 0, 1, 2 \}$ 1: Do you try to be confusing on purpose? 0: What's confusing about that? 1: Everything? 0: Ok so, in Cantor's set theory, the number N is defined to be the set of all the natural numbers less than it. So 3 is the set containing 0, 1, and 2. 1: That's weird. But ok. 0: And Kleene is the curly braces and commas. The bits that hold it all together and make the set be one thing. He's the glue. 1: That feels like a stretch. 0: It's not. 1: Anyways, can we read some of that book? 0: Not yet. We'll get to the bible eventually. 1: What? I didn't ask for more bible, I asked for the frighteningly technical book! ![[zfc-hirst-14.jpg]] 0: Oh sorry forgot to explain. The "frighteningly technical" book is also called Kleene's Blue Bible. 1: Oh ok. I'm down for that kind of bible. Can we read some now? 0: Nah, we're still at Church. 1: _(Looks back through the conversation.)_ I thought that book was by Jeff Hirst. 0: Right, this one is. But this situation has been going on since Church. 1: So? 0: So we're still talking about Church. 1: We haven't talked about Church in a while. 0: This is all about Church. 1: Are you sure this wasn't just a long digression? 0: I never digress. 1: I don't believe you. 0: I promise. We just need a reverse begat list to tie it back to Church. 1: What's a reverse begat list? goto: [[3 - Church's Descendants]]