วีดีโอ

Sure of course you can, sorry for the low volume

Yes, in theory the type never would be perfect for the job, but in practice you could introduce a paradox just as easily as this: const paradox: never = (() => { throw 0 })() Of course, one could always just use "as any" to bypass anything anyway, but at least "any" can be disabled, so I felt this recursive definition was (very) slightly more solid (or maybe all of this is just an excuse to have fun with recursions)

Fantastic vid. And working through the TypeScript examples is fun. However, you volume is too low. Please use louder volume going forward.

@@hexagonal6000 Thank you for the feedback! Yeah I was disappointed too when I noticed the volume difference after the upload... I'll do better next time I guess

It is haha, there is a video explaining it if you want: th-cam.com/video/-v6yPtM4VLA/w-d-xo.html

@@dappermink thank you 😊

I definitely will, thank you so much for the kind words it means a lot

That is because, by definition, 2+2 and 4 both reduce to the same expression: 4 = s(s(s(s(0)))) 2+2 = s(s(0))+s(s(0)) =s(s(s(0))+s(0)) =s(s(s(s(0)))+0) =s(s(s(s(0)))) That's kinda as if 2+2 were just an alias for 4 in this theory. Though I agree that's not the best example I could have chosen...

@@dappermink Thank you for kindly replying to my first comment on TH-cam. I appreciate it.

@@Aesthetycs No problem at all haha

Sorry I don't know any book about logic since I mostly studied it at uni and with wikipedia, but I suppose you can find some quite easily. Please note that type theory doesn't use classical logic but intuitionistic (or constructive) logic instead

There is this one that I used (HoTT), it introduces the basics homotopytypetheory.org/book/

Thank you! Sure, it's manim, created by 3blue1brown

I personally read Homotopy Type Theory (HoTT) but it is not only focused on type theory and since this is the only book I'm reading, I don't really know if there are better ones, sorry

Thank you so much, really! I do plan to make other videos to go further on this topic, but I have not enough free time for now to work on it so it's probably gonna take a while.

Probably not useful, but I dunno if it has been replaced sorry

Thank you so much!! Yes of course, what is provable depends of the set of axioms. I suppose you refer to the proposition "if a type has no inhabitant, then it is unprovable". What I meant by that is that if you cannot find an inhabitant of a given type, then that means you cannot prove its corresponding proposition. I was using "unprovable" as part of the metalanguage. If you want to PROVE that something is unprovable, you need to prove that it is impossible to construct any inhabitant of its corresponding type. That can sometimes be possible by allowing specific axioms, but by default Type Theory is built onto constructivism logic in which you cannot use proofs by contradiction.

@@dappermink Thanks for the response! I appreciate that clarification into both the type theory and constructivist way of thinking about it as I'm getting myself familiarized with it and getting out of my set theory comfort zone (aside: I have a personal goal of linking it up with categorical ways of thinking about these, e.g. the curry-howard-lambek "isomorphism", I've always been a sucker for redundant ways of seeing the same things I think) The intention behind the question originally was a lot less on the technical side. In other words I think it's obvious to us that what's provable depends on the set of axioms we have, but on the other hand I see a lot of people that e.g. go watch Veritasium's video on foundational mathematics, and they come out with this notion of "absolute unprovability" or even worse "math is subjective", "this proves my god and disproves your god", which I have no idea what any of those are supposed to mean. To be fair, the latter two are kind of crazy, outlier examples, but here's a take from one of my favorite mathematicians Alon Amit, criticizing even Stephen Hawking take on the Godel incompleteness theorem: "The paragraph concludes with "Thus mathematics is either inconsistent or incomplete. The smart money is on incomplete." [quote from Stephen Hawking's article] It isn't "mathematics" that is either inconsistent or incomplete. That statement is meaningless. It is certain (not all) formal systems that are used to analyze mathematical proofs which are inconsistent or incomplete." (If you want to read the rest of the article, it's Alon Amit's post on quora titled "On Hawking's "Gödel and the End of Physics" ". It's also not a one off, you'll find a lot of posts of his going into how much something like the incompleteness theorems get totally misrepresented even by people who work in heavy mathematics, maybe not necessarily foundational maths of course) So to cap this long post, basically although this is quite a lot for something that should be very simple, I think it's something that you might be interested in exploring and clarifying for people not used to thinking this way. At this point you could argue this is moreso epistemology than mathematics (but really, the lines blur, especially in foundational topics ground everything we know so far), but believe it or not a lot of us really suck at despite probably how many proofs we go through in say university. I definitely never had a class on it, I had to learn the hard way.

@@dappermink I think at this point I should offer a tl;dr, but basically, just like the other kind people who also devote their time to communicating yet another subject: quantum mechanics have to deal with, foundational mathematics sadly also attracts a lot of woo who misinterpret both communities. Otoh you might even see it as a "glass half full" thing and see opportunity there to cover something about it if you find epistemology interesting. (to me I use it as an excuse to trojan horse in my love of math, but disguise it as something else to not necessarily math people :D )

Thank you so much, this kind of support really helps motivation! Also, sure, it's planned (':

Shit, my secret identity is not that secret anymore 😢

​@@dappermink From a pie chart to a stack bar chart lol. Nice video btw, keep em coming

Thank you! I guess remaking it could be a good idea, but if I had some free time I'd rather use it to make a whole new video than just a remake : )

@@dappermink well that would be even better, although the video is pretty neat. :-)

damn you're right :(

Thank you!

Haha thanks! I don't know much about this yet since I am very new to the topic, so I wish you best of luck for your online researches if you're interested ( :

That's awesome, thank you! : )

I completely agree, thanks a lot btw!

Release bwian!

Thank you so much!

No, he's just proved that if a system can prove his own consistency, then it implies some contradiction. I'm not sure to understand what you're asking, tell me if I don't get it

@@dappermink Our English language is a system, therefore there's no way to prove what Gödel is trying to prove?

@@johndebord7802 As far as I know, he proved it into the Peano system, not English, so any system that includes Peano arithmetics is either incomplete or inconsistent (or both).