Are there formal systems that can not be proved to be complete or incomplete?

Question

I'm reading GEB and was thinking about this. Are there any formal systems where the proof of their completeness/incompleteness is unprovable?

This question could go ad infinitum. Could there be any formal systems where the proof that their completeness/incompleteness is not provable - could be not provable?

Let's try and say this again:

Are there any formal systems where one can not prove whether they are complete or incomplete?

Are there any formal systems where one can not prove that a proof exists / does not exist that says whether that system if complete or incomplete?

and so on..

I'm not looking for the full on hardcore mathematical explanation, just a some explanation about the current research results in the area.

Answer 1

For each reasonable meta-theory $M$ that is strong enough do do metamathematics in, we can find a theory $T$ such that "$T$ is complete" is independent of $M$:

By Gödel's incompleteness theorem, there is a primitive recursive function $f:\mathbb N\to\mathbb N$ such that $\exists x\in\mathbb N: f(x)=1$ is independent of $M$. Fix such an $f$.

Now we'll construct $T$ as a first-order theory with equality over the language with a single unary predicate $p$. The non-logical axioms of $T$ will be

1. $x=y$
2. $\underbrace{p(x)\land p(x)\land\cdots\land p(x)}_{n\text{ conjuncts}}$ for each $n$ such that $f(n)=1$.

Axiom scheme 2 is a bit unconventional in shape, but it is clear that the $T$ we have specified here is effectively axiomatized, which is all we usually ask of theories.

Axiom 1 makes sure that every model of $T$ has cardinality $1$. The interpretation where $p$ is true for the single element of the universe is a model of $T$; whether $T$ is complete or not is a matter of whether the interpretation where $p$ is false for the single element is also a model. But that depends on whether axiom scheme 2 has any instances, and that depends on whether $f(n)$ is ever $1$ for any $n$. But by construction, that is something $M$ doesn't know -- so $M$ doesn't know whether $T$ is complete or nor either.

Answer 2

Henning Makholm points out one way to achieve this. But it is also the case that, in reasonable cases, "$T$ is incomplete" is independent of $T$ itself. Let's just stick to PA; the explanation will show what properties of PA are actually required.

First, we have to work out what we mean by the statement "$T$ is complete" in PA. Since PA cannot talk about models, the definition has to be syntactic. I will take "$T$ is complete" to mean that for every $\phi$, either $\phi$ is provable or $\lnot \phi$ is provable. That is, $(\forall \phi)[\text{Pvbl}(\phi) \lor \text{Pvbl}(\lnot \phi)]$, where Pvbl is the formalized provability predicate for $T$. I do not assume in the definition that only one is provable, just that at least one is; so I am taking a very weak syntactic definition of completeness. But the same argument will go through if we define "$T$ is complete" to mean that for every $\phi$ exactly one of $\phi$ and $\lnot \phi$ is provable. That is the usual syntactic criterion for completeness (although it implicitly assumes consistency in a certain sense).

If PA proves "PA is not complete" then PA proves there is some $\phi$ such that neither Pvbl($\phi$) nor Pvbl($\lnot \phi$). Thus PA proves $(\exists x)\lnot\text{Pvbl}(x)$. But it is known that $(\exists x) \lnot \text{Pvbl}(x)$ is not provable in PA because that sentence is equivalent to Con(PA) over PA. So PA cannot prove "PA is not complete".

Now assume PA proves "PA is complete". Then for every actual formula $\phi$, PA proves that either Pvbl($\phi$) or Pvbl($\lnot \phi$). However, because PA is $\omega$-consistent, if PA proves that a formula is provable then the formula really is provable. Thus, if PA proves "PA is complete" then PA really is complete. But that is not the case, so PA cannot prove that PA is complete.

In the end all that we need to know about PA is that the incompleteness theorems apply to it and that it is sound for $\Sigma^0_1$ sentences. There are certainly finitely axiomatized theories that have those properties, for example NBG set theory.