Self-verifying axiom systems

1. G. Boolos, The Unprovability of Consistency: An Essay on Modal Logic Cambridge University Press, 1979.

   Google Scholar 

2. A. Bezboruah and J. Shepherdson, Godel's Second Incompleteness Theorem for Q, Journal of Symbolic Logic 41 (1976) pp. 503–512.

   Google Scholar 

3. S. Buss, Polynomial Hierarchy and Fragments of Bounded, Proceedings of 17th Annual ACM Symposium on Theory of Computing (1985) pp. 285–290

   Google Scholar 

4. S. Buss, Bounded Arithmetic, Princeton Ph. D. dissertation published in Proof Theory Lecture Notes #3 by Bibliopolic (1986), see also [Bu85].

   Google Scholar 

5. S. Buss, private communications.

   Google Scholar 

6. H. Enderton A Mathematical Introduction to Logic Academic Press 1972.

   Google Scholar 

7. S. Feferman, Arithmetization of Metamathematics in a General Setting, Fundamenta Mathematicae 49 (1960) pp. 35–92.

   Google Scholar 

8. S. Feferman, Finitary Inductively Presented Logics, in Proceedings of Logic Colloquium 88, North Holland Publishing House (1989) pp. 191–220.

   Google Scholar 

9. M. Fitting, First Order Logic and Automated Theorem Proving, Springer Verlag Monograph in Computer Science, 1990.

   Google Scholar 

10. G. Gentzen Collected Papers, translated by M.E. Szabo, North Holland, 1969.

    Google Scholar 

11. K. Godel, Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme, I, Monatsh Math Phys, 38, (1931) pp. 173–198.

    Google Scholar 

12. D. Hilbert and B. Bernays, Grundlager der Mathematik Volume 1 (1934) and Volume 2 (1939), Springer.

    Google Scholar 

13. R. Jeroslow, Consistency Statements in Formal Mathematics, Fundamentae Mathematicae 51 (1971) pp. 17–40.

    Google Scholar 

14. G. Kriesel, A Survey of Proof Theory, Part I in Journal of Symbolic Logic 33 (1968) pp. 321–388 (see especially footnote 8 and page 349); Part II in Proceedings of Second Scandinavian Logic Symposium (1971) North Holland Press (with Fenstad ed.), Amsterdam (see especially pp. 117(d) & 166).

    Google Scholar 

15. G. Kriesel and G. Takeuti, Formally self-referential propositions for cut-free classical analysis and related systems, Dissertations Mathematica 118, 1974 pp. 1–55.

    Google Scholar 

16. M. Lob, Solution of a Problem of Leon Henkin, Journal of Symbolic Logic 20 (1955) pp. 115–118.

    Google Scholar 

17. E. Mendelson, Introduction to Mathematical Logic, Wadsworth & Brooks/Cole Mathematics Series, 1987.

    Google Scholar 

18. H. Rogers, Theory of Recursive Functions and Effective Compatibility, McGraw Hill 1967, see especially pp. 186–188.

    Google Scholar 

19. H. Schwichteberg, Proof Theory: Some Applications of Cut Elimination, in Handbook on Mathematical Logic, North Holland Publishing House (1983) pp. 867–896.

    Google Scholar 

20. R. Statman, Herbrand's theorem and Gentzen's Notion of a Direct Proof, in Handbook on Mathematical Logic, North Holland Publishing House (1983) pp. 897–913.

    Google Scholar 

21. R. Smullyan, The Theory of Formal Systems, Princeton University Press, 1961.

    Google Scholar 

22. R. Smullyan, First Order Logic, Springer-Verlag, 1968.

    Google Scholar 

23. C. Smorynski, The Incompleteness Theorem Handbook on Mathematical Logic, pp. 821–866, 1983.

    Google Scholar 

24. G. Takeuti, On a Generalized Logical Calculus, Japan Journal on Mathematics 23 (1953) pp. 39–96.

    Google Scholar 

25. G. Takeuti, Proof Theory, Studies in Logic Volume 81, North Holland, 1987.

    Google Scholar 

26. D. Willard, Quasi-Linear Algorithms for Processing Relational Calculus Expressions, Proc of ACM's PODS-1990 Conf, pp 243–257. This reference may be helpful as an optimization technique to help render an efficient computer implementation of IS. (Much further optimization will clearly be greatly needed.)

    Google Scholar 

27. D. Willard, Self-Verifying Axiom Systems and their Implications, (the unabrideged version of the present article), SUNY-Albany Tech Report, 1993.

    Google Scholar 

Download references