[cubefox]

The way he presents Hilbert's program in 13:34 would make it immediately incompatible with Gödel's theorems. But Hilbert's program was different from what is suggested in the video. It was concerned with proving the consistency of mathematics (or more specifically, arithmetic) using "finitary methods", and in a "conservative" manner using the notions of "real" and "ideal" mathematics. Whether Gödel's theorems show that this is impossible is not completely clear, as it is not established what should count as "finitary", and how to interpret Hilbert's conservativity requirement. See this section for an overview: https://plato.stanford.edu/entries/hilbert-program/#4

Another inaccuracy: In 8:42 he says Russell pointed out a "problem in Cantor's set theory". But Cantor's theory wasn't even axiomatized, and Russell didn't talk about Cantor's theory, but about Frege's Basic Laws of Arithmetic, which contained an inconsistency.

The thing I was pointing at (grain of salt) is basically the same as Gell-Mann amnesia[1]: Why should you trust someone in a subject you don't know anything about, when you don't overly trust him in topics where you do know something about? The trust level should arguably be the same in both subjects.

1: https://news.ycombinator.com/item?id=13155538

[Tainnor]

I think you have to be really, really charitable not to see the Second Incompleteness Theorem as a complete repudiation of the Hilbert Program - at least it destroys the possibility of proving ZFC consistent in PA - to the point that I think it's a reasonable simplification to say that the Hilbert program failed, even if the paragraph you linked shows that some people have been trying to salvage Hilbert's program by relaxing it a little. I'm aware e.g. of Gentzen's proof of the consistency of PA, but I don't find it plausible to claim that it uses "finitary methods". At the very least, I don't think such arguments would have convinced the people that Hilbert was trying to convince, such as intuitionists.

Your second point also seems like a very minor nitpick. Clearly, set theory is inconsistent if you don't impose any restrictions on what kinds of set can be formed (something that Cantor to my knowledge didn't do), which is what Russell's paradox showed. The fact that they used Frege's formalisation for setting up the paradox doesn't seem particularly relevant to me.