So after Godel's Incompleteness theorem and the fact that some theorems mathematicians are interested in are independent of ZFC (e.g. Continuum Hypothesis) is there some hope for some other foundational theory which will be (provably) complete and the fact that it is complete will not imply it`s inconsistency ? Furthermore, is there hope for such theory to have have most of axioms to be intuitive, I mean not to be ad hoc ? If it is not, can it still be that there is some way different from foundations based on one foundating theory from which we build all other theories, which will allow us to avoid Godel incompletness theorem ? Or is it just unavoidable ?

  • 1
    $\begingroup$ You can avoid them in paraconsistent logics. $\endgroup$ – Shaun Aug 5 '18 at 12:52
  • 5
    $\begingroup$ The incompleteness theorem applies, roughly speaking, to any collection of axioms which 1) can be described by a computer program and 2) is powerful enough to describe computer programs; this is the meat of what's necessary to run the proof. If your axioms don't satisfy 1) then in general you have no way of telling what a valid proof from your axioms looks like. And if they don't satisfy 2) then your axioms are not powerful enough to do mathematics. See scottaaronson.com/democritus/lec3.html for some details. $\endgroup$ – Qiaochu Yuan Aug 5 '18 at 13:40
  • $\begingroup$ I think Qiaochu's comment says it all : Gödel's theorem essentially arises from the tension between being powerful enough to describe what's interesting to us, and being weak enough as to be interesting to us (a non recursively enumerable theory could be awesome, but it wouldn't be interesting to any user) $\endgroup$ – Max Aug 5 '18 at 15:16
  • $\begingroup$ The problem (as I see it) is that in order to ask questions about an infinite set we have to approach it from a finite perspective, which obviously is going to come short. If we could do uncountable computations, we could simply check the continuum hypothesis by checking the cardinality of every subset of $\mathbb{N}$. $\endgroup$ – Dark Malthorp Aug 5 '18 at 16:13
  • 1
    $\begingroup$ @DarkMalthorp That's missing the point: even basic questions about natural numbers get us into trouble. See my answer below. $\endgroup$ – Noah Schweber Oct 14 '18 at 17:44

The MRDP theorem gives a very good case that there is no satisfying way around this. Specifically, any foundational system we use surely needs to be able to talk about Diophantine equations. Specifically, let me phrase it this way:

Suppose $T$ is a complete computable theory. Then there is no computable function $f$ from Diophantine equations to sentences in the language of $T$ such that $T$ proves $f(E)$ iff $E$ has a solution.

Why should this be weird? Well, note that such an $f$ does exist for many natural computable, but incomplete, theories: PA, ZFC, etc., really any theory which is (i) $\Sigma_1$-sound and (ii) reasonably powerful.

Proof: otherwise, we could computably tell whether a Diophantine equation $E$ has a solution by searching through $T$-proofs - if $E$ has a solution we eventually find a proof of $f(E)$, and if $E$ has no solution then by completeness we eventually find a proof of $\neg f(E)$. And we can't find both, since then $T$ would be inconsistent and hence prove everything, and in particular prove $f(D)$ for some $D$ with no solutions, contradicting our hypothesis. $\Box$

So if we want to build a complete computable theory, we'll need to accept that this won't allow us to talk about even Diophantine equations in any reasonable way.

More generally, we're just running into the fact that the set of Diophantine equations without solutions isn't c.e.; so even if we move away from classical logic we won't be able to get completeness for Diophantine equations without proving that some Diophantine equation simultaneously does and doesn't have solutions, which is surely something we don't want!

The obvious thing to try to drop at this point is computability, but at that point our system isn't usable: we have no way to tell whether a purported proof in the system is in fact valid.

Now, this doesn't rule out interesting fragments of mathematics being fully decidable, such as arithmetic with only addition. But these are the exceptions, not the rule, and they don't even account for basic high school mathematics. Nobody would consider such a weak theory to be an appropriate foundation for mathematics.

  • $\begingroup$ @CarlMummert Whoops, fixed. $\endgroup$ – Noah Schweber Oct 14 '18 at 22:45
  • $\begingroup$ No problem, I do that too often myself. By the way -you might know some more examples for this question $\endgroup$ – Carl Mummert Oct 14 '18 at 23:06

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.