Some results on the length of proofs
HTML articles powered by AMS MathViewer
- by R. J. Parikh
- Trans. Amer. Math. Soc. 177 (1973), 29-36
- DOI: https://doi.org/10.1090/S0002-9947-1973-0432416-X
- PDF | Request permission
Abstract:
Given a theory T, let $\vdash _T^kA$ mean “A has a proof in T of at most k lines". We consider a formulation $P{A^\ast }$ of Peano arithmetic with full induction but addition and multiplication being ternary relations. We show that ${ \vdash ^k}A$ is decidable for $P{A^\ast }$ and hence $P{A^\ast }$ is closed under a weak $\omega$-rule. An analogue of Gödel’s theorem on the length of proofs is an easy corollary.References
- Seymour Ginsburg and Edwin H. Spanier, Semigroups, Presburger formulas, and languages, Pacific J. Math. 16 (1966), 285–296. MR 191770, DOI 10.2140/pjm.1966.16.285
- G. Kreisel and Hao Wang, Some applications of formalized consistency proofs, Fund. Math. 42 (1955), 101–110. MR 73539, DOI 10.4064/fm-42-1-101-110 R. Parikh, A decidability result for first order systems, J. Symbolic Logic 30 (1965), 269. (abstract) —, Some results on lengths of proofs, Notices Amer. Math. Soc. 13 (1966), 487. Abstract #66T-255.
- Rohit J. Parikh, On context-free languages, J. Assoc. Comput. Mach. 13 (1966), 570–581. MR 209093, DOI 10.1145/321356.321364
- Rohit Parikh, Existence and feasibility in arithmetic, J. Symbolic Logic 36 (1971), 494–508. MR 304152, DOI 10.2307/2269958 M. Presburger, Über die Vollständigkeit eines gewissen Systems der Arithmetic ganzer Zahlen, Comptes-rendus du I congrès des mathématiciens de pays Slaves, Warsaw, 1929, 1930, pp. 92-101, 395. D. Richardson, Some theorems with short proofs (to appear).
Bibliographic Information
- © Copyright 1973 American Mathematical Society
- Journal: Trans. Amer. Math. Soc. 177 (1973), 29-36
- MSC: Primary 02D99
- DOI: https://doi.org/10.1090/S0002-9947-1973-0432416-X
- MathSciNet review: 0432416