Gödel, Turing, Cantor: An Infinite Electric Arc

[00:02] hang around math forum and discuss things. Much of what I've learned about mathematics is by researching problems and questions asked by the people there. However, math forum often have a particular problem. In the same way you

[00:17] get flat-earthers and climate change deniers, in math forums, you get people who think there are just as many counting numbers as there are real counting numbers as there are real numbers. I got to see all the deeply

[00:32] flawed proofs of the countability of the reals and at the same time got a deep appreciation of the proof of Cantor's theorem. When I was studying for my comp

[00:44] sci degree, I encountered the unsolvability of the halting problem. Turing's proof of this is a key aspect of computer science, the mathematical underpinnings of computer programming. A book that I've read, which was highly

[00:58] influential on me, is the wonderful Gödel, Escher, Bach, which explains through analogy and narrative Gödel's second incompleteness theorem, which explains the limitations of provability within formal system. All these proofs

[01:15] felt very similar to me. They all used a technique called diagonalization and they were all about limitations within mathematics. However, it wasn't until mathematics. However, it wasn't until much later I learned about Löwenheim's

[01:30] fixed theorem, the grand unifying theorem of Cantor, Turing, and Gödel. I theorem of Cantor, Turing, and Gödel. I want to share this with you all now.

[01:44] into a bijection with its power set. A consequence of this, the set of counting numbers and the set of real numbers cannot be the same size. I explained the

[01:56] cannot be the same size. I explained the concept of bijection in one of my earlier videos on fractions. But a simple summary here is a bijection is a function that maps every element from one set into another without any result

[02:12] overlapping or any elements from the destination set being missed. And is a destination set being missed. And is a way we define two collections as having an equal number of things in them. We use the word cardinality to mean how

[02:27] many things in mathematics. I love factory building games like Factorio and Satisfactory and I tend to think of functions like they are little factory transforming mathematical objects from one type into another. So, how do we

[02:45] one type into another. So, how do we represent a bijection in this machine perspective? Let's start with the identity function. This is a function that returns what it takes in without making a change. Now, it's obvious that

[03:00] the both the domain, the place where stuff is coming from, and the codomain, place that stuff is going to, of the identity function must have the same number of elements in them.

[03:16] they're the same collection. An identity function function is a bijection from a collection of objects to itself. So, it expresses the rather simple idea that a collection has

[03:31] the same cardinality as itself. If we split identity function into two separate functions, one that transforms the functions, one that transforms the elements from its domain into some other

[03:44] form within a codomain, and then we have a matching inverse function which takes intermediate form from that function's domain and transforms it back into the original, then the intermediate collection

[03:59] has to have at least as many elements in it, if not more. In other words, it has to have an equal or larger cardinality than the original collection. Why? Cuz if the intermediate form had

[04:15] fewer possible elements, there would have to be a pair of domain elements have to be a pair of domain elements that would share a codomain element. And that would be impossible. This, by the way, is called the pigeonhole principle.

[04:27] In other words, it has to be able to encode all the information from the source domain into the intermediate form. If the functions are flipped around and they are still an identity, the only way this is possible is for the

[04:43] collections to be of equal size. In the type theory we're developing, we could define bijective this way. In this formula, the F is a function, the F

[04:57] formula, the F is a function, the F minus is its inverse, and this little round dot represents composition. So, applying F minus and then F to reverse

[05:09] it. The fact that if a function is bijective, it has an inverse that undoes bijective, it has an inverse that undoes that function is a very useful property. In addition, you can compose different bijections together in order to have a

[05:26] bijections together in order to have a chain of bijections to show that two chain of bijections to show that two things are bijective to each other via things are bijective to each other via some uh via something in between. I'll

[05:39] be using this later. A power set is a the set of all subsets of a a Each possible set is a set derived from the original set excluding some number

[05:52] of elements from that original set including the trivial case of all the elements are included and all the elements are excluded. With

[06:04] and all the elements are excluded. With finite elements, there will always be finite elements, there will always be two to the power of n elements in the power set. Cantor's theorem is that the power set will always have more elements

[06:18] power set will always have more elements in it than the elements in the original in it than the elements in the original set. For finite sets, that is obvious, but things get weird with infinite sets. So, rather than going off what is

[06:32] So, rather than going off what is obvious for finite sets, we have to have obvious for finite sets, we have to have proof. Indeed, this finding was actually proof. Indeed, this finding was actually incredibly contentious. Even now, you

[06:46] will come across people who will incorrectly claim that this isn't true for standard mathematics. I'm going to give you the proof for Cantor's theorem, but first, I'm going to explain the connection between power set of the

[07:01] connection between power set of the counting numbers and the badly named real number. It'll also be a warm-up for my factorial-like presentation of mathematical proofs. I like to think of bijections as a form of encoding. If

[07:17] bijections as a form of encoding. If there is a bijection between two things, you can encode that thing in the form of the other. For example, consider the 26 letters of the English alphabet. You can encode each of those letters as a

[07:32] counting number from zero to 25. There is an unambiguous, reversible rule that allows you to encode any letter as a number in this range

[07:44] number in this range and any and any number in this range as and any and any number in this range as a letter. Now, consider the power set of the counting numbers. We can encode these as bit streams, sequences of ones

[08:00] these as bit streams, sequences of ones and zeros that start but never end. We can index each position in this stream, 0 1 2 3, etc. for all of the counting numbers. And if the number is present in the subset, then a one will

[08:18] be set in the stream. Otherwise, a zero is set. You can think of this as encoding subsets as functions from the counting numbers to zero or one. Again,

[08:33] uh where that function takes a counting number and returns one if that particular number is present in the subset and zero if it's absent. This is subset and zero if it's absent. This is why I will abuse notation and sometimes

[08:48] why I will abuse notation and sometimes write this as the type natural to two. Just as an aside, it doesn't really matter what the two elements of the Boolean type are labeled as. It could be a zero or one,

[09:02] top or bottom, left and right, etc. Next, I'm going to massage the bit streams a little by applying another level of encoding. In

[09:15] this new encoding, if the original is a sequence of all zeros, it is going to be sequence of all zeros, it is going to be encoded as one followed by all zeros. The original one followed by all zeros in the original is going to be encoded

[09:31] in the original is going to be encoded as 0 1 0 0 0 and so on, shifting the as 0 1 0 0 0 and so on, shifting the ones down a set. All other streams will unaffected by this encoding. The important part is this is all the bit

[09:46] important part is this is all the bit streams except for the zero bit stream. streams except for the zero bit stream. Also, this is a unambiguous reversible Also, this is a unambiguous reversible rule that allows us to encode one type

[09:59] into the other. So, there is a bijection between these two forms and since between these two forms and since bijections are transitive, it means that bijections are transitive, it means that this is bijective to the counting number

[10:13] this is bijective to the counting number power set. The reason why I want the zero stream to be removed will become clear in a moment, but if you want to, please guess. Try to work out why I might have a problem with a stream of

[10:29] all zeros. Just before we get to that problematic operation, I've got another additional layer of encoding to do. We will use a similar technique to

[10:41] eliminate any stream that ends with all one, although in this situation, I'll keep the all one stream. Again, the explanation for this will come in a moment. All of these transformations I'm making, you can consider a bit similar

[10:56] making, you can consider a bit similar to how we move guests around in the to how we move guests around in the Hilbert Hotel. Now, with this system, we can stick a zero and a radix point at the start of the streams and encode them

[11:10] the start of the streams and encode them as binary numbers in the range of as binary numbers in the range of greater than zero up to one inclusive. And by eliminating the trailing ones in these streams, we have removed any of

[11:23] the double counting situations with situations like 0.01 repeating being equal to 0.1. If we take the reciprocal of this number, we have now encoded all of the elements of the

[11:40] power set as real numbers greater than or equal to one. Did you guess that I would have to eliminate the all zeros case because we're going to be doing something with division? If so, here is a smiley face

[11:53] stamp. Next step, subtract one. Now, our power set is encoded as all the non-negative reals. Almost all of these binary numbers will have their most

[12:05] significant digit set to one. If the digit following the most significant digit is set to zero, we'll remove that digit and negate the resulting number. Otherwise, we'll just remove the second most significant digit and return that

[12:20] most significant digit and return that number. Now, we are encoding in the form of all the reals. With this chain of bijective encodings from the power set of the counting numbers to the reals, we have proven there is a bijection between

[12:35] have proven there is a bijection between the reals and that power set. As I have said before, there are quite a lot of maths cranks out there who don't like maths cranks out there who don't like Cantor's theorem. Honestly, I don't know

[12:50] why, but some people are really uncomfortable with the fact that uncomfortable with the fact that infinities come in different sizes. I am going to now give a proof of Cantor's

[13:03] theorem for the counting numbers, aka the natural numbers, but this argument can be generalized to all infinite sets. Later on, we will generalize this proof Later on, we will generalize this proof further to include the halting problem

[13:18] of computer programs and even provability within mathematics. Now, we are ready for the proof of Cantor's theorem that there cannot be a bijection theorem that there cannot be a bijection between the naturals and its power set.

[13:33] Just a reminder, when we say not something type theory, we secretly mean something type theory, we secretly mean a function from the thing to the empty type. And how do we prove a function exists? By constructing a function that

[13:49] can corresponds to the type specified. The sigma sign can be read as there exists. Basically, it says there is a pair of functions from the natural to the power set and back again that are inverses of each other. So, if you

[14:04] compose or chain the two functions together, they'll cancel each other out and become the identity function. And here is my diagram of this type. We have

[14:19] here is my diagram of this type. We have to construct a function that takes elements of this bijection and show if it existed, then it would output an element of the empty type. Since by definition the

[14:35] empty type doesn't have any elements, we have proven that this type must not have any elements. According to the definition of a bijection, we have

[14:47] effectively four things to work with. A forward function from the natural numbers into a power into the power set. This is in a way a universal function

[14:59] that allows numbers to talk about numbers. Because every property of the counting numbers corresponds to a subset, like all the primes, all the

[15:11] subset, like all the primes, all the even numbers, the set of billionaire cut credit card numbers and such like. So, the universal function takes a number and returns that number's characteristic function. The characteristic function

[15:26] would then take a separate number and tell you if that number belongs to that subset. Note, there doesn't have to be any logical relationship between a particular number and what characteristic function it would

[15:41] correspond to. It would be like if you had a library full of books about particular functions and you just happened to number every book with a

[15:54] particular number. Or maybe an encyclopedia, perhaps all integer sequences, which would be online. The inverse of this function would take a inverse of this function would take a power set and turn it back into the

[16:09] power set and turn it back into the characteristic number for that particular set. It would sort of compress all of set. It would sort of compress all of these numbers back into a single number.

[16:21] these numbers back into a single number. We are also supplied with a witness that the inverse function inverses the forward function, witness that the forward function is the inverse's function inverse. These are proofs of

[16:34] function inverse. These are proofs of the left and right inverses. These witnesses are basically what ensures the functions behave as inverses of each other. Otherwise, they could just be any pair

[16:47] of function. With these functions, we can construct a helper function that looks like this. This anti-diagonal function, which I'm going to represent using a thur because it looks like a backwards capital D, takes a number,

[17:03] looks up that number from the universal function, then applies the same number function, then applies the same number to the return function, and returns the

[17:15] opposite result. This is a function from the counting numbers to bool. So, we can the counting numbers to bool. So, we can actually use the inverse function to actually use the inverse function to give us the number for this function as

[17:30] a characteristic function, which I am going to label with lowercase d, which I'm then going to write backwards. Now, if we feed feed back into d, we can

[17:44] if we feed feed back into d, we can construct this monstrosity. And then, if construct this monstrosity. And then, if we feed that into the witness of these numbers being an inverse, we can expand everything until we get this. Since we

[17:59] everything until we get this. Since we know that phi b is a boolean, we can examine the two cases. We can examine the case where phi b is true. In that case, we get true equals false, which is obviously false. We can examine the case

[18:15] where phi b is false. Then, we get false equals true. Again, that has to be equals true. Again, that has to be false. So, we have created an element false. So, we have created an element that must be in the empty type. That is

[18:30] that must be in the empty type. That is the thing we set out to do, thus proving the thing we set out to do, thus proving that if there was a bijection, we've just proved that if was a bijection between the power set and the counting

[18:43] numbers, then the empty type would have numbers, then the empty type would have to be non-empty, thus proving that there to be non-empty, thus proving that there can't be such a bijection. Cantor's

[18:56] can't be such a bijection. Cantor's theorem is true. Before going on to Turing's halting problem, I'm first going to examine the tools we made use of here. The first tool was a universal function that allowed numbers to talk

[19:11] function that allowed numbers to talk about number property. In other words, self-description. And the other tool we use was a function that always returned a value that was different to its input. In this case, not. A function that has

[19:29] In this case, not. A function that has no fixed points. a robotic head that when asked any question could answer by nodding or

[19:41] shaking. It is also said that he had summoned a succubus to teach him mathematics, which is totally preposterous. What sort of succubus teaches mathematics? But, could you build such a mechanical device that was

[19:56] able to answer any question? Mathematically, we call the class of things that can be answered by a mechanical device computable. And a function that can be implemented mechanically as a computable function.

[20:09] Those functions that can't be mechanically computed are quite logically called non-computable functions. In the root of this tech tree functions. In the root of this tech tree of videos, I introduced the untyped

[20:23] lambda calculus, a way of modeling computing in mathematics. And we are going to use that calculus as a way of to create a proof that there are things

[20:35] that are uncomputable. In particular, the halting problem. I am sure whenever you have looked at a program that has stopped responding, you've wondered, has it hung

[20:49] or is it merely taking a long time? Wouldn't it be great if you could work out if a program was going to get stuck or return normally? Can you build a computer program that can tell if another computer program would loop

[21:04] forever? Is the core question behind the Turing halting problem. We are going to Turing halting problem. We are going to use the same basic structure of proof that we used with Cantor. First, recall that we can turn any lambda expression

[21:19] into a number by assigning a number to each character and then using strings of each character and then using strings of numbers to represent that particular expression. Let's assume that some program written in lambda calculus that

[21:34] takes a lambda expression string and an argument to that lambda expression as a string that returns true if that combo halts and false otherwise. Let's call it

[21:47] F. Now, recall in lambda calculus that a Boolean works by having a function that returns its first argument if true and its second argument as false. We can then add two arguments, one a lambda expression that never terminates, which

[22:04] I am writing as a skull and crossbones. This gets called for the true value and we will return one when it's called with the false value. We're using one just as

[22:17] a thing that terminate. Since far is a lambda expression, we can also turn it into a string of numbers. So, what will happen if we call this lambda expression? What will it return? Well, far far expands due to the definition of

[22:34] due to its definition, then we can substitute in the far again and since we have already assumed that F far far is true, then we can simply substitute that in here, true blah blah, and since true

[22:50] returns its first argument, we get skull and crossbones, which loops forever. Oh and crossbones, which loops forever. Oh dear, we've just shown that assuming that it halts results in the opposite. Let's try the alternative

[23:04] case. Far far expands due to its definition again. We substitute in false, it now returns one and halts. But it was supposed to loop forever. In both situations, it gets the wrong result. So

[23:18] the only conclusion is that it is impossible to build such a function. And again, let's look back at our proof. We have a function that allows self-description and a function that does the opposite of its own inputs.

[23:33] something that's only possible if that function does not have a fixed point. In an upcoming video, I'm going to go over the consequences of the undecidability of the halting problem. However, there is a third limitation to

[23:47] However, there is a third limitation to mathematics of the sort that I have been mathematics of the sort that I have been describing. And in order to have proof, you have to have some sort of system to create

[24:04] proofs. These proofs exist inside what is called a formal axiomatic system. A is called a formal axiomatic system. A formal system is, in a way, the rules of the game of mathematics or alternatively, a shared mathematical

[24:20] reality. Like a game, you can have different rule sets and what might be true for one game might not be true for another. The type theory that I've been introducing throughout this tech tree is an example

[24:34] of a formal system, but there are others such as ZFC, the most common classic set such as ZFC, the most common classic set theory. A formal system is made up of three key components: a formal language in which proofs are written, a system of

[24:50] in which proofs are written, a system of logic which allows us to create new statements from old statements, and a collection of axioms which serve as our starting point. I've talked about formal languages before and I'm sure I'm going

[25:06] to talk about them again. A formal language is made up of symbols and a grammar, rules about how those symbols can be arranged. A logic allows us to take statements that formal language and derive new statements. These logical

[25:23] rules preserve the truth value between the statements. So, if something is true, then the new statement derived from those true statements is also true. Finally, we need a a starting point of true statements. These are our axioms,

[25:40] true statements. These are our axioms, which in hot tea, you kind of get many of the axioms for free as a result of the way type theory is defined, but there is no limit on how many or how few axioms you can have. Indeed,

[25:55] some popular systems sort of like have an infinite collection of axioms or more precisely, they have a schema that allows you to derive an infinite collection of axioms. There are some qualities that we would like to have in

[26:11] our formal systems. We would like it to be consistent. If we can prove something in a system, then we shouldn't be able to prove the opposite of that thing is also true. Another thing that we would like is that every mathematical fact

[26:28] should have an answer. If there is some property about a number, we should be able to create a proof to show that it is true. If that number lacks that property, we should be able to write a proof that shows that it's

[26:43] false. There shouldn't be anything where if you ask a math question, you get the answer it's perfectly fine either way. You decide for yourself. This is a property called completeness. Confusingly, there's a different

[26:57] property called completeness, which is completely unrelated or somewhat unrelated to this, but it's another thing that Gödel studied. In order for a formal system to be complete, every logical statement has to be either

[27:12] provably true or provably false. The final thing we would like to do in a formal system is to be able to use it to do arithmetic. I mean, arithmetic is one

[27:24] of the oldest form of mathematics, and it has a couple of practical uses. I think you already know where this is going from this point. We are going to transform this formal system into a to a system that can talk about itself, set

[27:39] system that can talk about itself, set up an anti-diagonal, and then use that to determine if it's able to fulfill all of these desirable qualities. The first step is to encode the systems of logic into numbers that can be manipulated

[27:54] numerically. Just like what we did with lambda calculus or lambda calculus or Unicode, we can encode logical symbols into numbers, and we can turn those strings of numbers

[28:07] into a number of their own. There are many methods of doing this. Some involve prime numbers, others involve concatenation. Whatever method we use doesn't really matter. What does matter is we end up with a number that can be

[28:20] used to represent mathematical statements, like for example, the axioms. We can then take functions that correspond to the rules of logic and allow us to derive new mathematical statements from the previous one. Let's

[28:34] call this mapping from the world of strings into the natural numbers G, and its inverse will take a number and turn it back into a string of mathematical symbols. This inverse function doesn't have any protection against it

[28:46] outputting nonsense. So, we have to be careful to only feed it numbers that correspond to well-formed mathematical formulas. Thankfully, we have the logical functions that will allow us to do that. One of these logical function,

[29:03] for example, would be the function that corresponds to the act of substitution. corresponds to the act of substitution. That is, replacing a variable name in a function with a some constant value. Now, these functions are simple

[29:17] enough that they can be expressed using the logical symbols of arithmetic. And so, again, we can encode these into numbers as well. We can then create sequences of numbers from the axioms using the rules

[29:32] of logic being applied, forming a sequence of true formable statements. And if you think about it, each of these number sequences corresponds to a proof. The last number in this sequence being the thing proven,

[29:48] and the first number in the sequence corresponding to the axioms which the proof depends on. We can then turn this sequence of numbers into a singular

[30:01] number itself. Since we have a method of turning number strings into numbers. We could even create a function that takes one of these number string numbers and a

[30:13] one of these number string numbers and a number corresponding to a sentence, and number corresponding to a sentence, and then returns true if the if the string is a proof that number. And this isn't just a theoretical thing. You could

[30:25] consider a computer's memory to be just one big number. A 64 billion-ish one big number. A 64 billion-ish digits long big number, more or less,

[30:37] depending on the cost of RAM, with the hardware and the software acting as functions on that number. So, a proof assistant like Lean is a function that

[30:49] takes a number and tells you if that number is a valid proof. It takes two number is a valid proof. It takes two numbers and says if one's a proof of the other proof. So, now we have a way of having a system talk about itself using

[31:05] arithmetic. Our statement proof can be used in a function like this one. This used in a function like this one. This says there is no proof of a statement that corresponds to X. In the case of something like

[31:18] something like 1 = 0, this function would be true. We 1 = 0, this function would be true. We can even use this function along with the substitution function we expressed before to do

[31:30] this, which we can then unwrap. This can be read as there is no proof of A. Now, let's consider what happens if this is false. That means there has

[31:44] if this is false. That means there has to be a proof that exists that proves A. However, this mean must be a sequence of logical statements that starts from the axioms of the formal system and ends with A. However, since A is false, that

[31:59] it represents a chain of logic from a true statement to a false statement, which is a contradiction. One of the things that we didn't want. However, what if A is a true statement? Well, we have a true statement that exists, but

[32:15] system that proves it. We had to step outside of the system to bring it into existence and show it that it was true. Now, and show it that it was true. Now, sometimes Gödel incompleteness is

[32:30] oversold, saying things like mathematics has no certainty. However, we can be very confident in mathematics. If any formal system had a contradiction in it, then it would be most likely discovered pretty quickly. All of the popular

[32:46] pretty quickly. All of the popular systems of mathematics have had heaps of systems of mathematics have had heaps of people examining them. So, we are likely in the second situation, that there are mathematical questions

[32:59] whose answers are independent of the axioms. There's no generalized way of checking for this unprovability. Another consequence of all of these limitations

[33:11] of mathematics that we have been going through. However, there is another way out. We can create a formal system that is both consistent and complete. All we have to do is reduce its power, so we can't do general arithmetic. If you look

[33:26] back at my explanation of the halting problem, a similar way out exists there. If you restrict the expressibility of lambda calculus, then you will get to a

[33:38] point where every function halts. For example, in certain forms of typed lambda calculus, which is why we've been using a typed lambda calculus as the

[33:51] using a typed lambda calculus as the foundation of our logic. It seems that there is a point of expressiveness that as we get closer to it and move over it, things start to break down. Now, if you look at these proofs, you would have

[34:07] noticed a common pattern. We created a way for a system to talk about its own property. Or, in more formal mathematical speak, we created a mapping between the objects within a system and that system's exponentiation. We then

[34:23] created a diagonal within the codomain of the map and showed that it led to of the map and showed that it led to some sort of contradiction. At the core some sort of contradiction. At the core of mathematics is spotting patterns

[34:37] and generalizing and abstracting those patterns into ideas. Löwenheim recognized recognized this pattern with these type of diagonal proofs and developed what is now known as Löwenheim's fixed point

[34:53] theorem, which I will go over in part two. So, please join me for that.

[35:05] to acknowledge a few projects and people. The incredible proof machine, people. The incredible proof machine, which strongly influenced my seeing of which strongly influenced my seeing of proofs as a form of node-based system.

[35:19] Nelson S. Yanofsky, whose paper A Universal Approach to Self-Referential Paradoxes, Incompleteness, and Fixed Points introduced me to Löwenheim's fixed point theorem. Also, uh Professor Yanofsky has a YouTube channel, which

[35:36] should be linked in this end card as well. Thank you very much for watching, and I hope to publish the next part of this video soon. But, all as always, I

[35:48] might get distracted and post a few other videos on other topics just to keep things flowing. Thank you very much for watching, and I hope to see you for watching, and I hope to see you later. Goodbye.