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 Free Access

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] Seymour Ginsburg and Edwin H. Spanier, Semigroups, Presburger formulas, and languages, Pacific J. Math. 16 (1966), 285–296. MR 0191770
  • [KW] G. Kreisel and Hao Wang, Some applications of formalized consistency proofs, Fund. Math. 42 (1955), 101–110. MR 0073539
  • [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}$] Rohit J. Parikh, On context-free languages, J. Assoc. Comput. Mach. 13 (1966), 570–581. MR 0209093
  • [Pa$ _{4}$] Rohit Parikh, Existence and feasibility in arithmetic, J. Symbolic Logic 36 (1971), 494–508. MR 0304152
  • [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

DOI: https://doi.org/10.1090/S0002-9947-1973-0432416-X
Keywords: Peano arithmetic, length of proofs, Presburger arithmetic
Article copyright: © Copyright 1973 American Mathematical Society