A decidable subclass of the minimal Gödel class with identity

1984 ◽  
Vol 49 (4) ◽  
pp. 1253-1261 ◽  
Author(s):  
Warren D. Goldfarb ◽  
Yuri Gurevich ◽  
Saharon Shelah
Keyword(s):  
Decision Problem ◽  
Existential Quantifier ◽  
Quantification Theory

The minimal Gödel class with identity (MGCI) is the class of closed, prenex quantificational formulas whose prefixes have the form ∀x1∀x2∃x3 and whose matrices contain arbitrary predicate letters and the identity sign “=”, but contain no function signs or individual constants. The MGCI was shown undecidable (for satisfiability) in 1983 [Go2]; this both refutes a claim of Gödel's [Gö, p. 443] and settles the decision problem for all prefix-classes of quantification theory with identity.In this paper, we show the decidability of a natural subclass of the MGCI. The formulas in this subclass can be thought of as exploiting only half of the power of the existential quantifier. That is, since an MGCI formula has prefix ∀x1∀x2∃x3, in general its truth in a model requires for any elements a and b, the existence of both a witness for and a witness for . The formulas we consider demand less: they require, for any elements a and b, a witness for the unordered pair {a, b}, that is, a witness either for or for .

Skolem reduction classes

1975 ◽  
Vol 40 (1) ◽  
pp. 62-68 ◽  
Author(s):  
Warren D. Goldfarb ◽  
Harry R. Lewis
Keyword(s):  
Decision Problem ◽  
Atomic Formula ◽  
Complex Situation ◽  
Quantification Theory ◽  
Reduction Class

Among the earliest and best-known theorems on the decision problem is Skolem's result [7] that the class of all closed formulas with prefixes of the form ∀···∀∃···∃ is a reduction class for satisfiability for the whole of quantification theory. This result can be refined in various ways. If the Skolem prefix alone is considered, the best result [8] is that the ∀∀∀∃ class is a reduction class, for Gödel [3], Kalmár [4], and Schütte [6] showed the ∀∀∃···∃ class to be solvable. The purpose of this paper is to describe the more complex situation that arises when (Skolem) formulas are restricted with respect to the arguments of their atomic subformulas. Before stating our theorem, we must introduce some notation.Let x, y1, y2, be distinct variables (we shall use v1, v2, ··· and w1, w2, ··· as metavariables ranging over these variables), and for each i ≥ 1 let Y(i) be the set {y1, ···, yi}. An atomic formula Pv1 ··· vk will be said to be {v1, ···, vk}-based. For any n ≥ 1, p ≥ 1, and any subsets Y1, ··· Yp of Y(n), let C(n, Y1, ···, Yp) be the class of all those closed formulas with prefix ∀y1 ··· ∀yn∃x such that each atomic subformula not containing the variable x is Yi-based for some i, 1 ≤ i ≤ p.

Prefix classes of Krom formulas

1973 ◽  
Vol 38 (4) ◽  
pp. 628-642 ◽  
Author(s):  
Stål O. Aanderaa ◽  
Harry R. Lewis
Keyword(s):  
Decision Problem ◽  
Decision Problems ◽  
Quantification Theory

In this paper we consider decision problems for subclasses of Kr, the class of those formulas of pure quantification theory whose matrices are conjunctions of binary disjunctions of signed atomic formulas. If each of Q1, …, Qn is an ∀ or an ∃, then let Q1 … Qn be the class of those closed prenex formulas with prefixes of the form (Q1x1)… (Qnxn). Our results may then be stated as follows:Theorem 1. The decision problem for satisfiability is solvable for the class ∀∃∀ ∩ Kr.Theorem 2. The classes ∀∃∀∀ ∩ Kr and ∀∀∃∀ ∩ Kr are reduction classes for satisfiability.Maslov [11] showed that the class ∃…∃∀…∀∃…∃ ∩ Kr is solvable, while the first author [1, Corollary 4] showed ∃∀∃∀ ∩ Kr and ∀∃∃∀ ∩ Kr to be reduction classes. Thus the only prefix subclass of Kr for which the decision problem remains open is ∀∃∀∃…∃∩ Kr.The class ∀∃∀ ∩ Kr, though solvable, contains formulas whose only models are infinite (e.g., (∀x)(∃u)(∀y)[(Pxy ∨ Pyx) ∧ (¬ Pxy ∨ ¬Pyu)], which can be satisfied over the integers by taking P to be ≥). This is not the case for Maslov's class ∃…∃∀…∀∃…∃ ∩ Kr, which contains no formula whose only models are infinite ([2] [5]).Theorem 1 was announced in [1, Theorem 4], but the proof sketched there is defective: Lemma 4 (p. 17) is incorrectly stated. Theorem 2 was announced in [9].

On the Gödel class with identity

1981 ◽  
Vol 46 (2) ◽  
pp. 354-364 ◽  
Author(s):  
Warren D. Goldfarb
Keyword(s):  
Recursive Function ◽  
Decision Problem ◽  
Decision Procedure ◽  
Finite Model ◽  
Quantification Theory ◽  
Free Variables ◽  
Primitive Recursive

The Gödel Class is the class of prenex formulas of pure quantification theory whose prefixes have the form ∀y1∀y2∃x1 … ∃xn. The Gödel Class with Identity, or GCI, is the corresponding class of formulas of quantification theory extended by inclusion of the identity-sign “ = ”. Although the Gödel Class has long been kndwn to be solvable, the decision problem for the Gödel Class with Identity is open. In this paper we prove that there is no primitive recursive decision procedure for the GCI, or, indeed, for the subclass of the GCI containing just those formulas with prefixes ∀y1∀y2∃x.Throughout this paper we take quantification theory to include, aside from logical signs, infinitely many k-place predicate letters for each k > 0, but no function signs or constants. Moreover, by “prenex formula” we include only those without free variables. A decision procedure for a class of formulas is a recursive function that carries a formula in the class to 0 if the formula is satisfiable and to 1 if not. A class is solvable iff there exists a decision procedure for it. A class is finitely controllable iff every satisfiable formula in the class has a finite model. Since we speak only of effectively specified classes, finite controllability implies solvability (but not conversely).The GCI has a curious history. Gödel showed the Gödel Class (without identity) solvable in 1932 [4] and finitely controllable in 1933 [5].

Conservative reduction classes of Krom formulas

1982 ◽  
Vol 47 (1) ◽  
pp. 110-130 ◽  
Author(s):  
Stål O. Aanderaa ◽  
Egon Börger ◽  
Harry R. Lewis
Keyword(s):  
Normal Form ◽  
Decision Problem ◽  
Conjunctive Normal Form ◽  
Satisfiability Problem ◽  
Quantification Theory ◽  
Finite Models ◽  
Reduction Class

AbstractA Krom formula of pure quantification theory is a formula in conjunctive normal form such that each conjunct is a disjunction of at most two atomic formulas or negations of atomic formulas. Every class of Krom formulas that is determined by the form of their quantifier prefixes and which is known to have an unsolvable decision problem for satisfiability is here shown to be a conservative reduction class. Therefore both the general satisfiability problem, and the problem of satisfiability in finite models, can be effectively reduced from arbitrary formulas to Krom formulas of these several prefix types.

On the reduction of the decision problem. Third paper. Pepis prefix, a single binary predicate

1950 ◽  
Vol 15 (3) ◽  
pp. 161-173 ◽  
Author(s):  
László Kalmár ◽  
János Surányi
Keyword(s):  
Decision Problem ◽  
Predicate Calculus ◽  
Existential Quantifier ◽  
First Order ◽  
Binary Predicate ◽  
Image Position ◽  
Analogous Theorem ◽  
Order Predicate Calculus ◽  
Predicate Variable

It has been proved by Pepis that any formula of the first-order predicate calculus is equivalent (in respect of being satisfiable) to another with a prefix of the formcontaining a single existential quantifier. In this paper, we shall improve this theorem in the like manner as the Ackermann and the Gödel reduction theorems have been improved in the preceding papers of the same main title. More explicitly, we shall prove theTheorem 1. To any given first-order formula it is possible to construct an equivalent one with a prefix of the form (1) and a matrix containing no other predicate variable than a single binary one.An analogous theorem, but producing a prefix of the formhas been proved in the meantime by Surányi; some modifications in the proof, suggested by Kalmár, led to the above form.

Special Cases of the Decision Problem

1951 ◽  
Vol 49 (22) ◽  
pp. 203-221 ◽  
Author(s):  
Alonzo Church
Keyword(s):  
Decision Problem ◽  
Special Cases

scholarly journals Algebraic Solution to Constrained Bi-Criteria Decision Problem of Rating Alternatives through Pairwise Comparisons

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 303
Author(s):  
Nikolai Krivulin
Keyword(s):  
Decision Problem ◽  
Optimization Problem ◽  
Pareto Frontier ◽  
Sufficient Conditions ◽  
Approximation Error ◽  
Optimal Solution ◽  
Algebraic Solution ◽  
Pairwise Comparisons ◽  
Logarithmic Scale ◽  
Idempotent Algebra

We consider a decision-making problem to evaluate absolute ratings of alternatives from the results of their pairwise comparisons according to two criteria, subject to constraints on the ratings. We formulate the problem as a bi-objective optimization problem of constrained matrix approximation in the Chebyshev sense in logarithmic scale. The problem is to approximate the pairwise comparison matrices for each criterion simultaneously by a common consistent matrix of unit rank, which determines the vector of ratings. We represent and solve the optimization problem in the framework of tropical (idempotent) algebra, which deals with the theory and applications of idempotent semirings and semifields. The solution involves the introduction of two parameters that represent the minimum values of approximation error for each matrix and thereby describe the Pareto frontier for the bi-objective problem. The optimization problem then reduces to a parametrized vector inequality. The necessary and sufficient conditions for solutions of the inequality serve to derive the Pareto frontier for the problem. All solutions of the inequality, which correspond to the Pareto frontier, are taken as a complete Pareto-optimal solution to the problem. We apply these results to the decision problem of interest and present illustrative examples.

Logical Decision Problems and Complexity of Logic Programs

1987 ◽  
Vol 10 (1) ◽  
pp. 1-33
Author(s):  
Egon Börger ◽  
Ulrich Löwen
Keyword(s):  
Fixed Point ◽  
Computational Complexity ◽  
Decision Problem ◽  
Decision Problems ◽  
Complexity Classes ◽  
Logic Programs ◽  
Finite Structures ◽  
Syntactic Restrictions

We survey and give new results on logical characterizations of complexity classes in terms of the computational complexity of decision problems of various classes of logical formulas. There are two main approaches to obtain such results: The first approach yields logical descriptions of complexity classes by semantic restrictions (to e.g. finite structures) together with syntactic enrichment of logic by new expressive means (like e.g. fixed point operators). The second approach characterizes complexity classes by (the decision problem of) classes of formulas determined by purely syntactic restrictions on the formation of formulas.

Modern Quantification Theory

2021 ◽  
Author(s):  
Shizuhiko Nishisato ◽  
Eric J. Beh ◽  
Rosaria Lombardo ◽  
Jose G. Clavel
Keyword(s):  
Quantification Theory
Sign in / Sign up

Export Citation Format

Share Document