Janos Surányi. Contributions to the reduction theory of the decision problem. Fifth paper. Ackermann prefix with three universal quantifiers. English with Russian abstract. Acta mathematica Academiae Scientiarum Hungaricae, vol. 2 (1951), pp. 325–335.

1953 ◽  
Vol 18 (3) ◽  
pp. 265-265
Author(s):  
Alonzo Church
Keyword(s):  
Decision Problem ◽  
Reduction Theory ◽  
Universal Quantifiers

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

1973 ◽  
Vol 38 (3) ◽  
pp. 471-480 ◽  
Author(s):  
Harry R. Lewis ◽  
Warren D. Goldfarb
Keyword(s):  
Normal Form ◽  
Decision Problem ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Principal Result ◽  
The Other ◽  
Universal Quantifiers

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.

Sign in / Sign up

Export Citation Format

Share Document