Speed-up by theories with infinite models
HTML articles powered by AMS MathViewer
- by R. Statman PDF
- Proc. Amer. Math. Soc. 81 (1981), 465-469 Request permission
Abstract:
We prove that if $S$ is a finite set of schemata and $A$ is a sentence undecided by $S$ such that $S \cup \{ {\neg A} \}$ has an infinite model then $S \cup \{A \}$ is an unbounded speed-up of $S$ for substitution instances of tautologies. As a corollary, we obtain a conjecture of Parikh’s.References
- 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. J. Parikh, Some results on the length of proofs, Trans. Amer. Math. Soc. 177 (1973), 29–36. MR 432416, DOI 10.1090/S0002-9947-1973-0432416-X
- Richard Statman, Bounds for proof-search and speed-up in the predicate calculus, Ann. Math. Logic 15 (1978), no. 3, 225–287 (1979). MR 528658, DOI 10.1016/0003-4843(78)90011-6
Additional Information
- © Copyright 1981 American Mathematical Society
- Journal: Proc. Amer. Math. Soc. 81 (1981), 465-469
- MSC: Primary 03F20
- DOI: https://doi.org/10.1090/S0002-9939-1981-0597664-7
- MathSciNet review: 597664