Hostname: page-component-78c5997874-xbtfd Total loading time: 0 Render date: 2024-11-16T15:06:37.935Z Has data issue: false hasContentIssue false

Some remarks concerning theories with recursively enumerable complements1

Published online by Cambridge University Press:  12 March 2014

Alan Cobham*
Affiliation:
International Business Machines Corporation

Extract

A system formalized within the first order predicate calculus either with or without the identity but without predicate or function variables we call simply a theory. We say that a theory T has a recursively enumerable complement (r.e. Comp.) if the set of all sentences of T not valid in T is recursively enumerable. This is equivalent to saying that there exists an effective, purely mechanical procedure for establishing the non-validity in T of precisely those sentences of T which are in fact not theorems of T. If in addition T is recursively enumerable, that is, if there is an effective procedure for establishing the validity in T of its theorems, then T is decidable. It will be shown here that several well-known results concerning decidable theories can be extended to cover theories with r.e. comps. In this respect it should be observed that there exist theories having r.e. comps. which are not decidable. An example is the theory which has as valid sentences just those which contain a given two-place predicate and which are valid in all non-void finite universes [3], [4].

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1964

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

1

Several of the results in this paper were presented at the Summer Institute of Symbolic Logic, Ithaca, 1957.

References

[1]Robinson, J., Definability and decision problems in arithmetic, this Journal, vol. 14 (1949), pp. 98114.Google Scholar
[2]Tarski, A., Mostowski, A. and Robinson, R. M., Undecidable theories, Amsterdam, 1953.Google Scholar
[3]Trahtenbrot, B. A., Impossibility of an algorithm for the decision problem in finite classes (in Russian), Doklady Akademii Nauk SSSR, n.s., vol. 70 (1950), pp. 569572.Google Scholar
[4]Vaught, R. L., Sentences true in all constructive models, this Journal, vol. 25 (1960), pp. 3953.Google Scholar