Ykhjuy

I have a question regarding the Hilbert Program and Gödel's Incompleteness Theorems. Below I will express my current understanding of them $($... if I get something wrong, please correct me!$)$ ... followed by my question.

Roughly put, the aim of the Hilbert Program was to look for a 'sound' and 'complete' set of axioms for mathematics: a set of axioms that logically imply all $($'completeness') and only $($'soundness'$)$ mathematical truths.

Now, it is my understanding that this is 'roughly put', because 'mathematical truth' is a bit of a tricky notion: unlike 'logical truth', for which we have a nice formal semantics $($at least for first-order logic$)$, we don't have a general formal semantics for all of 'mathematical truth'.

Avoiding semantics, then, the Hilbert Program was actually stated as a syntactical one: instead of asking for a 'sound' $($all true$)$ and complete set of axioms, the aim was to provide a 'consistent' and complete set of axioms: a set of axioms from which one cannot derive both $varphi$ and $neg varphi$ for some statement $varphi$. Likewise, 'completeness' is to be understood purely syntactically as well: for every statement $varphi$, we can derive either $varphi$ or $neg varphi$. ... Still, I assume the implicit goal was to have a set of axioms that would at least 'match' such 'mathematical truths' like $1+1=2$

Finally, Hilbert was hoping that there would be some 'effective method' or algorithm that could decide, for any statement $varphi$, whether $varphi$ was derivable from the axioms or not. Roughly translating this back into 'truth': if there would be such an algorithm, we could say that 'truth' is decidable. This is Hilbert's "Entscheidungsproblem"

OK, here is my question: Why did Hilbert add the criterion of decidability? Don't consistency and completeness together imply decidability? Because one can simply enumerate all possible proofs $($as finite sequences of symbols, the set of all proofs is enumerable$)$. Then, since by completeness either $varphi$ or $neg varphi$ is provable, at some point you will run into one of those proofs. If it turns out to be a proof of $varphi$, then obviously $varphi$ is derivable/provable, and if we find a proof of $neg varphi$, then by consistency we know that there is no proof of $varphi$. So, we can decide whether $varphi$ is provable or not.

Am I wrong about this? But if not: why did Hilbert explicitly add decidability to consistency and completeness?

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 "$langlevarphirangle$" 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 $negvarphi$. 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}modelsnegvarphi$), 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 modelsvarphiimpliesmathcal{A}modelsnegvarphi$, and so either $varphiin Th(mathcal{A})$ or $negvarphiin 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 xforall 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 $Tvdashvarphi$, 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 Godel'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 xforall y(x=y)}$ in the empty language.

Where Godel 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. Godel, 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. Godel 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.