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 Apr 29 '18 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 Apr 29 '18 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 May 1 '18 at 7:29

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 May 1 '18 at 0:38
  • 1
    @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 May 1 '18 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 Apr 30 '18 at 20:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.