In 1931, when he was only 25 years of age, the great Austrian logician Kurt Gödel (1906– 1978) published an epoch-making paper [16] (for an English translation see [8, pp. 5–38]), in which he proved that an effectively definable consistent mathematical theory which is strong enough to prove Peano’s postulates of elementary arithmetic cannot prove its own consistency. In fact, Gödel first established that there always exist sentences φ in the language of Peano Arithmetic which are true, but are undecidable; that is, neither φ nor ¬φ is provable from Peano’s postulates. This is known as Gödel’s First Incompleteness Theorem. This theorem is quite remarkable in its own right because it shows that Peano’s well-known postulates, which by and large are considered as an axiomatic basis for elementary arithmetic, cannot prove all true statements about natural numbers. But Gödel went even further. He showed that his first incompleteness theorem implies that an effectively definable sufficiently strong consistent mathematical theory cannot prove its own consistency. This theorem became known as Gödel’s Second Incompleteness Theorem. Since then the two theorems are referred to as Gödel’s Incompleteness Theorems. They became landmark theorems and had a huge impact on the subsequent development of logic. In order to give more context, we step further back in time. The idea of formalizing logic goes back to the ancient Greek philosophers. One of the first to pursue it was the great German philosopher and mathematician Gottfried Wilhelm Leibniz (1646–1716). His dream was to develop a universal symbolic language, which would reduce all debate to simple calculation. The next major figure in this pursuit was the English mathematician George Boole (1815–1864), who has provided the first successful steps in this direction. This line of research was developed to a great extent by the famous German mathematician and philosopher Gottlob Frege (1848–1925), and reached its peak in the works of Bertrand Russell (1872–1970) and Alfred North Whitehead (1861–1947). Their magnum opus Principia Mathematica [27] has provided relatively simple, yet rigorous formal basis for logic, and became very influential in the development of the twentieth century logic. ∗Mathematical Sciences; Dept. 3MB, Box 30001; New Mexico State University; Las Cruces, NM 88003; gbezhani@nmsu.edu. We recall that a theory is consistent if it does not prove contradiction. More details on the work of Boole, Frege, and Russell and Whitehead can be found on our webpage http://www.cs.nmsu.edu/historical-projects/; see the historical projects [24, 7]. The work of Boole has resulted in an important concept of Boolean algebra, which is discussed in great length in a series of historical projects [3, 2, 1], also available on our webpage.