Abstract
At the 1993 meeting of the Kurt Gödel Society, we described some axiom systems that could verify their own consistency and prove all Peano Arithmetic's II1 theorems. We will extend these results by introducing some new axiom systems which use stronger definitions of self-consistency.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. Benett, Ph. D. Dissertation, Princeton University.
A. Bezboruah and J. Shepherdson, “Gödel's Second Incompleteness Theorem for Q”, J of Symbolic Logic 41 (1976), 503–512.
S. Buss, “Polynomial Hierarchy and Fragments of Bounded Arithmetic“, 17th ACM Symposium on Theory of Comp (1985) pp. 285-290
S. Buss, Bounded Arithmetic, Princeton Ph. D. dissertation published in Proof Theory Lecture Notes, Vol. 3, published by Bibliopolic (1986).
S. Feferman, “Arithmetization of Metamathematics in a General Setting”, Fund Math 49 (1960) pp. 35–92.
P. Hájek, “On the Interpretatability of Theories Containing Arithmetic (11)”, Comm. Math. Univ. Carol. 22 (1981) pp.595–594.
P. Hájek and P. Pudlák, Metamathematics of First Order Arith, SpringerVerlag 1991
R. Jeroslow, “Consistency Statements in Formal Mathematics”, Fundamentae Mathematicae 72 (1971) pp. 17–40.
S. Kleene, “On the Notation of Ordinal Numbers”, JSL 3 (1938), pp. 150–156.
J. Krajíček, “A Note on the Proofs of Falsehoods”, Arch Math Logik 26 (1987) pp. 169–176.
J. Krajícek, Bounded Propositional Logic and Compl. Theory, Cambridge U Press 1995
J. Krajicek and P. Pudlik, “Propositional Proof Systems, The Consistency of First-Order Theories and The Complexity of Computation”, JSL 54 (1989) pp 1063–1079.
G. Kreisel, “A Survey of Proof Theory, Part I” in Journal of Symbolic Logic 33 (1968) pp. 321–388 and “ Part II” in Proceedings of Second Scandinavian Logic Symposium (1971) North Holland Press (with Fenstad ed.), Amsterdam
G. Kreisel and G. Takeuti, “Formally self-referential propositions for cut-free classical analysis and related systems”, Dissertations Mathematica 118, 1974 pp. 1–55.
M. Löb, A Solution to a Problem by Leon Henkin, JSL 20 (1955) pp. 115–118.
E. Nelson, Predicative Arithmetic, Mathematical Notes, Princeton Press, 1986.
R.Parikh, “Existence and Feasibility in Arithmetic”, JSL 36 (1971), pp.494–508.
J. Paris and C. Dimitracopoulos, “A Note on the Undefinability of Cuts”, JSL 48 (1983) pp. 564–569.
J. Paris and A. Wilkie, “Δ0 Sets and Induction”, Proceedings of the Jadswin Logic Conference (Poland), Leeds University Press (1981) pp. 237–248.
P. Pudlák, “Cuts Consistency Statements and Interpretations”, JSL 50 (1985) 423–442.
P. Pudlák, “On the Lengths of Proofs of Consistency”, Kurt Gödel Soceity Proc. (1996).
H. Rogers, Theory of Rec. Funct. & Effective Comp., McGraw Hill 1967, see pp 186–188.
C. Smorynski, “The Incompleteness Theorem”, Handbook Math Logic, 821–866, 1983.
R. Solovay, Private Communications (April 1994) proving Footnote l's statement. (See Appendix A of [31] for more details about Solovay's Extension of Pudlik's theorem [20].)
R. Statman, “Herbrand's theorem and Gentzen's Notion of a Direct Proof”, Handbook on Math Logic, (1983) pp. 897–913.
G. Takeuti, “On a Generalized Logical Calculus“, Japan J. Math 23 (1953) 39–96.
G. Takeuti, Proof Theory, Studies in Logic Volume 81, North Holland, 1987.
A. Wilkie and J. Paris, “On the Scheme of Induction for Bounded Arithmetic”, Annals Pure Applied Logic (35) 1987, pp. 261–302.
D. Willard, “Self-Verifying Axiom Systems”, in Proceedings of the Third Kurt Gödel Symposium (1993) pp. 325–336, published in Springer-Verlag LNCS (Vol. 713).
D. Willard, “Self-Reflection Principles and NP-Hardness”, in Proceedings of 1996 DIMACS Workshop on Feasible Arithmetic and Length of Proof (AMS Press.
D. Willard, “Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles” manuscript (1997).
D. Willard, “Some Curious Exceptions to the Second Incompleteness Theorem”, longer manuscript which is the unabridged version of the present conference paper.
C. Wrathall, Rudimentary Predicates and Relative Computation, Siam J. on Computing 7 (1978), pp. 194–209.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Willard, D.E. (1997). The tangibility reflection principle for self-verifying axiom systems. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1997. Lecture Notes in Computer Science, vol 1289. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63385-5_53
Download citation
DOI: https://doi.org/10.1007/3-540-63385-5_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63385-3
Online ISBN: 978-3-540-69806-7
eBook Packages: Springer Book Archive