Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-22T05:42:29.548Z Has data issue: false hasContentIssue false
  • English
  • Français

The decision problem for formulas with a small number of atomic subformulas

Published online by Cambridge University Press:  12 March 2014

Harry R. Lewis  and
Warren D. Goldfarb
Harry R. Lewis
Affiliation:
Aiken Computation Laboratory, Harvard University, Cambridge, Massachusetts 02138
Warren D. Goldfarb
Affiliation:
Society of Fellows, Harvard University, Cambridge, Massachusetts 02138
Get access Rights & Permissions [Opens in a new window]

Extract

In this paper we consider classes of quantificational formulas specified by restrictions on the number of atomic subformulas appearing in a formula. Little seems to be known about the decision problem for such classes, except that the class whose members contain at most two distinct atomic subformulas is decidable [2]. (We use “decidable” and “undecidable” throughout with respect to satisfiability rather than validity. All undecidable problems to which we refer are of maximal r.e. degree.) The principal result of this paper is the undecidability of the class of those formulas containing five atomic subformulas and with prefixes of the form ∀∃∀…∀. In fact, we show the undecidability of two sub-classes of this class: one (Theorem 1) consists of formulas whose matrices are in disjunctive normal form with two disjuncts; the other (Corollary 1) consists of formulas whose matrices are in conjunctive normal form with three conjuncts. (Theorem 1 sharpens Orevkov's result [8] that the class of formulas in disjunctive normal form with two disjuncts is undecidable.) A second corollary of Theorem 1 shows the undecidability of the class of formulas with prefixes of the form ∀…∀∃, containing six atomic subformulas, and in conjunctive normal form with three conjuncts. These restrictions to prefixes ∀∃∀…∀ and ∀…∀∃ are optimal. For by a result of the first author [5], any class of prenex formulas obtained by restricting both the number of atomic formulas and the number of universal quantifiers is reducible to a finite class of formulas, and so each such class is decidable; and the class of formulas with prefixes ∃…∃∀…∀ is, of course, decidable.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 38 , Issue 3 , September 1973 , pp. 471 - 480
Copyright
Copyright © Association for Symbolic Logic 1973

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.)

References

REFERENCES

[1]Church, A., Introduction to mathematical logic. Vol. I, Princeton University Press, Princeton, New Jersey, 1956.Google Scholar
[2]Dreben, B. S. and Goldfarb, W. D., A systematic treatment of the decision problem (forthcoming).Google Scholar
[3]Gladstone, M. D., Finite models for inequations, this Journal, vol. 31 (1966), pp. 581–592.Google Scholar
[4]Herbrand, J., On the fundamental problem of mathematical logic, Logical writings (Goldfarb, W. D., editor), Harvard University Press, Cambridge, Massachusetts, 1971.CrossRefGoogle Scholar
[5]Lewis, H. R., The decision problem for formulae with a bounded number of atomic sub-formulae. Notices of the American Mathematical Society, vol. 20 (1973), p. A–23.Google Scholar
[6]Maslov, S. Ju., An inverse method of establishing deducibilities in the classical predicate calculus, Soviet Mathematics Doklady, vol. 5 (1964), p. 1420.Google Scholar
[7]Minsky, M., Computation: Finite andinfimte machines, Prentice-Hall, Englewood Cliffs, New Jersey, 1967.Google Scholar
[8]Orevkov, V. P., Two undecidable classes of formulas in classical predicate calculus, Seminars in Mathematics, V. A. Steklov Mathematical Institute, Leningrad, (8), pp. 98–102; Consultants Bureau, New York, 1969.Google Scholar