Wolchover is masterful here. The layers of abstraction keep piling up, and I had to read the last part more than a couple of times to really get it, but then you have it.
Just going to echo @dwohnitmok here in saying that this is a pretty 'meh' article. Understanding Godel's First Incompleteness Theorem is actually very accessible, I wrote about it a few years ago[1]. His second is much more involved and laymen won't have the required tools to grasp it. In my opinion, the easiest way to understand it is probably using Löb's Theorem, but that's neither here nor there. Either way, I'm of the opinion that arithmetic coding is very confusing and shouldn't be used to introduce people to Godel.
I'm not sure this is equivalent to Gödel's theorem. Actually, I'm not sure this is a correct proof of anything at all, merely a sort-of demonstration of Richard's paradox.
First, for reference, let me quote First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F." (from Wikipedia)
Now back to your post.
Obviously, f' is not in T and it is not computable. But neither is T. It is incomputable merely by being the list of computable functions, which we cannot construct because of halting problem and stuff like that.
And your definition of f' relies on having T. So we don't in fact have seen "statement f'". So, the direct connection between Gödel's theorem and your construct is not obvious to me, because first is about constructable, but unprovable statements, and second seems to be a faulty (i.e. mathematically uninterpretable) construct itself.
> I'm not sure this is equivalent to Gödel's theorem.
It is. In fact, I've seen it proven this way several times (mostly in CS-y papers), but it's definitely not common. My post is in fact based (almost beat-by-beat) on this UC Davis lecture: https://www.youtube.com/watch?v=9JeIG_CsgvI
Your plain and confident statement "it is" doesn't really address any of my concerns, and I just explained why, as it seems, it actually isn't.
P.S.
I did some random googling, and while I'm not sure, all this story seems to be based off of Paul Finsler's work, which he himself thought to be the priority for an incompleteness theorem (Collected Works Vol. IV., p. 9), but didn't seem so to Gödel (and, seemingly, the majority of those who had to say something about it).
If this indeed is the same thing, it would explain to me why this "proof", which doesn't seem to me like a proof at all is so widespread. But, again, I'm not sure I'm reading into it correctly, and operating under assumption that if somebody could provide something more weighty than "it is" statement, I could be persuaded otherwise.
> Your plain and confident statement "it is" doesn't really address any of my concerns...
Your concerns aren't really valid (for example, the computability of T is irrelevant). These are questions I already answered before on both HN and in the Disqus comments. Further, metalogic was my area of focus in school, so I'm quite familiar with intricacies here, and don't really feel it's useful to get too deep into the weeds. But don't take my word for it; Dr. Gusfield's paper (that the lecture is based on) can be found here: https://csiflabs.cs.ucdavis.edu/~gusfield/godelproofreviseda...
The ideas in this proof have been well-tread by Scott Aaronson, Peter Smith, and Michael Sipser. My curt "it is" is also meant to nip in the bud -- correct -- claims that it's not exactly what Godel proved (the OG variant is actually slightly stronger). Why I'd want to nip these in the bud is that in school, you technically learn the weaker variant (albeit starting with a Henkin construction of Godel's Completeness Theorem). Sort of like this[1]. But the difference between the two is so nuanced, it's not even really worth bringing up unless we're in a graduate seminar.
The article plays a little fast and loose with language
> For example, Gödel himself helped establish that the continuum hypothesis, which concerns the sizes of infinity, is undecidable, as is the halting problem
The continuum hypothesis is definitely not "undecidable" in the same way that the halting problem is undecidable. Though there are deep connections behind the two, the two notions of "undecidability" (logical independence in the former and Turing machine computability in the latter) are very different.
Also,
> He also showed that no candidate set of axioms can ever prove its own consistency.
This is powerful as a limiting result, but it has little direct impact for philosophy, because you wouldn't trust the consistency result of a system you suspect might be inconsistent to begin with because inconsistent systems can prove anything. So saying "my axioms prove themselves consistent" shouldn't have increased your trust in those axioms to begin with in the absence of the incompleteness theorems.
I'm not really a fan of "true-but-unprovable" as short-hand the incompleteness theorems, because that hinges a lot on what kind of logic system you're in and how that logic system defines "truth" (taken at face value, how do we know that Godel's incompleteness theorem is "true?").
I prefer rather to pose two questions to reflect on that I think illuminate Godel's incompleteness theorems some more. Most modern logical systems (e.g. first-order logic and its various extensions and variants) equate unproveability with logical independence. So with that in mind, here's two questions.
First, Conway's Game of Life:
Conway's Game of Life seem like they should be subject to Godel's incompleteness theorems. It is after all powerful enough to be Turing-complete.
Yet its rules seem clearly complete (they unambiguously specify how to implement the Game of Life enough that different implementation of the Game of Life agree with each other).
So what part of Game of Life is incomplete? What new rule (i.e. axiom) can you add to Conway's Game of Life that is independent of its current rules? Given that, what does it mean when I say that "its rules seem clearly complete?" Is there a way of capturing that notion? And if there isn't, why haven't different implementations of the game diverged? If you don't think that the Game of Life should be subject to Godel's Incompleteness Theorems why? Given that it's Turing complete it seems obviously as powerful as any other system.
Second, again, in most logical systems, another way of stating that consistency is unproveable is that consistency of a system S is independent of the axioms of that system. However, that means that the addition of a new axiom asserting that S is either consistent or inconsistent are both consistent with S. In particular, the new system S' that consists of the axioms of S with the new axiom "S is inconsistent" is consistent if S is consistent.
What gives? Do we have some weird "superposition" of consistency and inconsistency?
Hints (don't read them until you've given these questions some thought!):
1. Consider questions of the form "eventually" or "never." Can those be turned into axioms? If you decide instead to tackle the question of applicability of the incompleteness theorems, what is the domain of discourse when I say "clearly complete?" What exactly is under consideration?
2. Consider carefully what Godel's arithmetization of proofs gives you. What does Godel's scheme actually give you when it says it's "found" a contradiction? Does this comport with what you would normally agree with? An equivalent way of phrasing this hint, is what is the actual statement in Godel's arithmetization scheme created when we informally say "S is inconsistent?"
At the end of the day, the philosophical implications of Godel's incompleteness theorems hinge on whether you believe that it is possible to unambiguously specify what the entirety of the natural numbers are and whether they exist as a separate entity (i.e. does "infinity" exist in a real sense? Is there a truly absolute standard model of the natural numbers?).
Who cares about the philosophical implications of the theorems? Philosophers! The linked article is about how the theorems destroyed Whitehead et al's aspirations to find One Algebra To Rule Them All.
The literature on Gödel and philosophy is gargantuan, for some reason. Wasn't it summed up well by Wittgenstein? Paraphrasing: "Who cares about your contradictions?" Well said. Also not the topic Wolchover's article.
Math people can make the same move: "Who cares about your philosophizing?"
> The linked article is about how the theorems destroyed Whitehead et al's aspirations to find One Algebra To Rule Them All.
Sort of. Whitehead's contributions to universal algebra are still relevant and universal algebra is still a thriving field of study for mathematical logic. Although perhaps you mean "algebra" in a more informal sense?
Again, the conclusion of the article is a bit strong.
> Gödel’s proof killed the search for a consistent, complete mathematical system.
The consistency half doesn't make sense. (EDIT: I get it now, see the last sentence of this paragraph) There was never a search for a consistent mathematical system in the sense that Godel destroyed because again a system that can prove its own consistency has no positive value in evaluating the consistency of that system (Godel's big contribution here is contributing a strong negative result, if it could prove its own consistency you're pretty screwed). EDIT: On reflection I see that the sentence probably means to tie consistency to completeness rather than as a stand-alone quality. That makes more sense.
As for mathematicians, their reactions to Godel's incompleteness theorems overall are probably similar to "Who cares about your incompleteness theorems?" (there's a reason Russell and Whitehead are known primarily for being philosophers first and mathematicians second and why often times there is distinction between logicians like Godel and other mathematicians). Most mathematicians don't think about the foundations of mathematics because it is (perhaps surprisingly) largely irrelevant to the day-to-day work of mathematicians. Indeed the vast majority of mathematics is very resilient to changes in its underlying foundations.
To interpret Godel's incompleteness theorems requires a healthy dose of at least mathematical logic that can start veering quite close to mathematical philosophy.
An example from the article:
> However, although G is undecidable, it’s clearly true. G says, “The formula with Gödel number sub(n, n, 17) cannot be proved,” and that’s exactly what we’ve found to be the case!
Well no, that's not true in certain senses. Indeed in a larger axiomatic system subsuming the current system that corresponds to G, it is completely consistent to state that G is provable and that its statement is provable (see my example of S'), i.e. there are Godel numbers that correspond to both a proof of G and to a proof of its content. To interpret that statement that way requires certain philosophical commitments to the correspondence between a Godel number and truth, which not everyone would accept (do you accept the truth of the new axiom introduced by S'? Why then do you accept the truth of the statement "S is consistent?" and vice versa).
"In striving for a complete mathematical system, you can never catch your own tail." This on the other hand I think is a very good informal description of what's on with Godel's incompleteness theorems. Focus on the incompleteness not on truth.
That's why I'm not a fan of using the word "truth" when talking about Godel's incompleteness theorems. I am in fact deeply sympathetic to your desire to separate philosophy from Godel's incompleteness theorems.
I prefer to clearly delineate between its logical properties in mathematical logic and its philosophical implications and using the word "truth" by necessity muddles the two.
FINAL EDIT: I am being perhaps a bit too harsh on the article. I think it does a fine job of describing the arithmetization of the incompleteness theorems. But if someone else reading this also decides to create an informal guide to Godel's incompleteness theorems, please please please don't use the word "truth" and "true" or at least separate it out into its own section on philosophy.
I think it's not true in a very clear sense: you can construct semantic models of the axioms of arithmetic in which it is false. In other words, you can construct semantic models of the axioms of arithmetic (more precisely, of the axioms of arithmetic using first-order logic, which is what the article is about) in which there is a "number" that is the Godel number of a proof of the Godel sentence G! Godel's Theorem just ensures that in any such model, the "number" that is the Godel number of such a proof will not be a "standard" natural number, i.e., one that you can obtain from zero via the application of the successor operation.
So another way of viewing this whole issue of "truth" is that it is always relative to some semantic model. If your chosen semantic model of the axioms of arithmetic is the "standard" natural numbers, and only those numbers, then the Godel sentence G for that system will be true--there will indeed be no number in your model that is the Godel number of a proof of G. But if you pick instead a non-standard model that includes "numbers" other than the standard natural numbers, but still satisfies the axioms, then the Godel sentence G can be false in that model, since there can exist a "number" (just not a standard one) in that model that is the Godel number of a proof of G.
What you are saying is true (as you allude to with first-order logic) in any context in which Godel's completeness (not incompleteness) theorem holds. Not all logics have versions of Godel's completeness theorem (e.g. second order logic with full semantics). You can argue that philosophically in systems where Godel's completeness theorem fails that the article's statement is valid. But yes that's why it's only true in "certain senses."
More generally the philosophical question of truth revolves around whether there is a single, true set of standard natural numbers that corresponds to reality, and therefore all nonstandard natural numbers are "artificial" in some sense, or whether even standard natural numbers exist only in a relative sense.
You seem like somebody who I could ask some (2) questions on the topic.
1. First of, I'm still not sure what to make of Gödel's theorems philosophically. In the "pop-culture", so to speak, there seems to be a notion that Gödel's theorems are, in essence, some grand, weighty statement about fundamental "inaccessibility of truth". That since Peano's arithmetic exemplifies very simple (compared to our general needs) mathematical system, no matter how we further develop math, one day there will be a useful, meaningful statement which cannot be proved or disproved.
What's perhaps even worse, some people, even some with names I feel uncomfortable to argue against (Penrose, for example, seems to be of this opinion) try to use it as a transition to the idea that "human mind is more than a computer", which I always implicitly assumed to be just a manifestation of anthropocentric hubris. The key to their reasoning is the observation, that some expressions unprovable within some formal system are "obviously true" (and they often kinda are, and they are provable within a higher-order formal system). So, the story goes, since the Turing machine couldn't see it (because of Gödel's), but we see it, we are more than a Turing machine.
And since that informal version of Gödel's findings was familiar to me long before I was acquainted with a formal version of it, I'm kinda used to the idea that "it must be right".
However, when I'm looking at the formal explanation of Gödel's theorems, or even perhaps more interesting "applied" findings, based on them (like Goodstein's theorem), they all seem to be surprisingly "boring" and non-consequential clever tricks based on self-referencing. I mean, it's sure a very interesting finding about formal systems as such, but if we take a step back into the realms of common sense: isn't it rather quite intuitive, that a system cannot be proven to be consistent by the means of the same system? So it must be of no surprise that any formal system powerful enough to be able to express statements about consistency of itself must be "incomplete".
So, my question is, am I missing something? Is there any truth to that pop-cultural image of Gödel's theorems? Because to me it seems like there actually isn't, just more of an "urban myth".
2. Continuum hypothesis. As I understand it, it is a matter of axiom, if 2^Aleph₀ ?= Aleph₁ and |R| could be as well Aleph₅ or whatever. Of course, we have most natural axiomatic system (with axiom of determinacy) where the former is true. But are there, like it was with Euclid's fifth postulate, any alternative, but still "interesting" constructs? Is there any use whatsoever in the assertion that continuum hypothesis is false?
I'll give brief statements with lots of hand-waving since I'm low on time. These are long questions.
1. In short, this is a deeply philosophical question. My personal inclination follows yours that the incompleteness theorems are overhyped. I don't buy Penrose's argument. Like most other formal limiting results philosophically I view those results as representing fundamental limits of both human and machine reasoning. While a single unproveable but "obviously true" result generally point to an inadequacy of the formal system, if every formal system suffers from some inadequacy that is indicative of a limitation in the fundamental human faculties of comprehension rather than a limitation of formal systems per se (the assumption e.g. that our formal systems must use finitistic methods is one born of human limitations and, depending on one's thoughts about the universe, potentially fundamental physical ones).
There are philosophically defensible positions that try to claim the incompleteness theorems have implications for truth in the real world, but I go back and forth on whether I believe them and more to the point they are far more subtle than the usual pop culture presentations of Godel's incompleteness theorems.
2. The mathematical Platonists I've come across believe that the continuum hypothesis is in fact false. (As an aside it's interesting that you find the axiom of determinacy natural as it contradicts the axiom of choice.) This mainly hinges on your opinion of the reality of large cardinals (which perhaps count as your "interesting" constructs), which many Platonists for a variety of reasons believe to be real.
Don't read this without thinking about the questions first!
I tried to be short... there's a considerable amount of handwaving. I'll present two components to each of my answers. One that stays within mathematical logic and then one that expands a bit into philosophy.
1. Strictly mathematical logic: Godel's incompleteness theorems can be viewed as a limiting result on the absoluteness of mathematical induction (this is not strictly true, in fact we lose even more than absoluteness of induction, see e.g. Robinson's Q, but I'll leave that aside for now). Conway's Game of Life rules are complete in the context of a single step. That is for any step n, Conway's Game of Life rules completely determine step n + 1. The assumption that given a fixed starting state, this means that Conway's Game of Life is completely determined for all steps is exactly a statement of mathematical induction. In particular, we are piggy-backing off of the induction axiom of Peano arithmetic here. That's where Godel's incompleteness theorems get you.
One way of thinking about Godel's incompleteness theorems is that they attack the assumption that because we have defined every step transition we have defined the whole process. Hence certain "global" statements about potentially unbounded processes remain up in the air. Even if we rule by fiat with an induction axiom (or axiom schema) that this must be true, some ambiguity remains. "After a certain point once this square turns white it never turns black again" or "this square will never turn white" are both statements that are independent of Conway's Game of Life rules for certain squares and starting configurations.
Now this ambiguity is not observable because while we have ambiguity for unbounded questions, as soon as we place any bound, no matter how large the n (e.g. for the next 1000000 steps this square will not turn black), there is no ambiguity. Incompleteness hinges essentially on the ability to make unbounded statements which involve the words "eventually," "always," "never," etc.
Now the philosophical implications of this are interesting. This question is why I'm skeptical of naive attempts to talk about the incompleteness theorems' consequences for physical theories of the universe. Intuitively I view physicists as trying to find the "Game of Life" rules for the universe, and that if they did, that would be as good a candidate as any for a "theory of everything." In particular these rules would be local and finite, rather than global, infinite statements of the sort I outlined above. If you're willing to accept Conway's Game of Life as being complete enough for your purposes, I would argue you should accept a similar "theory of everything" as being "complete enough."
Now there's no reason why Mother Nature must be kind enough to furnish us with such a theory, but that's a different story.
Another interesting philosophical component here is whether this implies Godel's incompleteness theorems have any meaningful physical manifestation. I don't have the time at the moment to get into that discussion, but suffice it to say I generally think that these discussions usually go off the rails really really quickly without a deep understanding of the incompleteness theorems rather than informal overviews of them. In the philosophical context of Conway's Game of Life, you'd expect to find deviations in different implementations of the the rules "after an infinite amount of steps have passed." Whether you find that a coherent statement or not has implications for the applicability of Godel's incompleteness theorems to the physical universe.
EDIT: To tie this to the hints I gave, unbounded statements involving words like "eventually" or "never" are precisely those statements that can be independent of the "axioms" of the Game of Life. When we talk about the completeness of the Game of Life we are talking about it only at a per-step level.
2. Godel's incompleteness theorems are ultimately statements about natural numbers, or at least what the current logical system in question thinks is a natural number. The interpretation that this natural number represents some logical statement is a metalogical one and unjustified within the logical system itself. We can only make this interpretation as an outside observer. So S' produces a "number" according to the algorithm we use to represent the statement of inconsistency of S. However, within S' this is just a number. It doesn't know how to turn that number into a logical contradiction that it can then produce and use to prove things. As an outside observer then we are either free to agree with S' that indeed yes what you've produced is a number and then use that number to deduce the inconsistency of S or we can disagree with S' that this number represents an inconsistency of S (informally, you can imagine that S' is "hallucinating" a number that while might be a natural number according to the axioms of S', is not a natural number according to ours as an outside observer).
If we have a notion of what the "true" natural numbers are, as opposed to natural numbers are "hallucinated," we can talk about whether S' is right about the consistency of S. The assumption that S' is not "hallucinating" natural numbers is known as omega-consistency (https://en.wikipedia.org/wiki/%CE%A9-consistent_theory). Whether "true" natural numbers exist... well that brings me to the philosophical ramifications.
If you believe that there is one true set of natural numbers then it's easy to dismiss S' as a trick, useful for proofs and exploration, but ultimately simply an interesting tool rather than reflective of reality. If you believe that there is no such thing as "one true set of natural numbers" then consistency is simply a relative statement.
EDIT: To tie this to the hints I gave, Godel's arithmetization scheme only gives you numbers. It's up to you the reader to interpret those as proofs and logical statements. Within certain bounds, you are free to disagree that in your interpretation that this number represents a valid proof (or in equivalent phrasing that this "number" is truly a number).
May I suggest that "true" in "true-but-unprovable" means from God's eye or in a higher level system but not in current system because "unprovable"（in current system only) means it's not really true in current system? Correct me if I'm wrong in this context.
You are wrong. Godel in fact showed precisely that there are unprovable statements in any consistent set of axioms. In fact it’s equivalent. The only systems in which every statement is provable are inconsistent. Consistent here meaning that statements cannot be proven to be both true and false from axioms.
There are two other conditions/premises that, arguably, play a bigger role in Gödel's theorems:
1. The theory must be strong enough to do a certain amount of arithmetic
2. The axioms of the theory must be computably enumerable
So, you can have relatively weak theories in which the incompleteness results don't hold. A major example here is comes from Gödel's _completeness_ theorem (notice "completeness" not "INcompleteness") which says: in first-order logic a statement is true if and only if its provable.
You can also have strong theories whose axioms are not computably enumerable. Start with something like the Peano axioms and consider the set of all true statements in that theory. We can take any set we want as axioms, so what if we take the set of all true statements in Peano arithmetic as our axioms?
Now every valid "proof" is one line long since what was previous a theorem is now an axiom, but we've kicked the can down the road. How do we figure out whether something is an axiom in this new system or not?
This latter system is called "true arithmetic" Gödel's incompleteness theorems don't apply there, either.
Godel's completeness theorem is not in opposition to his incompleteness theorems.
Godel's incompleteness theorems and completeness theorem can hold at the same time. They talk about two separate notions of completeness (the former about incompleteness in the sense of logical independence and the latter in the sense of the correspondence between semantics and syntax). Indeed Godel's incompleteness theorem is usually presented in the context of first-order Peano arithmetic.
This is again why I don't like talking about "truth." It is not completely inaccurate to say Godel's completeness theorem says "a statement is true if and only if it's provable." It is also not completely inaccurate to say Godel's incompleteness theorems say "some true statements are not provable." But the vagaries and philosophical baggage behind the two statements mean you have to tread _very_ carefully and without _extremely_ careful qualifications you can start making philosophical statements that are extrapolations of those theorems rather than the theorems themselves. That's why I strongly believe that it's much much much more productive to talk about incompleteness and consistency rather than truth.
I'm not contradictory to your statement. Or your explanation hasn't touch my potential flaw if exists. Let me put in this way:
There is at least some "thing" that can not be proved without cause inconsistency. To avoid the inconsistency to prove the "thing" which become true we need to create a high order system in which then the "thing" is truth but also cause the same dilemma in the new bigger system that new "thing" will show up that need another high order system. So it's correct that no system can contain all truth while keeping consistent. This is the point you want to express in your statement, right? (Actually it's Godel theorem in plain English itself)
What I try to say is: if its not provable in current system so it can not be called true within current system. I could be wrong at this part but not what you tried to explain which I already agree.
This isn’t quite right, though perhaps a nit, plenty of formal systems are provably sound (only true things are provable) and complete (all true things are provable). For example, the predicate calculus you learn in Logic 101. Formal systems become provably incomplete when they are able to express arithmetic (e.g., Peano axioms).
Yes, that Scott Aaronson paper was an eye opener for me.
It wasn't because of the correspondence between Godel's theorems and the halting problem, although for a computer programmer Aaronson's formulation turns Godel's inscrutable theorem into something easily accessible. (Oh, and for the curious, the reason Godel's theorem is so hard to understand is he needed a computer programming language for his proof but there were none lying around back then, so he invented his own. I strongly suspect he wasn't thinking of it as a series of executable steps, let alone a programming language whose most important property is to be readable. As a consequence it's bloody terrible.)
No, it was because it Aaronson made it plain both the halting problem and Godel's theorem are really statements about the difficulty of reasoning about infinities. The infinities are really well hidden in both approaches, but once you uncover them it's like seeing the elephant in the room - it all becomes obvious. And it also becomes evident they aren't particularly relevant to anything you are likely to encounter here on earth. That's because there are no infinities in our corner of the universe. And, there there is no halting problem for finite, bounded systems. For some reason, no one ever tells you that.
This paper, listed here on HN recently, explains it much better than I can:
A Couple of comments here on "this isn't an introduction, its a book!!", for anyone who checked here first, that is the title of the book, and while I can't speak to Smith's coverage, if you're going to "introduce" someone to the incompleteness theorems, a book is how you're going to do it. They're two of the most significant theorems in modern mathematics, maybe all of mathematics. Logicomix is fine, but I'm not pushing anyone to actually learn these theorems through a graphic novel or a blogpost.
As far as book alternatives, an interesting and useful way to get your head around what Godel was doing is to try to read Gottlob Frege, his notation isn't that hard to parse, and it marks the origin point of modern mathematical logic and the attempt to do that which Godel proved impossible.
Foundations of Arithmetic is easily readable with only a slight amount of contextualization for someone with a high school level mathematical education.
I found this super helpful when I was studying Gödel's theorems in grad school. (Fwiw, the 3rd edition of Boolos & Jeffrey's Computability and Logic is also great and takes a somewhat atypical approach to the proofs.)
I can recommend Peter Smith as an author; I was part of a small reading group with him while we were all getting to grips with Cambridge's Part III Introduction to Category Theory, and he's definitely good at identifying the difficult bits and breaking them down.
It's a book! I was expecting a short paper along the lines of [0] or [1] but this is going to take a while to evaluate. Nonetheless I like the surface-level presentation and it seems like the author takes the time to carefully explain each concept in detail.
I need to learn more about Godel and read the books about him. From the outside, he almost seems like an intellectual rebel, showing how systems are broken when people assume they aren't. With his completeness theorems and his Godel metric, he seemed to be excited by logical exotica. I find the Godel metric and its closed timelike curves to be an interesting case study of general relativity. This is just me spitballing here, as I have not yet dove into the many books I have on him.
It's more or less explained in 1.2. A system is "sound" if it's consistent AND can only prove true things.
To see the difference between sound and consistent, suppose you have a formal system A which you know is sound. You can then (by Godel's construction) make a proposition G that says A can't prove or disprove G. We know that G is true because A can't in fact prove or disprove G, by construction.
Make a new formal system by taking the axioms of A and adding the negation of G, that is, B=A+not(G). B is consistent but not sound. It's consistent because A can't prove G, so adding not(G) as an axiom can't possibly lead to a contradiction. And it's not sound because it can prove a falsehood, namely not(G) (granted, it's a very easy proof, since it's an axiom).
Scott Aaronson calls systems like B "self-hating" [1], because they "believe" they're not consistent (even though they are).
Wolchover is masterful here. The layers of abstraction keep piling up, and I had to read the last part more than a couple of times to really get it, but then you have it.