Formalization of logic: from high hopes to limitations

We will read some of the early communications of Russell, Frege and Hilbert from the first few years of 1900's which are concerned with formalizations of arithmetics and by extension of the whole mathematics (in particular of set theory which started to emerge as an axiomatic system around that time). The short letters between Russell and Frege show the awarness of the problems which formalization might encounter, but also a mild optimism with regard to the possibility of resolving them. Hilbert's address is perhaps more optimistic, in particular when he mentions the consistency of whole mathematics, which he took to be a desirable (and achievable) goal.

These optimistic communications seem too optimistic in light of Goedel's result from 1931 on incompleteness which we also include here.  

Remark. While formalization of logic was successfully carried out by Hilbert and Ackermann in the end of 1920's (see also next Remark), it failed to provide the desired outcome of ensuring the consistency and completeness of mathematics, carried out in the formal system (this outcome was blocked by Goedel's results). The hopes that mathematics could be reduced to simple manipulation of symbols (in a formal system) was of a theoretical concern at the time, but would be a more practical one today with powerful computers around. However, Goedel's results put an early stop to this "easy" approach to mathematics.

Remark. An earlier result of Goedel in 1930 (also included here) showed that the system of Hilbert and Ackermann correctly captures the connection between truth and the proof (completeness theorem). This is still seen as a very important and desirable feature of first-order logic.