On the completeness of the calculus of logic (1929)
Solomon Feferman, John W Dawson, Stephen Cole Kleene, Gregory Martin Moore, Robert M Solovay, Jean van HEIJENOORT · 2001
Abstract The main object of the following investigations is the proof of the completeness of the axiom system for what is called the restricted functional calculus, namely the system given in Whi’tehead and Russell 1910, Part I, *1 and *10, and, in a similar way, in Hilbert and Ackermann 1928 (hereafter cited as H. A.), III, §5. Here ‘completeness’ is to mean that every valid formula expressible in the restricted functional calculus (a valid Ziihlaussage, as Lowenheim would say) can be derived from the axioms by means of a finite sequence of formal inferences. This assertion can easily be seen to be equivalent to the following: Every consistent axiom system1 consisting of only Ziihlaussagen has a realization. (Here ‘consistent’ means that no contradiction can be derived by means of finitely many formal inferences.) The latter formulation seems also to be of some interest in itself, since the solution of this question represents in a certain sense a theoretical completion of the usual method for proving consistency (only, of course, for the special kind of axiom systems considered here); for it would give us a guarantee that in every case this method leads to its goal, that is, that one must either be able to produce a contradiction or prove the consistency by means of a model.2 L. E. Brouwer, in particular, has emphatically stressed that from the consistency of an axiom system we cannot conclude without further ado that a model can be constructed. But one might perhaps think that the existence of the notions introduced through an axiom system is to be defined outright by the consistency of the axioms and that, therefore, a proof has to be rejected out of hand.