Remote Access Transactions of the American Mathematical Society
Green Open Access

Transactions of the American Mathematical Society

ISSN 1088-6850(online) ISSN 0002-9947(print)



Some results on the length of proofs

Author: R. J. Parikh
Journal: Trans. Amer. Math. Soc. 177 (1973), 29-36
MSC: Primary 02D99
MathSciNet review: 0432416
Full-text PDF

Abstract | References | Similar Articles | Additional Information

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 [Enhancements On Off] (What's this?)

  • [GS] S. Ginsburg and E. Spanier, Semigroups, Presburger formulas, and languages, Pacific J. Math. 16 (1966), 285-296. MR 32 #9172. MR 0191770 (32:9172)
  • [KW] G. Kreisel and H. Wang, Some applications of formalized consistency proofs. I, II, Fund. Math. 42 (1955), 101-110; ibid. 45 (1958), 334-335. MR 17, 447; MR 20 #4483. MR 0073539 (17:447g)
  • [Pa$ _{1}$] R. Parikh, A decidability result for first order systems, J. Symbolic Logic 30 (1965), 269. (abstract)
  • [Pa$ _{2}$] -, Some results on lengths of proofs, Notices Amer. Math. Soc. 13 (1966), 487. Abstract #66T-255.
  • [Pa$ _{3}$] -, On context-free languages, J. Assoc. Comput. Mach. 13 (1966), 570-581. MR 34 #8901. MR 0209093 (34:8901)
  • [Pa$ _{4}$] -, Existence and feasibility in arithmetic, J. Symbolic Logic 36 (1971), 494-508. MR 0304152 (46:3287)
  • [Pr] 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.
  • [R] D. Richardson, Some theorems with short proofs (to appear).

Similar Articles

Retrieve articles in Transactions of the American Mathematical Society with MSC: 02D99

Retrieve articles in all journals with MSC: 02D99

Additional Information

Keywords: Peano arithmetic, length of proofs, Presburger arithmetic
Article copyright: © Copyright 1973 American Mathematical Society

American Mathematical Society