Decision problems for multiple successor arithmetics
- 1 June 1966
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 31 (2) , 182-190
- https://doi.org/10.2307/2269809
Abstract
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.Keywords
This publication has 3 references indexed in Scilit:
- Rekursive WortfunktionenMathematical Logic Quarterly, 1960
- Weak Second‐Order Arithmetic and Finite AutomataMathematical Logic Quarterly, 1960
- Concatenation as a basis for arithmeticThe Journal of Symbolic Logic, 1946