Here is one recent and seemingly expert appreciation on the consequences of Gödel’s incompleteness theorem for mathematics:

Gödel’s incompleteness theorem showed that it is impossible to achieve absolute rigor in standard mathematics because we can never prove that mathematics is consistent (free from contradictions). (...) However, real mathematical systems have very few axioms, and these can be carefully studied. — Norman Megill, Metamath, A Computer Language for Mathematical Proofs (2019)

Metamath is a repository of computer-verified theorems, an activity which arguably belongs to computer sciences, but I assume that contributors to metamath are essentially mathematicians, and also mostly not philosophers.

See https://en.wikipedia.org/wiki/Metamath for details.

Given this, is Norman Megill's view compatible with, or perhaps even typical of, what philosophers say about the consequences of Gödel's incompleteness theorem for mathematics.

  • 3
    It is a bit sloppy, but he basically states a platitude. Philosophers would rather say something like "certainty" instead of "rigor" (that usually just means being formalizable regardless of consistency of the formalism), and specify that "can never prove" is by what Hilbert called "finitary means" and concerns the more advanced mathematics. Some elementary fragments, like Boolean algebra or Euclidean geometry, have been proved consistent by finitary means. By stronger means, one can even prove consistency of arithmetic or ZFC
    – Conifold
    Aug 19, 2022 at 12:10
  • Not exact if read at face value: a system like formal arithmetic cannot prove its own consistency, but the consistency can be proved in a different system, with different axioms/rules. Conclusion (obvious, as per Conifold's comment): we have to start sonewhere. IMO the consistency of natural numbers system is a good starting point. Aug 19, 2022 at 12:17
  • Theoretical computer science is essentially a branch of mathematical logic. Rebel against the tyranny of discontinuity.
    – J D
    Aug 19, 2022 at 14:54
  • 1
    It's like everyone wants to survive but can never rigorously prove so in any future... What specific argument do you think philosophers are in disagreement with your above quote? In fact Gödel’s own logic inspiration and interest was learned from philosophers such as Schlick and Carnap, perhaps including his famous fixed point lemma leading to his incompleteness theorems... Aug 19, 2022 at 22:28
  • 1
    I hope it's not typical, because it is incorrect. Goedel's theorm in no way prevents proving a system of logic is free of contradictions. If a statement is unprovable in line with the theorm, then it is not a contradiction, since it is not provable to be true or false.
    – BillOnne
    Aug 20, 2022 at 1:43

2 Answers 2


Part of ths relies on interpretation.

Your quote uses the expression, "standard mathematics." Given that section 74 of Kleene's "Introduction to Metamathematics" explicitly describes a difference betwen "informal mathematics" and "formal systems," what is meant by "standard mathematics"?

A similar distinction is found in one of Tarski's papers where he differentiates between actual systems which ought to be studied individually and the commonalities he intends to address. This may be compared to Aristotle's distinction between theses and axioms needed by all.

Megill's statement is certainly acceptable. But, has the case been made for a reduction of mathematics to the linguistic analysis attached to signatures from universal algebra? The first incompleteness theorem is slightly wider than formal systems, as they had not been fully developed. It used formalisms related to "Principia Mathematica" to address a metamathematical approach suggested by Hilbert. But the question of the reduction is still basically correct.

When one admits that the word "mathematics" is inherently vague, it becomes easier to see how statements like the one you quote deserve a great deal of scrutiny.

Philosophers do not teach mathematics in the same way as mathematicians in mathematics departments.


These days, it is unlikely that any algebraist does not use category theory. Thanks to the work of William Lawvere (on the shoulders of Grothendieck, MacLane and Eilenberg) category theorists make claims about "what mathematics is" that are quite different from what first-order logicians claim.

In May, a simple question about Bourbaki re-ignited a recurring argument on the FOM mailing list. At one point the category theorist, Colin McLarty chimed in because of a historical statement about MacLane's book, "Categories for the Working Mathematician." His statement is in the link,


Harvey Friedman, a strongly committed set theorist, responded by declaring that category-theoretic had no intellectually significant basis,


Harvey Friedman collects his paycheck in the mathematics department of Ohio State University. While it is true that Colin McLarty is in a philosophy department, Saunders MacLane had been in the mathematics department of my alma mater, the University of Chicago. The teaching of category theory is not some arcane "non-standard" mathematics.

And disagreements like these are not uncommon.

One often hears that set theory is the "foundation" of mathematics. That is true, perhaps, for logicists. However, Skolem's criticism showing that Zermelo's set theory cannot be categorical moves "foundations" to the language signatures of universal algebra. Chang and Kiesler describe (first-order) model theory as "universal algebra + logic." With the development of stability theory, a more modern summary from Wilfred Hodges summarizes (first-order) model theory as "algebraic geometry + logic."

The common theme here, then, is the "algebraization" of mathematics. And, Goedel's theorems are easily adapted to this in relation to universal algebra. To address "completed infinities" Hilbert distinguished between syntactic methods based upon the "sensible impressions of symbols on a page" and what can be studied through formal axiomatics. When structural induction is used to delineate the well-formed formulas of a formal language, the singular notion of a "language" presupposes a completed infinity. The structural induction, however means that any spelling of a well-formed formula can be recursively verified. Goedel's theorems depend upon these inductive relations.

Extension of the first theorem to a more general context involves understanding that axiomatic statements can sometimes be recursively verified as axioms. Thiis is why Zermelo-Fraenkel set theory and Peano arithmetic can have infinitely many axioms given through schemas. Importantly (because forcing can be justified on this basis), only finitely many axioms are assumed within any given derivation.

Goedel's theorems are often portrayed as differentiating provability from truth. Proofs, after all can be seen as lists of formulas. Arithmetization of formulas can be extended to lists of formulas. So this is how the theorem may speak of a truth from the standard model which cannot be proven.

Yet, notice that this is all based upon a characterization of mathematics reducing mathematics to linguistic forms. Following Paul Halmos, any algebraic logician will concede the validity of Goedel's theorems when applied to syntactic forms.

Is mathematics "just words"? Mark Steiner wrote a book on the applicability of mathematics. If mathematics is "just words" then what are applications? While they will deny any tangible relationship, set theorists use the word "belief" to compare "truths" between models of set theory. In his book, "Retreat to Commitment," Bartley outlines how the kind of foundationalism found wth the first-order paradigm has undermined "science." If mathematics is "just words," then applied mathematics are "just beliefs."

Steiner asked, by way of a conclusion, if applications of mathematics did not suggest a form of Pythagoreanism.

Among what others call "non-standard" mathematics, you will find homotopy type theory which makes an appeal to authority against Martin-Lof type theory. When Andriej Bauer and Steve Awodey could not engage significant consideration for this "new foundation" on the FOM mailing list they made very public "resignations" from the list. During this time, I discovered that Martin-Lof type theory advocates "verificationalism," thereby sidestepping the kind of distinction found in Goedel's arguments which had been so disconcerting. More precisly, proofs verify. So, the issues involving truth associated with Goedel's theorems need not actually be mathematical in nature.

Given "truth values" (or subobject classifiers) one can study "logic" without actually concerning one's self with truth.

When any mathematically-inclined person discounts these debates as "philosophy" or "history," they are engaging in rhetoric meant to avoid the hard questions which must creep in from philosophy. Because of the "wow factors" attached to information technology, "standard mathematics" thirty years from now may be quite different from the "standard mathematics" I learned thirty years ago. I had been at the University of Illinois as an entering graduate student (never completed because of an illness) when they started teaching calculus using Wolfram's Mathematica. And, there are already courses being taught with the proof assistant Lean.

The development of proof assistants had been a stated goal of the Fields medalist Veodovsky in his promotion of homotopy type theory. Again, these developments are a part of standard mathematics being put into standard curricula.

I know what I know because I have studied a single mathematics problem for 37 years. Yes, I am an autodidact -- or crank if that is the manner of your thinking. But, I am on record in this forum as advising any student of mathematics to avoid "foundations." They should like what they like and believe what they believe without concern for "what mathematics is." Such advice is not typical of a crank. To the contrary, I have found the study of a difficult problem to be entirely humbling.

I will consider the time I have spent with this narrative as successful if it has led you to reconsider your assumption on the meaningfulness of the expression "standard mathematics." All I have found is a diversity of opinions which cannot be reconciled.

  • "standard mathematics" I was hoping that this was clear to everybody. I would say the sort of mathematics most mathematicians do, presumably meaning mathematics following or based on FOL? It seems to me Gödel was in that particular side of the aisle. Aug 19, 2022 at 16:30
  • 1
    Shurangama sutra hinted: He seems to have obtained something, but he cannot use it...His hands and feet are intact, his seeing and hearing are not distorted, and yet his mind has come under a deviant influence, so that he is unable to move...then a demon of memory will enter his mind. Day and night it will hold his mind suspended in one place...Once the problem of paralysis subsides, his mind can then leave his body and look back upon his face. It can go or stay as it pleases...This person can then transcend the turbidity of views... Aug 20, 2022 at 4:51
  • @mls "a diversity of opinions which cannot be reconciled" Yes, but this is public knowledge, and diversity of opinion does not imply no standard. It just means some or many people will not regard it as their standard. Maybe a more informative word is "mainstream"? Thanks for these precisions, though. Aug 20, 2022 at 10:46
  • +1 Theoretical CS is not a branch of mathematical logic. Mathematical logic is a branch of CS. Arguably, theories of physical computation subsume all branches of computation, and mathematical logic isn't special. ; ) Ignaz Semmelweis was accused of being a crank. Sometimes history vindicates the oustsider.
    – J D
    Feb 17 at 1:18

The very first axiomatic system is Euclidean geometry. With the advent of formal mathematical logic in the early 20th C, Tarski formalised a substantial fraction into first order logic with a single primitive notion, point, and without any set theory. In some ways it went beyond what Euclid did because, for example, he also formalised the property of betweeness, which is, as Pasch pointed out, not proveable in Euclidean geometry.

Tarski was able to prove that Euclidean geometry, formalised as he had done, was:

  • complete : every sentence can be proved to be true or false.

  • consistent : it was not possible to both prove some sentence and its negation.

  • decidable : there is an algorithm that can decide any sentence true or false.

This underlines Megill's point.

However, the fetishisation of axiomatic thinking as being thought that characterises mathematics is simply wrong. And hence also the thought that Godel's theorem somehow prevents the achievement of "absolute rigor". That might have been the agenda of certain mathematicians at certain times, and might have been talked and hyped up by some philosophers who craved "absolute rigor" and thought that mathematics may achieve this. One way that this is stated is that once a theorem is proven, it is true for all time and maybe even outside of time. That sounds rather remarkable and grand with the invocation of eternity and truth. But this doesn't stop whole theories going out of fashion or becoming irrelevant. For example, algebraic geometry based on valuations after the advent of Grothendiecks schemes.

A case in point, physics is inconsistent, even today after four hundred years of development from Galileo. This is acknowledged by everyone, the major inconsistency being between GR & QM. Yet despite its inconsistency, it has achieved great things. More broadly, rational thinking in every day life is often inconsistent and yet the life of the species, species-life, has gone on from strength to strength. Thus inconsistency is no barrier to achievement.

Mathematics is, like all fields and practises, a living and organic expression of the thought and acts of men and women. Absolute rigor, as I have pointed out briefly above, was never its point, but to achieve clarity of thought and expression. A trait that it shares with other fields of human endeavour.

Moreover, there is such a thing as paraconsistent logic where the charge of inconsistency does not explode into triviality - the inconsistency is contained. Whilst what is called classical logic is not paraconsistent, it seems the actual classical thinkers were ahead of us here as Aristotelian logic is paraconsistent. So what Goedel's theorem might be telling us is that we are simply using the wrong underlying logic ...!


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .