Gödel's Incompleteness Theorems Explained with Lean Proof Assistant

[00:00:00]Yeah, I thought uh I'd talk about uh Gur and uh his famous theorem, Gle's incompleteness theorem because it's something I I cover in my logic course at the very end and I think it's I mean it's quite fascinating and although I think there are lots of people who who think this is philosophically very I mean have some conclusion whether God exists or stuff like this which I don't think is has anything to do uh with this theorem. It's over over valued has a sort of populist uh account. Yeah.

[00:00:37]>> And okay. So I'm going to show my ignorance here though. Is this something you can summarize before we go into the detail because I I don't know.

[00:00:44]>> Yeah. I want to start with something which is hopefully which is quite simple.

[00:00:50]What I'm doing in my logic module which is called introduction to formal reasoning.

[00:00:56]uh we we learn how to use this tool here called lean which is an interactive proof system. I think we have done >> some videos about it already and so here I have two propositions P1 and P2. What does P1 say? P1 says for all natural numbers n + 0= n and P2 says for all natural numbers N + N= N. So now I want to decide these propositions which means I want either to prove them or prove the negation. So what I can do here in in lean I can prove P1 in two steps very easy yeah short proof and I can prove the negation of P2 and here I use just the fact that if N is 1 then 1 + 1 = 1 is two and that's uh no that even lean knows that this is not true.

[00:01:47]>> Okay.

[00:01:47]>> Okay. So here's my question. Is it true can I for any proposition P can I prove either P or not P? And that's a question which G or actually Hibbert already asked. So if I have a proposition P is my proof system good enough or complete in in the sense that for any propositions I can either prove P or not P. I we've seen in these examples for P1 I can prove P and for P2 I can prove not P. Right? But the question is can we do this for any proposition?

[00:02:27]>> I'm guessing the answer is no.

[00:02:29]>> Yeah, you're you're as good as Google.

[00:02:33]Let me let me let's look at at another proposition. I'm not going into the details here. So that's a famous problem in computer science. It's actually the most famous famous problem. It's a problem about problems. Sorry for the for the confusion.

[00:02:47]The problem is uh uh uh is a is a set of natural number a subset of natural numbers like the set of all prime numbers set of all even numbers and so on. Yeah. And now we can define the set P is a set of problems which we can solve on a on a touring machine in deterministic polomial time. Yeah. So which is feasible. And then there is a a class NP which is the the set of problems which we can solve on a nondeterministic touring machine in polomial time. And yeah uh the problems in P are easy problems u like yeah astonishingly this is recent result that the primes are NP whereas NP are problems like uh I give you a a formula in propositional logic find out whether there's a satisfying uh uh uh evaluation satisfying assignment of truth values Right? So that's quite hard because they're exponentially 2 to the n many lines in a tool table. Um so that usually requires exponential time. But on a nondeterministic touring machine you can solve it in polinomial time. Now the famous question is is P equal NP or is P not equal NP? And actually nobody knows. So nobody has a proof of either.

[00:04:17]That's why it's famous. You can $1 million by the way if you can.

[00:04:20]>> Okay.

[00:04:21]I'll nip home and see.

[00:04:22]>> Yeah. Yeah.

[00:04:23]>> Put some time on it.

[00:04:24]>> Yeah. So, most people believe that P is not equal NP, but nobody has a proof.

[00:04:29]Neither is a proof of P equals NP. But I mean, most likely it's just because we are too stupid, right?

[00:04:38]We >> Well, we'll check GPT and see what comes out.

[00:04:41]>> That's a good always a good approach.

[00:04:42]Yeah, we should try this. Yeah, >> I'm going to >> since we don't know, it could be that our proof system is not strong enough.

[00:04:48]And this was something already observed by Hbert, David Hbert, famous mathematician. He's he's really good guy. But here he plays the role bit of the not so clever guy because he said, "Yeah, I mean if we have a logical system which is incomplete, we can just add something and make it complete."

[00:05:07]Yeah. So maybe we have to add this as an axiom that P is not equal NP and then then we are fine. Yeah. We decide this.

[00:05:15]And basically he thought if we have an incomplete system if we just add enough exum we will make it complete.

[00:05:23]And now comes G. Yeah. So G defines a proposition G proposition so that we can neither prove G nor we can prove not G.

[00:05:34]Okay. And he did this for the theory of uh arithmetic. So which is just a theory of natural numbers with some basic axums about natural numbers. So let me yeah let me go outside of of lean and and let me construct uh a a good sentence right actually I have to move between lean and and paper but we'll do this. Okay.

[00:06:06]So if you look at at lean here when we do a proof you see this symbol here this turn style right it's called turn style because it looks like a turn style. So we're looking at this G is such a proposition and we want that we're not able to prove G and we also not able to prove not G.

[00:06:26]And so so what Gur was able to do he said in the theory of arithmetic and the theory about natural numbers with some basic operations like addition and multiplication and some basic exums we can always find such a statement and even better he could also show that not only in arithmetic but anything which extends arithmetic which is for example lean we can define such a proposition.

[00:06:54]So how do we do this? Okay, so the first step in Google did is let's say P is any proposition then we have a natural number which we which write here funny brackets P which is a natural number which represents this proposition. What does it mean? P here is some formula something which you have seen there for all X natural number X plus 0= X or and so on. And now we want to represent this inside our system because the basic idea of girdle is that we always get this girdle sentence this sentence G if a system can talk about itself if you can sort of implement it in itself and the first idea is that we can represent these propositions as natural numbers.

[00:07:41]Now you can think for a while how to do this but I'm claiming it's sort of obvious for any computer scientist because you can represent proposition as some bytes in computer memory and some byes are just a natural number just a number maybe a very big number but it's just a and we can also define when something is provable so let me let me let me say this let me just pretend I can do this I say I have a predicate or set of natural number which I call proof So the are the natural numbers which correspond to propositions we can prove.

[00:08:15]So what do you want to say? I want to say if I can prove a proposition P then it is the same as if I can prove inside my system that the code of P is in the set proof. Okay. So what I'm saying here I can prove P if and only if I can prove that this the code of P is an element of my predicate of my set. So that means I can encode probability inside my my logical system and uh and and Gur observed that you can do this in arithmetic with a bit of hacking. Uh you can just encode the the the probability of arithmetic inside of arithmetic. It's bit what we do in computer science always you know you write a compiler for C in C. So here we we we define the logical system of arithmetic within arithmetic. No big deal. It's it's hacky. Yeah. Like hell because you have to do lots of encoding, lots of twiddling, but it's it's not impossible.

[00:09:25]It's I I don't want to write it down. I mean I can't because it would take long time. Okay. Now let me let me go a little bit further and let's say uh we really want to think about predicates.

[00:09:38]If you have a predicate Q which is a set of natural number. Okay. So we we can do this. So here we do this for P is a proposition but I can also do this for predicates on natural numbers. So I have this predicate proof two which is like proof but with a parameter. And what do I want to say? If Q is is a predicate on natural numbers or a set of natural numbers, then I know that I can prove Q of N if and only if I can prove proof two. Oh, sorry, I I I I changed this.

[00:10:12]What I want to say is if the pair of the code for Q in the number n is in proof two. So what proof two is is a bit of a variation of proof. for proof is just for for propositions.

[00:10:26]But if we can encode proposition, we can also encode predicates. So predicates are just subsets of natural numbers which we can define here. And we now say I have a code for every predicate such that I can prove q of n if and only if uh the spare qn is in my proof predicate. So it's a bit of a refinement of the first that I can do this not just for propositions but also for predicates which are proposition depending on some values right and now if I can do this I can define something weird and this is a set of natural numbers I define in lean and this is the set of of quotes such that you cannot prove that that n comma n is not in in this in this relation proof two. What does this mean? And it it means that that if n is a code of a proposition then the proposition applied to its own code. You you take like you take a program and you feed it its own input. Yeah. This is the technique of diagonalization which we use in in lots of situations. So we say so v is a set of natural numbers that if n is a code of a of a of a predicate and I apply it to itself then it should not be probable. Okay. So it's it's a set of quotes for predicates which if applied to their own code are not provable.

[00:11:57]>> This reminds me a little bit of the undecidability.

[00:12:00]>> Yes. Yes. It's the same idea. It's like it proves something different with the same technique. The technique is called diagonalization. And we use it for lots of things. We use for for the for the undecidability.

[00:12:11]But we also use it to prove that uh so that there more than one infinite set.

[00:12:16]Yeah. the set of uh uncountable and uncountable sets is bigger than the set of countable. So they're infinitely infinitities is the same idea. Okay. So so now if I have the set V then something I can define a girdle sentence and the girdle sentence is just so if I have Viet I take the code of Viet and the question is is Viet an element of Viet? So is a code of viet an element of the set v. Now by the definition of v this is the case if v code of v is not in proof two. And now by the definition of proof two this is the case if and only if not the course of weird is an element of the predicate weird. Right?

[00:13:08]What did I do? I said when is we an element of weird? I look up the definition. It's the case if if the could of v applied to v is not an element of my proof two predicate but by by by the property that proof two really corresponds to provability this is the case okay now I should have done a turn star this is provable if this is provable if and only if this is provable so the situation I have weird and weird is provable if not weird and weird is provable And that means that this here is a good sentence because now I can prove G if and only I I can prove not G.

[00:13:57]Yeah. So G is a is is a statement that V is provable for its own code. That is provable if and only if the negation is provable. Now that means if I could prove G then I can prove not G and then I can prove false. It means my system is inconsistent and if I can prove not G I can prove G and also means my system is inconsistent. So this sentence G is such a sentence where you cannot prove it and you cannot prove its negation.

[00:14:31]>> So is that the incompleteness?

[00:14:32]>> That's the incompleteness theorem. It's the first incompleteness theorem.

[00:14:37]Yes. Uh there is a second one which says uh that uh you you you cannot prove now we can we can talk about the system in itself. Right. And we can ask the question is is false not provable? Yeah. If false is provable that means the system is inconsistent. And and the question is can we prove that we cannot prove false?

[00:15:00]So not prove false. Can we prove in a system that it's consistent? And it turns out and this is the second incompleteness theorem which relies on the first one is we cannot prove this either. We we we in particular we cannot prove which is not surprising. I mean if you have a logical system so so it's like pulling your yourself out of the swamp you know proving proving in the system itself that the system is consistent and that's not possible. So that's is the second incompleteness theorem and it how to prove it is by taking the first one and then going one level higher and encode the proof of the first one inside arithmetic. So it's getting I mean it's not technically complicated but you start to lose track on the levels you know I'm talking about the system talking about itself.

[00:15:58]>> Yeah it's I'm getting inception vibes.

[00:16:01]So >> getting what vibes? Oh, do you remember the film Inception?

[00:16:06]>> Oh, yeah. Yes. Yes. Exactly.

[00:16:08]>> Okay. Which is a little bit cliche, but you know, dream inside a dream inside a dream.

[00:16:12]>> Yes. That's exactly what going on. And it's it's it's it's just keeping track all the levels makes it makes it confusing. Yeah.

[00:16:22]>> But let me say a few more things about this incompleteness theorem. Uh first of all, it applies to arithmetic. But if you look at the proof, it's actually also works for any system which includes arithmetic.

[00:16:38]So so so it it it doesn't help like Hbert hoped that the uh to make the system stronger because this defect always remains you. It doesn't matter how strong you you make it you always get this incompleteness but you can make it weaker. Yeah. So uh in g observed this incompleteness theorem all you need is addition and multiplication which is quite clever hack. Yeah.

[00:17:08]Um but if you leave multiplication out then it's complete. Yeah. But then you cannot do as much in particular in this system uh is called presber arithmetic it cannot talk about itself because obviously if it could talk about itself it would be incomplete. Yeah. But it's useful for for some things and there are some some surprising system which are complete. So for example if you if you encode the the logic of the real numbers the the the field of the real numbers. Yeah. Uh it turns out that this is complete.

[00:17:46]So that because because you don't have the natural numbers you cannot do this programming stuff. Yeah. just with the real numbers and the real numbers on its on its own are complete. Yeah. And another example is geometric ge geometric geometry geometry.

[00:18:06]uh uh so Uklides uh it was the first aum system formulated for about lines and lines being in parallel and cutting each other and and and so here the exoms of of geometry are actually complete but again and just with lines and points you cannot talk about itself.

[00:18:27]So it's it's a weak system. Yeah.

[00:18:37]it is. on that sphere. If Sha and I start walking due north and we keep our angles with the equator rigidly the same as each other, then the innate curvature of the earth, so long as you are