There are two things I will argue with on this otherwise great explanation.
First, I've said this before and I'll bang this drum across every Godel post I see. Please don't introduce the notion of truth into an introductory post on Godel's Incompleteness Theorems (the Power of Numbers section). Introductory posts on Godel's Incompleteness Theorems like to say things like "there are true things you cannot prove" or in the case of this post "there are some truths that you can never write down as an algorithm." This is very nuanced and depends very heavily on what logical system you're in.
To demonstrate how subtle this point is, there is also Godel's Completeness Theorem, which can informally be summarized as "all true statement are provable," and holds for most logical systems that mathematicians use, including those to which Godel's Incompleteness Theorems apply. The subtle point of course here is that "true" means something different in both contexts.
This leads to the classic overly strong philosophical statements such as "For example, it may mean that we can’t write an algorithm that can think like a dog." That may be true, but it's not a direct consequence of Godel's Incompleteness Theorems.
That's why in an introduction I strongly strongly recommend just sticking to incompleteness, i.e. the fact that you cannot have an exhaustive list of axioms. There will always be new axioms you can add.
The second drum that I will keep banging on is that articles talking about how Godel's Incompleteness Theorems show that a system S cannot prove its own consistency and stop there miss the significance of this statement. Usually, like in this article, they go in the "opposite" direction by saying S can't prove itself, so maybe you could try using a more powerful S' to prove S, but then you couldn't prove S', and so you need an S'' to prove the consistency of S', and so on and so forth in an infinite regress. But we actually care about the opposite direction: using S to prove the consistency of S' and then using S' to prove the consistency of S'' and so on.
That is we don't actually care about using S to prove its own consistency because if we were ever doubtful of S's consistency, we wouldn't trust any proof it produced, let alone a proof of its own consistency.
Rather what is important is that we cannot prove the consistency of the stronger S' in the weaker S, since if we were able to prove the consistency of S', then we could definitely prove the consistency of the weaker S. This is the fatal blow to Hilbert's program. Hilbert was perfectly fine with having to assume the consistency of some logical system. His hope was something akin to a "trusted computing base" that if you assumed was consistent could then prove the consistency of all other more complex systems. Ideally this "trusted computing base" could be quite small, but it wouldn't necessarily have to be, as long as there was some definite size after which we could stop having to take consistency on faith.
Godel's consistency result implies that this trusted computing base cannot exist! There is no minimal base whose consistency, when taken on faith, is enough to prove the consistency of other systems we care about. That is we care about the opposite direction: S can't prove the consistency of S, so it can't prove the consistency of the larger S', so it can't prove the consistency of the still larger S'', and so on.
Now again there's some nuance here. We know that Con(S) is independent of S and in turn Con(S + Con(S)) is independent of S + Con(S) etc. but we also somehow know how to "collapse" this whole hierarchy if we know that S is consistent (the formalization of this intuition requires a deeper dive into model theory), so something is a little bit off here. Moreover stuff like Gentzen's proof of the consistency Peano Arithmetic demonstrate there is some more wiggle room in exactly what it means for a system to be logically stronger than another system.
But the most straightforward, naive way of trying to use a single trusted computing base to prove the consistency of everything else will fail.
1: Model theory, which formalizes "truth", is very
important for understanding inferential
incompleteness. Axioms of foundational theories of
Computer Science have just *one* model up to a unique
isomorphism, which defines "truth".
The theorems of foundational theories of Computer
Science are *not* computationally enumerable.
Consequently, even the provable proposition's
*cannot* be computationally enumerated, much less the
ones true in the unique model.
2. Foundational theories of Computer Science can prove
their own consistency because they *disallow* the
[Gödel 1931] proposition *I'mUnprovable*, which if it
were allowed would make the theories inconsistent.
First, I've said this before and I'll bang this drum across every Godel post I see. Please don't introduce the notion of truth into an introductory post on Godel's Incompleteness Theorems (the Power of Numbers section). Introductory posts on Godel's Incompleteness Theorems like to say things like "there are true things you cannot prove" or in the case of this post "there are some truths that you can never write down as an algorithm." This is very nuanced and depends very heavily on what logical system you're in.
To demonstrate how subtle this point is, there is also Godel's Completeness Theorem, which can informally be summarized as "all true statement are provable," and holds for most logical systems that mathematicians use, including those to which Godel's Incompleteness Theorems apply. The subtle point of course here is that "true" means something different in both contexts.
This leads to the classic overly strong philosophical statements such as "For example, it may mean that we can’t write an algorithm that can think like a dog." That may be true, but it's not a direct consequence of Godel's Incompleteness Theorems.
That's why in an introduction I strongly strongly recommend just sticking to incompleteness, i.e. the fact that you cannot have an exhaustive list of axioms. There will always be new axioms you can add.
The second drum that I will keep banging on is that articles talking about how Godel's Incompleteness Theorems show that a system S cannot prove its own consistency and stop there miss the significance of this statement. Usually, like in this article, they go in the "opposite" direction by saying S can't prove itself, so maybe you could try using a more powerful S' to prove S, but then you couldn't prove S', and so you need an S'' to prove the consistency of S', and so on and so forth in an infinite regress. But we actually care about the opposite direction: using S to prove the consistency of S' and then using S' to prove the consistency of S'' and so on.
That is we don't actually care about using S to prove its own consistency because if we were ever doubtful of S's consistency, we wouldn't trust any proof it produced, let alone a proof of its own consistency.
Rather what is important is that we cannot prove the consistency of the stronger S' in the weaker S, since if we were able to prove the consistency of S', then we could definitely prove the consistency of the weaker S. This is the fatal blow to Hilbert's program. Hilbert was perfectly fine with having to assume the consistency of some logical system. His hope was something akin to a "trusted computing base" that if you assumed was consistent could then prove the consistency of all other more complex systems. Ideally this "trusted computing base" could be quite small, but it wouldn't necessarily have to be, as long as there was some definite size after which we could stop having to take consistency on faith.
Godel's consistency result implies that this trusted computing base cannot exist! There is no minimal base whose consistency, when taken on faith, is enough to prove the consistency of other systems we care about. That is we care about the opposite direction: S can't prove the consistency of S, so it can't prove the consistency of the larger S', so it can't prove the consistency of the still larger S'', and so on.
Now again there's some nuance here. We know that Con(S) is independent of S and in turn Con(S + Con(S)) is independent of S + Con(S) etc. but we also somehow know how to "collapse" this whole hierarchy if we know that S is consistent (the formalization of this intuition requires a deeper dive into model theory), so something is a little bit off here. Moreover stuff like Gentzen's proof of the consistency Peano Arithmetic demonstrate there is some more wiggle room in exactly what it means for a system to be logically stronger than another system.
But the most straightforward, naive way of trying to use a single trusted computing base to prove the consistency of everything else will fail.