zbMATH — the first resource for mathematics

An open formalism against incompleteness. (English) Zbl 0972.03058
Summary: An open formalism for arithmetic is presented based on first-order logic supplemented by a very strictly controlled constructive form of the omega-rule. This formalism (which contains Peano Arithmetic) is proved (non-constructively, of course) to be complete. Besides this main formalism, two other complete open formalisms are presented, in which the only inference rule is modus ponens. Any closure of any theorem of the main formalism is a theorem of each of these other two. This fact is proved constructively for the stronger of them and nonconstructively for the weaker one. There is, though, an interesting counterpart: the consistency of the weaker formalism can be proved finitarily.
03F30 First-order arithmetic and fragments
Full Text: DOI
[1] Boolos, G., The Logic of Provability , Cambridge University Press, Cambridge, 1973. · Zbl 0891.03004
[2] Church, A., “The constructive second number class,” Bulletin of the American Mathematical Society , vol. 44 (1938), pp. 224–32. · Zbl 0018.33803
[3] Davis, M., “Hilbert’s tenth problem is unsolvable,” American Mathematical Monthly , vol. 80 (1973), pp. 233–69. JSTOR: · Zbl 0277.02008
[4] Ebbinghaus, H.-D., J. Flum, and W. Thomas, Mathematical Logic , Springer, New York, 1984. · Zbl 0556.03001
[5] Feferman, S., “Transfinite recursive projections of axiomatic theories,” The Journal of Symbolic Logic , vol. 27 (1962), pp. 259–316. JSTOR: · Zbl 0117.25402
[6] Feferman, S., “Introductory note to 1931c,” Kurt Gödel: Collected works , vol. 1, edited by S. Feferman, Oxford University Press, London, 1986.
[7] Feferman, S. “Reflecting on incompleteness,” The Journal of Symbolic Logic , vol. 56 (1991), pp. 1–49. JSTOR: · Zbl 0746.03046
[8] Gentzen, G., “New version of the consistency proof for elementary number theory,” pp. 252–86 in The Collected Papers of Gerhard Gentzen , edited by M. E. Szabo, North-Holland, Amsterdam, 1969. (translated from the original: “Neue Fassung der Wiederspruchfreiheitsbeweises für die Reine Zahlentheorie,” Forschung zur Logic und zur Grundlegung der Exakten Wissenschaften , new series vol. 4 (1938), pp. 19–44). · Zbl 0209.30001
[9] Graham, R. L., B. L. Rothschild, and J. H. Spencer, Ramsey Theory , 2d edition, Wiley Interscience Series in Discrete Mathematics and Optimization, New York, 1990. · Zbl 0705.05061
[10] Ignjatović, A., “Hilbert’s program and the \(\omega\)-rule,” The Journal of Symbolic Logic , vol. 59 (1994), pp. 322–43. JSTOR: · Zbl 0820.03002
[11] Jones, J. P., and Y. Matijasevič, “Proof of recursive unsolvability of Hilbert’s tenth problem,” American Mathematical Monthly , vol. 98 (1991), pp. 689–709. JSTOR: · Zbl 0746.03006
[12] Kotlarski, H., “On the incompleteness theorems,” The Journal of Symbolic Logic , vol. 59 (1994), pp. 1414–19. JSTOR: · Zbl 0816.03025
[13] Mendelson, E., Introduction to Mathematical Logic , Van Nostrand, Princeton, 1964. · Zbl 0192.01901
[14] Paris, J., and L. Harrington, “A mathematical incompleteness in Peano Arithmetic,” pp. 1133–42 in Handbook of Mathematical Logic , edited by J. Barwise, North-Holland, Amsterdam, 1977.
[15] Smorinski, C., “The incompleteness theorems,” pp. 821–65 in Handbook of Mathematical Logic , edited by J. Barwise, North-Holland, Amsterdam, 1977.
[16] Smorinski, C., “Some rapidly growing functions,” Mathematical Intelligencer , vol. 2 (1980), pp. 149–154. · Zbl 0453.03049
[17] Suppes, P., Axiomatic Set Theory , Dover, New York, 1972. · Zbl 0269.02028
[18] Takeuti, G. Proof Theory , 2d edition, North-Holland, Amsterdam, 1987. · Zbl 0609.03019
[19] Turing, A., “Systems of logic based on ordinals,” Proceedings of the London Mathematical Society, series 2, vol. 45, (1939) pp. 161–228. · Zbl 0021.09704
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.