Automated proofs of Löb's theorem and Gödel's two incompletensess theorems

1. Boolos, G., The Unprovability of Consistency, Cambridge: Cambridge University Press (1979).

   Google Scholar 

2. Boolos, G., and Jeffrey, R., Computability and Logic, Cambridge: Cambridge University Press (1980).

   Google Scholar 

3. Gödel, K., ‘On formally undecidable propositions of Principia Mathematica and related systems I,’ English translation in J. Van Heigenoort, From Frege to Gödel: a source book in mathematical logic, 1879–1931, Cambridge: Harvard University Press (1967).

   Google Scholar 

4. Hofstadter, D., Gödel, Escher and Bach: An Eternal Golden Braid, New York: Basic Books, 1979.

   Google Scholar 

5. Löb, M., ‘Solution of a problem of Leon Henken’, Journal of Symbolic Logic 20, 115–118 (1955).

   Google Scholar 

6. Lusk, E., and Overbeek, R., The Automated Reasoning System ITP, ANL-84-72, Argonne National Laboratory (1984).

7. Mendelson, E., Introduction to Mathematical Logic, New York: D. Van Nostrand (1979).

   Google Scholar 

8. Shankar, N., Proof-Checking Metamathematics, Ph.D. Dissertation, University of Texas at Austin (1986).

9. Smullyan, R., Forever Undecided, New York: Knopf (1987).

   Google Scholar 

10. Solovay, R., ‘Provability Interpretations of Modal Logic’, Israel Journal of Mathematics 25, 287–302 (1976).

    Google Scholar 

11. Tarski, A., ‘The Concept of Truth in Formalized Languages,” English translation in A. Tarski, Logic, Semantics, Metamathematics, Oxford: Clarendon Press (1956).

    Google Scholar 

12. Tarski, A., Mostwoski, A., and Robinson, R. M., Undecidable Theories, Amsterdam: North Holland Publishing Co. (1968).

    Google Scholar 

Download references