Article contents
Decision problems for multiple successor arithmetics1
Published online by Cambridge University Press: 12 March 2014
Extract
Let Nk denote the set of words over the alphabet Σk = {1, …, k}. Nk contains the null word which is denoted λ. We consider decision problems for various first-order interpreted predicate languages in which the variables range over Nk (k ≧ 2). Our main result is that there is no decision procedure for truth in the interpreted language which has the subword relation as its only non-logical primitive. This, together with known results summarized in Section 4, settles the decision problem for any language constructed on the basis of the relations and functions listed below.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1966
Footnotes
This paper is part of a Ph.D thesis submitted to the Program in Communication Sciences at the University of Michigan and was presented to the American Mathematical Society, Notices of the American Mathematical Society, 11, Abstract 64T-359 (1964) 582.
The author gratefully acknowledges the suggestions and corrections offered by J. H. Bennett, C. C. Elgot and E. C. Wagner. The author is especially grateful to J. B. Wright who has provided so much encouragement through many englightening and stimulating discussions.
This work was supported in part by the following government agencies through contracts and grants administered by the University of Michigan; Office of Naval Research contact Nonr 1224(21); National Science Foundation grant G-22258; U. S. Army Research Office (Durham) grant DA-ARO(D)-31–121-G433; and through U. S. Air Force (Rome Air Development Center) contract AF 30(602)-3340 administered by the IBM Watson Research Center.
References
- 7
- Cited by