I am amateur in the field of mathematical logic, so sorry for any confusing parts of this question.

It is well known that Gödel's incompleteness theorem shows there are great limits to what first-order logic can do. Is it possible to base our formal reasoning in some other system (different kind of logic, Type theory(?), something based on category theory) in such a way that Gödel's incompleteness theorem doesn't apply?

Has anyone tried to invent whole new system as foundation of mathematics to prevent this? Maybe one not based on formulae and proofs, but on something entirely different?

  • 3
    Inifnitary logic is free from Gödel's theorems. Actually, that's because infinitary logic is not recursive.
    – rus9384
    Commented Apr 29, 2018 at 16:38
  • 2
    You'll need tighter constraints than "reasoning in some other system in such a way that Gödel's incompleteness theorem doesn't apply" to make the question interesting. It explicitly applies to theories that are first order, subsume Peano arithmetic, recursively axiomatizable and consistent, any of the above can be, and have been, dropped but not without a cost. Complete paraconsistent arithmetics exist for example, Tarski's elementary geometry is complete, etc.
    – Conifold
    Commented Apr 29, 2018 at 20:12
  • 1
    If you are also interested in proofs of consistency, you may like to know that it is possible to prove the consistency of arithmetic using relevance logic. To be more precise, if you create relevant arithmetic by adding the Peano axioms to relevance logic, this arithmetic is provably absolutely consistent using finitary methods. Relevance logic is weaker than classical, so relevant arithmetic does not contain all the theorems of classical arithmetic. See Meyer and Friedman, 1992, “Whither Relevant Arithmetic?,” The Journal of Symbolic Logic, 57: 824–831.
    – Bumble
    Commented May 1, 2018 at 7:29
  • Clearly you misunderstood Godel's incompleteness theorems, almost certainly because the popular account you read is incorrect or misleading. Godel's original result was for a classical first-order theory of arithmetic, but the generalized incompleteness theorems hold for any reasonable foundational system for mathematics, even those that have not yet been conceived. As stated in the linked post, it is false that it applies to only FOL, or only deductive systems involving conventional formulae.
    – user21820
    Commented Jun 7, 2021 at 8:06
  • In particular, no matter what kind of exotic foundational system you have, if it has a proof verifier program and can reason about programs, then it is inconsistent (proves contradictory claims about programs) or incomplete (fails to prove that P halts on X, for some program P that really halts on input X). The conditions are satisfied by any reasonable foundational system S, because for S to be usable in the first place it must have a proof verifier program, and if S cannot even reason about finite program execution then it is too weak to be foundational.
    – user21820
    Commented Jun 7, 2021 at 8:12

2 Answers 2


There are a large number of ways to sidestep Gödel's proof. The question is whether those systems have sufficient practical value to mathematics to be used for any purpose other than sidestepping his proof.

My personal favorite solution is Dan Willard's work: Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles.. In it, he created a system which could prove all of its own true statements and contained all truths of arithmetic (i.e. Peano Arithmetic), but he did not define multiplication to be total. This was just powerful enough (weak enough?) to refuse to admit the diagonalization required for Gödel's proof.

Apparently it had an interesting quirk, that one could construct a countable infinity in a system, and then construct such a self-referential system within it such that that particular infinity was provably uncountable within the self-referential "Willard world," but provably countable within the larger system. I've had fun playing with the philosophical implications that one could draw from that.

  • 2
    "All of its own statements"??? Wouldn't negation of a statement also be a statement? Do you mean that it has no undecidable statements because it is too weak to contain all of Peano arithmetic or violates some other of Godel's assumptions (which one?).
    – Conifold
    Commented May 1, 2018 at 0:38
  • 2
    @Conifold Good catch. I missed the word "true." Edited to say it proves all of its true statements. It contains all of Peano arithmetic except that it does not guarantee that multiplication is a total function.
    – Cort Ammon
    Commented May 1, 2018 at 0:41

Very, very simplified Gödel showed how you can express the statement S "there is no proof for the statement S" in arithmetic, and either S is true, then you have a true statement without proof, or S is false, then you have a false statement with a proof. Incompleteness or contradiction.

You get the exact same result in any system where you can express the same statement S in the system. Now you can reasonably argue that systems where you can express S are stronger and those where you cannot express S are weaker, and it follows that stronger systems are incomplete or contradictory, while weaker systems may be both complete and without contradictions.

  • 1
    What if we introduce some alternative notion of proof? Has anyone studied such systems?
    – Punga
    Commented Apr 30, 2018 at 20:40

You must log in to answer this question.

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