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.