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 ?
Is Godel’s incompleteness theorem unavoidable
foundationsincompletenesssoft-question
Related Solutions
Is it possible to deduce Godel's first incompleteness theorem from Chaitin's incompleteness theorem?
Gödel's incompleteness theorem, in its modern form using Rosser's trick, only requires that (beyond being effective and sufficiently strong), the theory must be consistent. There is no requirement that the theory has to be $\omega$-consistent or meet any soundness assumption beyond simple consistency. You cannot apply Chaitin's theorem in its usual form to these theories, in general, because the usual form of Chaitin's theorem assumes more (e.g. many proofs of Chaitin's theorem assume as an extra soundness assumption that the theory only proves true statements.)
Many of the "alternate proofs" also require stronger assumptions than the standard proof of the incompleteness theorem. You have to be very careful when reading about this to check which assumptions are included in each theorem.
In the particular proof of Chaitin's theorem presented by Kritchman and Raz, however, they do not need to assume any particular soundness beyond just consistency. I am going to explain this in detail.
They do need to assume that $T$ is sufficiently strong. In particular, they assume that if $n$ and $L$ satisfy $K(n) < L$, then $T \vdash \hat K(\dot n) < \dot L$. Here $\dot n$ and $\dot L$ are terms of the form $1 + 1 + \cdots + 1$ corresponding to $n$ and $L$, and $\hat K$ is a formula of arithmetic defined directly from the definition of $K$. (Note that the set of pairs $(n,L)$ with $K(n) < L$ is recursively enumerable, so there is no real issue in assuming $T$ proves all true sentences of that form.)
Given the assumption on $T$, their proof goes as follows (rephrased in more precise terms):
Begin proof
Given $L$, we can make a program $e_L$ that does the following:
Search for any $n$ such that $T \vdash \hat K (\dot n) > \dot L$. We do this by searching through all $T$-proofs in an exhaustive manner.
Output the first such $n$ we find, if we ever find one.
Because we can code $L$ into the program as a fixed constant, using the standard coding methods, the length $|e_L|$ of $e_L$ no worse than $2\log(L) + C$ for some constant $C$. In particular, we can fix an $L$ with $|e_L| < L$. Assume such an $L$ is fixed.
For this $L$, suppose $e_L$ returns a value, $n$. Then $K(n) \leq |e_L| < L$. By our assumption that $T$ is sufficiently strong, this means $T$ proves $\hat K (\dot n) < \dot L$.
But if $e_L$ returns $n$ then $T$ also proves $\hat K(\dot n) > \dot L$. This means that if $e_L$ returns a value then $T$ is inconsistent. So, if we assume $T$ is consistent, then $e_L$ cannot return a value. This means that, for our fixed $L= L_T$, $T$ cannot prove $\hat K(\dot n) > \dot L$ for any $n$.
Thus, if we take $n = n_T$ to be such that $K(n) > L$, we have that $\hat K (\dot n) > \dot L$ is a true statement that is not provable in $T$.
End proof
This proof just given (in italics) proves:
If $T$ is a consistent, effective theory of arithmetic that proves every true formula of the form $\hat K(\dot n) < \dot L$, then there is a true statement of the form $\hat K(\dot n) > \dot L$ that is not provable in $T$.
This is almost the same as Gödel's incompleteness theorem. The only difference is that the usual proof of the incompleteness theorem gives us an explicit formula that it is true but not provable in $T$ (namely, the Rosser sentence of $T$). On the other hand, the proof in italics requires us to find $n_T$ in order to have an explicit example, and there is no algorithm to do this.
This is one motivation for what I think of as the "standard form" of Chaitin's theorem. In that form, we look instead for unprovable sentences of the form ($\dagger$): $(\exists x)[\hat K(x) > \dot L]$.
Because we can compute $L= L_T$, we can compute a specific sentence of that form for $T$. But, for the proof to work, we need to have an actual $n$ such that $T \vdash \hat K(\dot n) > \dot L$. So we have to add an additional soundness assumption to the theorem, namely that if $T$ proves a sentence of the form ($\dagger$) then there is an $n$ such that $T$ proves $\hat K(\dot n) > \dot L$.
Overall, in this version of Chaitin's theorem, we have an explicit sentence, but with a stronger soundness assumption. The proof of Gödel's incompleteness theorem using Rosser's method gives us an explicit sentence without any stronger soundness assumption.
First, recall that for any structure $\mathcal{A}$ - including $\mathcal{N}:=(\mathbb{N};+,\times)$, the standard model of arithmetic - the theory of $\mathcal{A}$ $$Th(\mathcal{A}):=\{\varphi:\mathcal{A}\models\varphi\}$$ is trivially complete and consistent. Since $\mathcal{N}\models\mathsf{PA}$ this gives as a special case that $Th(\mathcal{N})$ - more commonly denoted "$\mathsf{TA}$" for "true arithmetic" - is a very natural complete consistent theory extending $\mathsf{PA}$.
So Godel's incompleteness theorem cannot possibly apply to arbitrary complexity theories, at least not without additional complicating hypotheses which would rule out things like $\mathsf{TA}$.
OK, now let's actually say a bit about Godel.
The proof of the first incompleteness theorem has a key technical limitation: the theory $T$ in question must exhibit a combination of weakness and strength. Roughly speaking, $T$ must be able to prove all "very basic" facts about its own provability predicate. This both requires $T$ to be reasonably strong, and requires $T$ to be not too complicated. For example, true arithmetic $\mathsf{TA}$ is not definable in $\mathcal{N}$, so it can't even talk about itself at all (let alone prove things about itself).
As such, GIT is in fact fairly limited. Here's one way to pose GIT which is pretty close to optimal:
No consistent complete r.e. theory can interpret Robinson arithmetic.
The notion of interpretation here is a particularly technical one, so this isn't necessarily a good formulation of the incompleteness theorem to start off focusing on. But I think it's a good thing to see, if only briefly, early on: the various ingredients (consistency, completeness, r.e.-ness, and "logical strength" in some capacity) are clearly displayed and there is no imprecise language being used.
That said, we can indeed push Godel beyond the r.e. theories, at least to a certain extent. Basically, we just need to strengthen the consistency hypothesis to rule out errors which are "low-level" compared to the theory itself. One result along these lines which I think is folklore is discussed at this old answer of mine (albeit focusing on theories in the language of arithmetic for simplicity - note that I just corrected that answer, since looking back on it the original version had an indexing error!).
Best Answer
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:
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.