What A General Diagonal Argument Looks Like (Category Theory)
Vložit
- čas přidán 16. 05. 2024
- Diagonal Arguments are a powerful tool in maths, and appear in several different fundamental results, like Cantor's original Diagonal argument proof (there exist uncountable sets, or "some infinities are bigger than other infinities"), Turing's Halting Problem, Gödel's incompleteness theorems, Russell's Paradox, the Liar Paradox, and even the Y Combinator.
In this video, I try and motivate what a general diagonal argument looks like, from first principles. It should be accessible to anyone who's comfortable with functions and sets.
The main result that I'm secretly building up towards is Lawvere's theorem in Category Theory
[link.springer.com/chapter/10....]
with inspiration from this motivating paper by Yanofsky
[www.jstor.org/stable/3109884].
This video will be followed by a more detailed video on just Gödel's incompleteness theorems, building on the idea from this video.
====Timestamps====
00:00 Introduction
00:59 A first look at uncountability
05:04 Why generalise?
06:53 Mathematical patterns
07:40 Working with functions and sets
11:40 Second version of Cantor's Proof
13:40 Powersets and Cantor's theorem in its generality
15:38 Proof template of Diagonal Argument
16:40 The world of Computers
21:05 Gödel numbering
23:05 An amazing program (setup of the Halting Problem)
25:05 Solution to the Halting Problem
29:49 Comparing two diagonal arguments
31:13 Lawvere's theorem
32:49 Diagonal function as a way for encoding self-reference
35:11 Summary of video
35:44 Bonus treat - Russell's Paradox
CORRECTIONS
21:49 - I pronounce "Gödel" incorrectly throughout the video, sorry! Thanks to those who have pointed it out.
- Let me know if you spot anything else!
This video has been submitted to the 3Blue1Brown Summer of Maths Exposition 2
#some2 #mathematics #maths
====Timestamps====
00:00 Introduction
00:59 A first look at uncountability
05:04 Why generalise?
06:53 Mathematical patterns
07:40 Working with functions and sets
11:40 Second version of Cantor's Proof
13:40 Powersets and Cantor's theorem in its generality
15:38 Proof template of Diagonal Argument
16:40 The world of Computers
21:05 Gödel numbering
23:05 An amazing program (setup of the Halting Problem)
25:05 Solution to the Halting Problem
29:49 Comparing two diagonal arguments
31:13 Lawvere's theorem
32:49 Diagonal function as a way for encoding self-reference
35:11 Summary of video
35:44 Bonus treat - Russell's Paradox
I would love more videos like this if you get the time and interest.
Bruh, how can you make one of the very best math explainer videos on youtube and then just stop!? Can you imagine how disappointed I was to finish this video and go to your page to start watching them all?
Thinking about category theory as the linguistics of mathematics is a big breakthrough for me. I think this might be the best introduction to category theory I have seen so far. Could you make videos exploring more of category theory from this perspective?
Thanks for the kind words! I am working on a follow up to this video on Gödel's Incompleteness Theorems (viewed through the same lens). I hope the comparisons to linguistics in that and other future videos would scratch the same itch!
That was actually how I first got started looking into category theory! David Spivak wrote a great article called "Category Theory as Mathematical Models" covering some of that idea, and I would definitely recommend it (as well as the rest of his work on applied category theory)
I never heard that analogy before, very interesting!
@@Thricery I would also love for you to continue this series. Concrete applications of Category Theory really help bridge the gap to the abstraction at a pedagogical level.
Well, that would explain why it interests me.
This is the best introduction to category theory I've ever seen. It managed to actually motivate category theory for me. Calling it the "linguistics of mathematics" was a really clever metaphor.
This video is a shining example of clarity.
That was an amazing video! I had an intuitive feeling in the back of my head that those proofs were similar, but this really opened my eyes
Yaaay category theory!
@@onion013 Woops, 1 year later but no new video!
This was a really cool view of diagonal arguments that I'd never seen before. I really like the (new to me) view that diagonal functions enable self reference! And everyone knows self-reference opens to door to all sorts of contradictions, so it makes perfect sense in hindsight!
I really love this video. Cantor's diagonal and the simple halting problem proof you described are my two favorite proofs in math, and it's really nice to see how well they fit together. In fact, I thought about making a SOME2 about one or both of those, but you've done it better than I ever could, so congrats!
That second version of Cantor's proof made it finally make sense to me, i've seen it explained countless times before but i've never felt it was rigorous enough. Awesome video!
This is probably the best math video I've ever watched! Really added a lot to my understanding of diagonal arguments and category theory.
That was a powerful intuitive explanation of the diagonal argument. I’m glad you didn’t stop there. I’m glad you did the math after giving us the aerial view. Subscribed.
Great stuff! I've encountered many of these things before and always had a sense that they were connected somehow, but never had the confirmation and clarity you provide here. I love that CZcams's index for your video ends with "cc" which reminds me of C compilers and quines and Ken Thompson's paper "Reflections on Trusting Trust". What a fertile area for thought this is. Anyway, please do make more videos; I will certainly watch!
Thank you for this beautiful, mind expanding presentation!
Thank you! Your video shows fantastically the actual practical usefulness of category theory, which is something I never saw before.
OMG, i'm so happy to find this (through 3b1b), for years i've been wanting to dig into this puzzling aspect of math/ reality but didn't have the skills necessary, it always felt to me like a trick in the worst case, or an obvious observation about axioms and foundations of knowledge in the best case (especially thinking of Godels incompleteness theorems, and their implications). I am "almost literally" dying to see your next lesson/ "take" on the matter, CAN"T WAIT!! :)
what a brilliant comparison with language!! i love seeing overlaps like that. keep up the great work!!
probably the best intro to what's great about the categorical point of view I've ever seen.
kudos for your fantastic work.
As fine an explanatory video of a complex topic as I've ever seen. And, as another commenter said, a great intro to category theory.
This is an excellent video! I think this kind of application of category theory to make sense of key concepts in mathematics and logic is the best use for it - using abstraction to show (just) the important stuff is exactly what cats should be for! Bravo, and I'm looking forward to more!
I love videos that let me see things in a whole new light. I've studied all the examples here but never considered their relationships.
amazing insight between those seemingly distant concept
I can't believe I only now came across this video, it is the absolute best and most comprehensive explanation of diagonal arguments out there, from beginning to end. I truly hope more videos are in the making!
Very neat perspective! I knew about the diagonal argument and the various self-referential paradoxes separately and never thought they were actually instances of the same concept
I know they are related somehow because all of them involve a flipping function. But I did not know that this relatedness is rigorously express in category theory.
👏 excellent, I love category theory and this is an awesome introductory exposition.
Well done! Many thanks for your clear inside into the background of category theory.
Amazing quality stuff! Finally someone lucidly shows the path from diagonal argument (Cantor) to the fundamental limitations of math (Gödel), comp. sci (Turing) and philosophy/language (Liar's & Russell)! Brain orgasm, literally! 🥳
This was very well explained and illustrated, kudos to you!
Wow, that was brilliant. Beautifully explained the link between many fundamental results 🙂
Great great video. Looking forward to the next one about Gödel's theorem.
Well done. I watched the whole video. Very interesting. I guess this is an example of a meta level of thinking. I will need to watch it again and do some practice before I claim to fully comprehend but it was very interesting and intriguing.
This is the best introduction to category theory for making proofs I have seen. Superb video sir!
I love the way you motivate the proof of the halting problem. It's really surprising to see the similqrities with th classical diagonal argument!
This CZcamsr discovered this one trick, see why mathematicians hate him.
This was actually pretty mind blowing. One of those concepts that are extremely deep and powerful but once someone explains it to you in a pedagogical sense it feels so intuitive and simple like it is something that should have been obvious all along.
Amazing video, my brain will never be the same again.
This is amazing. Applications of Category Theory are so cool
This is such an excellent video, it's a real shame it doesn't have more views!
This was incredible! Thank you so much :)
Very cool video ! I'm waiting for your video on Lawvere's fixed point theorem, and hopefully a bit of topos theory, which is really at the heart of all you're explaining. As an algebraic geometer, I'm used to see a topos as some kind of "space", but seeing these results which are more on the logical side of the theory is always a pleasure.
Perhaps one day logic and type theory will give us a purely syntactic approach to these objects, model-independant, which will surely
be useful in (higher) topos theory.
Beautiful presentation of a beautiful concept. Bravo! Bahut atchah! 😃
Oh man, I liked this video so much that I hit a like from all my google accounts. Really great work!
Masterful presentation!!!
Really beautiful and intuitive explanation of how the capability for self reference relative to a base set like {0,1}, {halts, doesn’t halt} etc. leads to the non-existence of functions that describe everything you care about (infinite binary seqs, programs/data) in terms of that base set. Like, if the the collection of things you’re trying to describe via some property is TOO expressive, through being able to refer to itself having the property you care about, it can actually prevent you from having any hope of describing everything in terms of that property at all! Kinda feels like someone trying to run a classification algorithm and ending up having data points that lie directly ON your decision boundary, rather than on either side.
subscribed!
I was learning Haskell programming language and was delighted to see many terms I've already seen there applied in maths (where they originally come from, actually)
Excellent video, really enjoyed it. Eagerly waiting for the continuation on Godels incompleteness theorems :)
Great analysis
Excellent. I look forward to your presentation of Godel's incompleteness theorems.
What a journey! We went from counting to computation to turing!
Can't wait for the follow-up video on Gödels incopleteness theorem :)
This is fantastic
Incredible! Fantastic job :)
great stuff! and thank you for the links
That was so satisfying!
Excellent explanation 👌
This was very intructive and to the point. At the same time, it was vivid and descripive without any graphical animation tools - respect! The only thing I'd like to recommend to get an even better presentation, is to improve your sound recording system ...
you were mentioned .. caught my interest .. will watch but not on a saturday night.
Excellent video, really like it. Would really love to hear your ideas about what the pattern itself "means" :) And looking forward for the Godel theorem video.
I love lawvere's fixed point theorem and I'm glad someone is talking about it. I wrote a formalization of it in agda if you have any interest
I'm busy trying to wrap my puny brain around Y-combinators in a practical way, since in recent years they've gone from a functional language curiosity to a way to wrestle compilers into tail-call optimization-like behavior whether they're spec'ed for it or not (what blew me away was following a tutorial to write factorial in javascript, ending in a Z combinator, the moment when I began typing out the command to give me 25!, as soon as I closed the parentheses the IDE spat the answer out on the next line. I was like "aren't you supposed to wait for me to execute this?" but to increasingly intelligent editors which anticipate your input, they had already stacked 25 copies of my function on top of each other before I formally ran the program). Since I'm not even close to understanding the gestalt of them, I'm scratching my head about questions like "what is the fixed point of merge sort?". So I'd be interested. Unlikely I will understand it though.
Its a really nice video!
Great and brilliant video! I'm just become a fan of yours, I respect your times but please for all humanity don't leave CZcams.
I'm late to the party here, but damn... this video is _criminally_ underexposed. A terse yet lucid illumination of a delightful, profound, and easily missed common thread. Bravo.
12:00 - Visually, this really looks like asking if every f: N --> {0, 1} is "representable", in the sense of Yoneda. Of course, it's not literally asking that because N doesn't have the necessary categorical structure, but I wonder if it's possible to construct a category with objects indexed by N whose Hom-sets encode L. Awesome video!
Great video. Impatient for the Godel follow-up.
Any chance that such a categorical explanation could be given for the forcing argument?
19:36 It's possible to work with a kind of set theory where every partial function is computable, so the correspondence between programs and partial functions is perfect. In particular, if ZF is Π¹₁-consistent, then there is a computable model of ZF. Slightly less-abstractly and more-practically, in computability theory, one can define a near-equivalent to partial functions called computable functions that corresponds to programs exactly.
Amazing video!
Good work!
This is a very strong video
Here's a solution to Russell's paradox using verbs and relative order, though in this case the order isn't between verb and object but between the actions denoted by repeated occurrences of a given verb. The set R includes all and only those sets which do not include themselves. The verb "include" occurs twice, and though here it's written in the same grammatical tense, usually known as the present simple, it denotes actions which in fact are performed in sequence since they are uttered in sequence. What sequence that is becomes clear when we use explicit grammatical tenses: R includes all and only those sets which didn't include themselves, (or R included all and only those sets which don't include themselves). To make it even clearer we could add in adverbial time markers: R includes now all and only those sets which didn't include themselves before. This parallels the famous barber version: The barber shaves now all and only those men who didn't shave themselves before. Contradiction gone once we make a distinction between tenses. There's already a precedent in elementary arithmetic. 2 + 3 * 4 = 14 or 20? Solve this by explicitly marking the sequence of operations we want, in this case perhaps by using brackets or a convention like PEMDAS.
Time doesn't really "exist" in mathematics though. A formal sense of such timing would introduce a lot more complexity. Nevertheless, there is a similar things that mathematicians do where, I think in some typed lambda calculi, they have a time Omega_0 whose elements are all types that aren't itself, and a type Omega_1 whose elements are Omega_0 and the elements of Omega_0, and so on for Omega_N, and hence in each step you can never have a statement about Omega_n inside itself, you can only talk about it within Omega_n+1. A similar thing, as you mention, happens with order of operation, but in this case it's a wildly different thing where it's not the language that is ambiguous, it's the statement itself that is contradictory. What it leads us to do, regardless, is to reconsider the rules of the system and limit it.
LINGUISTS of MATH! so neat
Linguistics example really was great
Waiting for the second part
Wow. A new math channel. Interesting.
At 13:00 the contradiction is much more satisfying than the first proof. The first proof has that feeling of doubt that you just haven't looked far enough. But the second proof says if somebody tries to tell me that my S is in b, I can ask well where is it? What's k? Then I can look there and prove them wrong.
Amazing vid man! +1 sub :)
For the first example, I came up with a "counterexample"--
Write down each number, essentially "incrementing" from left-to-right in binary:
.1000000...
.0100000...
.1100000....
.0010000...
.1010000...
Then if you apply the diagonalization, you get the number .00111111111... which is equal to .01, the second number on the list. (This is like the .9999..=1 thing, but for binary.)
It's not a real counterargument, but is a case where the diagonalization argument fails (the diagonalization argument just needs any case where it works).
0100000... ≠ 0011111...
4:37 it's cool to see how the diagonalization argument subtley uses the axiom of choice, which we just take for granted.
How does it use the axiom of choice?
(I know this is pretty silly of me, but I'm just commenting to say that I just so happened to be the 1000th person to like this! It most definitely deserved it.)
This video was so good, even though I was familiar with the different examples for diagonal argument the generalization gave it all a new perspective and looking at the argument as function composition is really cool.
I had a thought after watching it, is there a famous diagonal proof where the set of values has more than two values?
Great question! A silly and unsatisfying answer would be "yes, it works even if we consider infinite trinary sequences for Cantor's diagonal argument", but that feels like cheating because it's not an essentially new idea.
That being said, during the construction of the Y Combinator, the "collection" of Values will have more than two things in it, and that will genuinely feel very different. I think my video on the Y Combinator will be part 3 in this series (after the incompleteness theorems) - so stay tuned!
@@Thricery I would love to see the video on Y combinator!
I have a question. Our function L somehow acknowledges that there in fact is a listing of all posible 0 and 1 lists, because there they are, just input a certain k and you get the list b_k(-)=L(k,-). However, we prove that there is some list b that is not listed by any k, so doesn't this prove that L cannot exist as a function such that L(k,m) gives the mth element of the kth list of infinite sequences in the first place?
Very interesting video, thank you ; awaiting the upcoming ones !
Is it possible to use bolder pen for drawings ? Sometimes they are not very legible on a mobile phone (depends also on color).
Thanks for the feedback, I'll try increasing the line thickness for the next video and will have a look into what colours work nicely! :)
@@Thricery Have you unlisted all the other videos or did this end up being the only one made?
Great video, thanks. Please make more content on Gödel's theorem. There is a niche for this type of video on youtube, I think you could be very successful :)
No Y combinator? That's my favorite one...
Stay tuned! It's mine too (I have a Y Combinator tattoo), but I think I need to build up to it!
Why do you need to specify that countability means the ability to enumerate a set's members one at a time? Are there uncountable sets that can be exhaustively represented if their members are enumerated all at once?
Looking forward to the Godel video!
Small point: to translate from a sequence of 0s and 1s to a number, you should place a 1 in front of it so that leading zeros don't get deleted. Every (nonzero) binary number begins with 1, so this is bijective onto those.
Very enjoyable video. But, if you find working at this abstraction level, do some programming and formal verification in Haskell. This level of abstraction will start feel natural after a while.
Excellent video! Hopefully #SoME2 will give it the exposure it deserves. It almost makes category theory seem useful. The question remains however, has Lawvere's theorem ever been used to prove things (outside Category Theory itself), or has it only ever been used to show _a posteriori_ that the proofs were similar? That is, has it been useful in mathematics, or is it just clever hindsight?
Great question! I personally feel like "pointing out similarities" and "demystifying theorems" is itself useful in mathematics, because it means that what used to be several different tools in our mental toolbox can be combined into one tool. More explicitly, it could be useful and lead to "new results" whenever some context is newly realised to be a Cartesian Closed Category. Then, Lawvere's theorem holds, and we can benefit from that. Whether or not that has happened historically (or is likely to happen in the future) is not something I know, but will be curious to learn!
I don't know about Lawvere's theorem; this was my introduction to it. But on the usefulness of Category Theory, I'd like to point you to the Curry-Howard-Lambek isomorphism. Results in logic now have an immediate corresponding result in computer science. You might say there exists a functor between the two categories.
Lawvere’s theorem helps explain why character theory with the trace (diagonal) function is important with representation theory.
27:30 Doesn't the k used as input into k, also need an input? And so on?
Damn man really good stuff, we were recently doing a real ana;ysis course and it always bugged me why we had to formalize a function for cantor diagonalization as i thought of it to be of little importance.
ps i was wondering how the lawrence theorem sort of resembled the hairy ball theorem, turns out that for even dimensional spheres the lawrence theorem is a corollary to the hairy ball theorem.
Very excellent video! Great presentation with clear and concise examples that intuitively correlate to the concept being explained! Please invest in a pop filter and highpass your narration at ~150Hz.
Thanks for your feedback!
brilliant video, may I ask how this is related to the Y combinator?
Stay tuned, it'll be in part 2 (where I talk about the incompleteness theorems) or part 3 depending on what fits!
Captivating; reminded me of 3b1b :')
holy shit what a video
Take all my money this is CZcams gold
Infinite was not defined.
Assume there are countably infinite digits in a sequence. Then all the sequences are listable and the diagonal argument fails. If there are n digits in a sequence, there are 2^n sequences, for all n.
Example: two digits in a sequence
1) 00
2) 01
3) 10
4) 11
The diagonal number is 10, which is in the list.
A real number in [0,1) can be represented by a sequence of digits, finite for a rational number and countably infinite for an irrational number. Hence the real numbers are countable.
Audio tip - a pop-shield would vastly improve your audio for little to no cost. Otherwise thanks for the vid. It is beyond my understanding, but it expresses ideas I had vaguely formulated in thinking about Godel.
Thank you, I hope to do this for the next video! :)
@@Thricery An old trick is to get some tights (thin nylon legwear mostly used by women) which are torn and will be thrown away, and attach it to a piece of wire such as a coat-hanger. Add layers until you are satisfied.
You could also improve the sound just by pointing your mouth a little to the side of the mic so the big rush of air does not hit it directly when you say 'p' or 'd'.
Why do I ask for this? Well audio that clips is quite bad for speakers and can degrade them.
@@Thricery Also, the audio is too low. After turning all the sound settings to maximum, this video is still slightly quieter than other videos under my normal setting.
This is Artificial Intelligence in synthesis, and a conglomeration of symbolic, imagined discrete, temporally displaced if you accept that past-future superposition is distance not centred on the real-time wave-package envelope-shaping time-timing sequence tuning of the Observer's POV. An example of thinking for your self in Self, Theoretically, shape shifting i-reflection actual arrangements of ONE-INFINITY.
What are you talking about man
Lawvere Rules!
Pretty cool explanation. Looking forward to the rest. But since you have already announced the topic... Gödel is pronounced differently.
Does the binary diagonalization argument require the axiom of choice? If so, where?
Such a list is not possible that is it can not logiclly exist. Consider a universe of elements that is finite - say the English alphabet. Let's start with the set { a, b, c }. The possible combinations of the elements of this set can be enumerated -
1. a, b, c
2. a, c, b
3. b, a, c
4. b, c, a
5. c, a, b
6. c, b, a
.... and so forth. Diagonalization of the list produces the elements a, c, c which is admittedly admittedly not on the list because we have been limited to sets with no repetition of elements. But this easily remedied by listing them as well. In which case diagonalization fails to produce a unique arrangement. But most importantly because such a list grows iterativly across the row - adding the letter {d} to our parent set so that that it comtains four elements, {a, b, c, d} extends the list of possible combinations to columns that extend down a page or more. The point point being that any list of combinations of a finite set of elements will grow downward by the factorial of its growth iterativly across. Diagonalization depends on a square list at least or perhaps one with longer rows than columns. But if diagonalization is to cover every entry then the list must contain at least as many elements from left to right as it does from top to bottom. Diagonalization fails with finite sets. And therefore cannot be extended to the the simplest infinity which as Zermelo points out is only initially available by counting.