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$ – Trevor Wilson Sep 7 '12 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 '12 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$ – Trevor Wilson Sep 7 '12 at 20:21
  • $\begingroup$ @TrevorWilson, I removed one 'provable' from the first question. Also added an explanation. $\endgroup$ – CamelCamelCamel Sep 7 '12 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$ – Trevor Wilson Sep 8 '12 at 1:56

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.

| cite | improve this answer | |
  • $\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$ – Trevor Wilson Sep 8 '12 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$ – Trevor Wilson Sep 8 '12 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$ – hmakholm left over Monica Sep 8 '12 at 20:41
  • $\begingroup$ @HenningMakholm I love this answer! Very cute. :) $\endgroup$ – Peter Smith Sep 9 '12 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.

| cite | improve this answer | |
  • $\begingroup$ This argument depends on inconsistent theories being considered complete, but isn't a complete theory usually defined as a maximal consistent theory? $\endgroup$ – Trevor Wilson Sep 10 '12 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$ – Carl Mummert Sep 10 '12 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$ – Carl Mummert Sep 10 '12 at 10:44
  • $\begingroup$ @Henning Makholm: I mistyped. I meant "completeness" in two places where I didn't type it. Thanks. $\endgroup$ – Carl Mummert Sep 10 '12 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$ – hmakholm left over Monica Sep 10 '12 at 19:49

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.