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.

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.)

Panu Raatikainen reminded me that the list is sometimes referred to as Martin Davis’ honor roll (after this FOM post).