A couple of days ago, Daniel Litt linked to Patrick Brosnan‘s computer-verified “proof” of the inconsistency of Peano arithmetic. The proof is correct; I just put it in quotes because it relies on a quirk of the proof verification system used (Metamath), which requires you to explicitly prohibit certain variable substitutions. The axiom of PA used in the proof of \(0=1\) is \(x < y \leftrightarrow \exists z\, y = x + z’]\). Nothing wrong with that, but you can’t allow \(y\) to be substituted by \(z\) (or \(z\) to be renamed to \(y\)). The author of the original Metamath file was Robert Solovay, so this reminded me that quite a number of famous logicians proposed axiom systems that turned out to be inconsistent (although most of them didn’t just forget to prohibit an obviously illegal substitution). Here’s a partial list; let me know of additions.
First, of course there’s Frege’s basic law V, which was shown inconsistent by Russell (Russell’s paradox). The inconsistency gave us Russell’s theory of types and Whitehead & Russell’s Principia mathematica, and, much later, the neo-logicist systems of second-order arithmetic that replace Basic Law V with Hume’s principle.
An early version of the logic underlying Principia, the so-called substitutional theory, turned out to be inconsistent. Russell found the inconsistency himself; see this paper by Bernie Linsky (thanks Landon Elkind for pointing me to this).
Hilbert and Ackermann also had notorious problems with the correct formulation of their substitution rules, although their errors in successive versions of Grundzüge der theoretischen Logik made the system only unsound and not outright inconsistent (as far as I know)—see Pager’s 1960 paper and references therein.
In the early 1930s, Alonzo Church (“A set of postulates for the foundations of logic“) and Haskell Curry (“Grundlagen der kombinatorischen Logik“) proposed new logical systems for the foundations of mathematics. Both were shown to be inconsistent by Kleene and Rosser in 1935 (in the case of Curry, only the equality axioms proposed in 1934 lead to contradiction). The consistent subsystem that Church extracted is—you guessed it—the lambda calculus (see Cantini’s SEP entry for details). On the other hand, Curry’s analysis of the inconsistency gave us Curry’s paradox.
Quine’s system of New Foundations was originally introduced in his Mathematical Logic in 1940. The system as presented in the first (1940) edition allows the derivation of the Burali-Forti paradox. This was again proved by Rosser, who thus leads the scoreboard in number of systems shown inconsistent.
Rosser actually went on to use Quine’s NF in his own textbook Logic for Mathematicians, published in 1953. In his development of mathematics in NF, he discussed and used the axiom of choice. Unfortunately, that same year Specker showed that NF also disproves the axiom of choice (thanks to Martin Davis for pointing this out). In his review of Specker’s paper, Rosser suggested that a restriction of AC is all that’s needed for the results developed in his book. There, he only proposed countable choice as an axiom (Axiom 15, p. 512) which (as far as is known today) is consistent (thanks to Randall Holmes).
A version of the theory of constructions developed in the 1960s by Georg Kreisel and Nicolas Goodman was inconsistent as shown in Goodman’s 1968 dissertation (see this paper by Dean & Kurokawa).
Per Martin-Löf’s original (1971) system of constructive type theory was also inconsistent—shown by Jean-Yves Girard in his 1972 dissertation (Girard’s paradox), and this led to important developments in type theory.
Another famous example from set theory is the inconsistency of Reinhardt cardinals, proved by Kunen. This has perhaps a different flavor than the other examples: presumably (I don’t have access to Reinhardt’s thesis) he proposed the axiom (that there is a non-trivial elementary embedding of the universe into itself) originally as an object of investigation, rather than as something taken to be obviously true (as Frege took Basic Law V). (Thanks Toby Meadows and David Schrittesser for reminding me of this nevertheless. Factoid: Reinhardt is my academic uncle.)
Inconsistency is a problem in classical logic because from an inconsistency you can prove anything: thus classically, inconsistent theories are trivial. One way to get around this is to change the logic in such a way that inconsistencies by themselves don’t make the theory “explode”. Newton da Costa pioneered such logics and in the 1960s he developed paraconsistent set theories on their basis. The hope was that they would prove contradictions such as Russell’s paradox without thereby proving absolutely everything. Unfortunately, some of those nevertheless turned out to be trivial (shown in 1985 by Arruda; h/t Luis Estrada-González).
Panu Raatikainen reminded me that the list is sometimes referred to as Martin Davis’ honor roll (after this FOM post).
Thanks for this interesting topic! I have a question about what you said for Martin-Löf’s system: Did his systems lead to important developments in type theory or did Girard’s proof of the inconsistency lead to these developments? The point I’m after is if the important developments in type theory came about despite the inconsistency or because of (the proof of) it? I’m currently looking into inconsistencies that arose in logic and that were productively used in the practice despite them leading to explosion and it would be nice to get a further example for this. Thanks!
I wish I knew!
Nomenclature. Quine’s system NF (New Foundations) is introduced in his paper, New foundations for mathematical logic, included in his book From a Logical Point of View. It is … not known to be inconsistent: Randall Holmes may have proven this.
The system of his 1940 Mathematical Logic which Rosser showed inconsistent is MAYBE called ML: it stands to NF roughly as Morse-Kelly set theory stands to ZF. The second edition of Quine’s book (still in print) contains a weakened version (due to Hao Wang) which I guess is also called ML. (I think recent writers use the name ML for the second version.). Wang prove a relative consistency result for it: @nd edition ML is consistent if NF is.
NF was not first proposed in “Mathematical Logic”, it was first posted in the 1937 paper “New foundations for mathematical logic”, and that version has never been shown to be inconsistent [that is the version Rosser used, not the corrected version of the system of ML]. In fact, the core of my claimed proof that it is consistent has just been formally verified in Lean…