Hilbert program: Does Consistency and Completeness imply Decidability?

Milo Brandt's comment is exactly correct. The issue is when you write

one can simply enumerate all possible proofs

To do this, one needs to be able to identify valid proofs. This is only possible if we know what the axioms are: in a theory $T$, the sequence "$\langle\varphi\rangle$" is a valid proof of $\varphi$ iff $\varphi$ is an axiom of $T$. Indeed, the three conditions are fully independent of each other, in the sense that we can have any two without the third:

• An inconsistent theory is both decidable and complete (it proves everything) but not consistent.

  • Note that some texts define "complete" so that it includes consistency: $T$ is complete iff for each sentence $\varphi$, $T$ proves exactly one of $\varphi$ and $\neg\varphi$. But Hilbert is using the weaker notion of completeness here, which allows for inconsistency.

• If $\mathcal{A}$ is any structure, the set of all axioms true in $\mathcal{A}$ - the theory of $\mathcal{A}$, $Th(\mathcal{A})$ - is consistent and complete, and the latter means $\mathcal{A}\models\neg\varphi$), but in general need not be decidable (take $\mathcal{A}=(\mathbb{N};+,\times)$).

  • In a bit more detail (since it's been asked here before): $Th(\mathcal{A})$ has a model, namely $\mathcal{A}$, and so is consistent by the soundness theorem. The completeness of $Th(\mathcal{A})$ comes down to the inductive definition of "$\models$:" by definition, $\mathcal{A}\not \models\varphi\implies\mathcal{A}\models\neg\varphi$, and so either $\varphi\in Th(\mathcal{A})$ or $\neg\varphi\in Th(\mathcal{A})$.

• The theory of algebraically closed fields is decidable and consistent, but not complete (it doesn't specify the characteristic).

  • A less-interesting but simpler example: consider the language containing a single unary predicate $U$ and the theory $T=\{\exists x\forall y(x=y)\}$; then this theory has exactly (up to isomorphism) two models, each of which has one element, that differ only on whether $U$ holds of that one element. $T$ is clearly consistent and decidable - to tell whether $T\vdash\varphi$, just check whether $\varphi$ is true in each of the two models of $T$, and note that checking whether a statement is true in a finite structure (in a finite language) is computable. However, it's not complete since it doesn't decide whether $\forall x(U(x))$ is true.

---

EDIT: It's important at this point to note that Gödel's theorem does not imply that there is no complete, consistent, decidable theory! For example, the theory of algebraically closed fields of characteristic $17$ (say) is complete, consistent, and decidable, and a more trivial example is given by the theory $\{\exists x\forall y(x=y)\}$ in the empty language.

Where Gödel pops up is when we try to fold in a fourth requirement, saying that the theory is sufficiently strong (e.g. "contains PA"). This is what the "for mathematics" means in "the aim of the Hilbert Program was to look for a 'sound' and 'complete' set of axioms for mathematics" - we want a theory which is capable of "implementing" (in some reasonable sense) all of our mathematics, and something like algebraically closed fields of characteristic $17$ just doesn't cut it.

Very long comment, trying to supply on overview of Hilbert's approach.

See : David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic-Chelsea (English transl. of the 2nd German ed. 1938).

Page 87 :

§ 9. Consistency and Independence of the System of Axioms

The method of arithmetical interpretation, by means of which we were previously able to gain an insight into the consistency and independence of Axioms a) through d) [the axioms of propositional calculus], also makes it possible for us to recognize that the entire axiom system of the predicate calculus is consistent.

Page 88 :

We must not, by the way, overestimate the significance of this consistency proof. It amounts to saying that we assume the domain of individuals underlying the axioms to consist of only a single element, and thus to be finite. We have absolutely no assurance that the formal introduction of postulates unobjectionable as regards content leaves the system of theorems consistent. For example, the question remains unanswered whether the addition of mathematical axioms would not, in our calculus, make any arbitrary formula provable. This problem, whose solution is of fundamental importance for mathematics, is incomparably more difficult than the question dealt with here. The mathematical axioms actually assume an infinite domain of individuals, and there are connected with the concept of infinity the difficulties and paradoxes which play a role in the discussion of the foundations of mathematics.

Page 92 :

§ 10. The Completeness of the Axiom System

We remarked in the first chapter that the completeness of an axiom system can be defined in two ways. In the stronger sense of the word, completeness means that the addition of a previously unprovable formula to the axiom system always yields a contradiction. We do not have this kind of completeness here [i.e. in the case of restricted predicate calculus].

Page 95 :

Having shown that the axiom system is not complete in the stronger sense of the word, we may ask whether we have completeness in the other sense, defined [above]. The question here is whether all universally valid formulas of the predicate calculus, as defined at the beginning of this chapter, can be proved in the axiom system. We actually do have completeness in this sense. The proof is due to K. Gödel, whose exposition we shall follow.

Page 101 :

§ 11. Derivation of Consequences from Given Premises; Relation to Universally Valid Formulas

So far we have used the predicate calculus only for deducing valid formulas. The premises in our deductions, viz. Axioms a) through f), were themselves of a purely logical nature. Now we shall illustrate by a few examples the general methods of formal derivation in the predicate calculus, which previously, before the axioms were set forth, could merely be sketched. It is now a question of deriving the consequences from any premises whatsoever, no longer of a purely logical nature.

Page 107 :

The method explained in this section of formal derivation from premises which are not universally valid logical formulas has its main application in the setting up of the primitive sentences or axioms for any particular field of knowledge and the derivation of the remaining theorems from them as consequences. It may even be said that only now is the concept of a system of axioms formulated with precision; for, a complete axiomatization should include not only the setting up of the axioms themselves, but also the exact statement of the logical means which enable us to derive new theorems from the axioms. We will examine, at the end of this section, the question of whether every statement which would intuitively be regarded as a consequence of the axioms can be obtained from them by means of the formal method of derivation.

Page 108 :

The following question now arises as a fundamental problem: Is it possible to determine whether or not a given statement pertaining to a field of knowledge is a consequence of the axioms ?

We wish to show that this problem can be reduced to one of the pure predicate calculus, i.e. of the calculus containing only predicate and individual variables. For the question of the logical dependence of a statement upon an axiom system can be reduced to the question of whether a given formula of the pure predicate calculus is or is not universally valid. However, this holds only if the axiom system is of the first order.

Page 112 :

§ 12 The Decision Problem

From the considerations of the preceding section, there emerges the fundamental importance of determining whether or not a given formula of the predicate calculus is universally valid. According to the definition given [above], the universal validity of a formula means the same as its universal validity in every domain of individuals. The problem just mentioned is called the problem of the universal validity of a formula. More precisely, instead of universal validity one should speak of universal validity in every domain of individuals. The universally valid formulas of the predicate calculus are precisely those formulas which are deducible from the axiom system of [predicate calculus]. This fact does not yield a solution of the problem of universal validity, since we have no general criterion for the deducibility of a formula [emphasis added]. [...] It is customary to refer to the two equivalent problems of universal validity and satisfiability by the common name of the decision problem of the restricted predicate calculus. As noted [above], we are justified in calling it the main problem of mathematical logic.

Page 119 :

We now report on the most important special cases in which a successful solution of the decision problem has been reached. [...] The theorem that for any formula of the predicate calculus we can find one which is equivalent in respect to satisfiability and which contains only monadic and dyadic predicate variables, has its analogy in the theorem that the decision problem has been solved for all formulas containing only monadic predicate variables.

Page 124 :

Results by A. Church based on papers by K. Gödel show that the quest for a general solution of the decision problem must be regarded as hopeless. We cannot report on these researches in detail within the limits of this book. We shall only remark that a general method of decision ,vould consist of a certain recursive procedure for the individual formulas which would finally yield for each formula the value truth or the value falsehood. Church's work proves, however, the non-existence of such a recursive procedure; at least, the necessary recursions would not fall under the general type of recursion set up by Church, who has given to the somewhat vague intuitive concept of recursion a certain precise formalization.