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.

  • $\begingroup$ I think you may be using the word "proof" at least one time too many in each paragraph. Would it capture your intended meaning to ask "are there any formal systems whose completeness is undecidable"? It might also help to specify the meta-theory. $\endgroup$ Sep 7, 2012 at 19:49
  • $\begingroup$ @TrevorWilson Decidability is sometimes a term used for computable. In terms of theories, it may mean that the theory is computable, i.e. there is a computable algorithm for determining whether a statement is proveable. This appears to be stronger. $\endgroup$
    – William
    Sep 7, 2012 at 20:01
  • $\begingroup$ @William: You're right. Instead of "undecidable" I meant to say "independent of the meta-theory". As it stands the question does not quite make sense: what does "the proof...is unprovable" mean? $\endgroup$ Sep 7, 2012 at 20:21
  • $\begingroup$ @TrevorWilson, I removed one 'provable' from the first question. Also added an explanation. $\endgroup$ Sep 7, 2012 at 21:20
  • $\begingroup$ Is there a formal definition for "formal system"? I'm asking because usually the definition of completeness presupposes some kind of semantics. $\endgroup$ Sep 8, 2012 at 1:56

2 Answers 2


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.

  • $\begingroup$ Can you find a finitely axiomatized theory $T$ with this property? Your example seems dubious to me because whatever the theory $T$ might turn out to be as a set of sentences, by "looking at" that set of sentences we can easily tell whether the theory is complete or incomplete; it's just that we don't know what set of sentences the theory is. $\endgroup$ Sep 8, 2012 at 2:58
  • 1
    $\begingroup$ This is a technically correct answer to a reasonable interpretation of the problem, of course. The reason I kept asking the OP for clarification was that I was trying to ascertain whether some trick like this would count, but you beat me to it :) $\endgroup$ Sep 8, 2012 at 3:06
  • $\begingroup$ @Trevor: No -- I don't know how to make a finitely axiomatized theory hard to reason about without ending up so strong that it is essentially incomplete. $\endgroup$ Sep 8, 2012 at 20:41
  • $\begingroup$ @HenningMakholm I love this answer! Very cute. :) $\endgroup$ Sep 9, 2012 at 11:50

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.

  • $\begingroup$ This argument depends on inconsistent theories being considered complete, but isn't a complete theory usually defined as a maximal consistent theory? $\endgroup$ Sep 10, 2012 at 3:36
  • $\begingroup$ If you strengthen the definition of completeness to say that exactly one of $\phi$ or $\lnot \phi$ is provable for each $\phi$, the same argument goes through; that is the usual definition of completeness. So the argument does not depend on inconsistent theories being considered complete. If you define complete to mean "Consistent and there is no extensionally larger consistent theory", the negation of this is "if consistent, there is an extensionally larger consistent theory", which is essentially the incompleteness theorem, so PA would prove that it is incomplete in that sense. $\endgroup$ Sep 10, 2012 at 10:39
  • $\begingroup$ Other strange things happen with "maximal consistent" theories in PA, though. For example, PA proves that "the maximal consistent initial segment of the standard enumeration of axioms of PA" is a consistent theory. Of course we know that this initial segment contains all the axioms, because PA is consistent. In this sense PA proves its own consistency... but PA does not prove the maximal consistent initial segment of its axioms contains all its axioms. Things like this suggest that definitions involving "maximal" are not natural for use in PA. $\endgroup$ Sep 10, 2012 at 10:44
  • $\begingroup$ @Henning Makholm: I mistyped. I meant "completeness" in two places where I didn't type it. Thanks. $\endgroup$ Sep 10, 2012 at 19:24
  • $\begingroup$ +1. In my answer, I attempted to sidestep the issue of whether an inconsistent theory is "complete", by deliberately restricting my attention to theories that the metatheory can prove consistent. $\endgroup$ Sep 10, 2012 at 19:49

You must log in to answer this question.

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