Linear sampling and the ∀∃∀ case of the decision problem

Let Q be the class of closed quantificational formulas ∀x∃u∀yM without identity such that M is a quantifier-free matrix containing only monadic and dyadic predicate letters and containing no atomic subformula of the form Pyx or Puy for any predicate letter P. In [DKW] Dreben, Kahr, and Wang conjectured that Q is a solvable class for satisfiability and indeed contains no formula having only infinite models. As evidence for this conjecture they noted the solvability of the subclass of Q consisting of those formulas whose atomic subformulas are of only the two forms Pxy, Pyu and the fact that each such formula that has a model has a finite model. Furthermore, it seemed likely that the techniques used to show this subclass solvable could be extended to show the solvability of the full class Q, while the syntax of Q is so restricted that it seemed impossible to express in formulas of Q any unsolvable problem known at that time.In 1966 Aanderaa refuted this conjecture. He first constructed a very complex formula in Q having an infinite model but no finite model, and then, by an extremely intricate argument, showed that Q (in fact, the subclass Q2 defined below) is unsolvable ([Aa1], [Aa2]). In this paper we develop stronger tools in order to simplify and extend the results of [Aa2]. Specifically, we show the unsolvability of an apparently new combinatorial problem, which we shall call the linear sampling problem (defined in §1.2 and §2.3). From the unsolvability of this problem there follows the unsolvability of two proper subclasses of Q, which we now define. For each i ≥ 0, let Pi be a dyadic predicate letter and let Ri be a monadic predicate letter.

Download Full-text

The Transition from an Infinite Model of Factors that Determine the System to a Finite Model. The Model of Algebraic Formalization of Risks of Changing the Scenarios of the Long-Term Development of a Smart System of Six Factors on the Example of a Smart University

Smart Innovation, Systems and Technologies - Algebraic Formalization of Smart Systems ◽

10.1007/978-3-319-77051-2_8 ◽

2018 ◽

pp. 137-147

Author(s):

Natalia Serdyukova ◽

Vladimir Serdyukov

Keyword(s):

Finite Model ◽

Smart System ◽

Infinite Model

Download Full-text

Church’s theorem and the decision problem

Routledge Encyclopedia of Philosophy ◽

10.4324/9780415249126-y003-1 ◽

2018 ◽

Author(s):

Rohit Parikh

Keyword(s):

Decision Problem ◽

Combinatorial Problem ◽

Order Logic ◽

First Order Logic ◽

Negative Solution ◽

Great Contribution ◽

Solvable Problem ◽

First Order ◽

Mathematical Definition ◽

Definition Of

Church’s theorem, published in 1936, states that the set of valid formulas of first-order logic is not effectively decidable: there is no method or algorithm for deciding which formulas of first-order logic are valid. Church’s paper exhibited an undecidable combinatorial problem P and showed that P was representable in first-order logic. If first-order logic were decidable, P would also be decidable. Since P is undecidable, first-order logic must also be undecidable. Church’s theorem is a negative solution to the decision problem (Entscheidungsproblem), the problem of finding a method for deciding whether a given formula of first-order logic is valid, or satisfiable, or neither. The great contribution of Church (and, independently, Turing) was not merely to prove that there is no method but also to propose a mathematical definition of the notion of ‘effectively solvable problem’, that is, a problem solvable by means of a method or algorithm.

Download Full-text

The undecidability of entailment and relevant implication

Journal of Symbolic Logic ◽

10.2307/2274261 ◽

1984 ◽

Vol 49 (4) ◽

pp. 1059-1073 ◽

Cited By ~ 73

Author(s):

Alasdair Urquhart

Keyword(s):

Decision Problem ◽

Main Tool ◽

Finite Model ◽

Modular Lattices ◽

Finite Model Property ◽

Von Neumann ◽

Relevant Implication ◽

Decision Methods ◽

Extensive Class ◽

Ticket Entailment

In this paper we show that the propositional logics E of entailment, R of relevant implication and T of ticket entailment are undecidable. The decision problem is also shown to be unsolvable in an extensive class of related logics. The main tool used in establishing these results is an adaptation of the von Neumann coordinatization theorem for modular lattices.Interest in the decision problem for these systems dates from the late 1950s. The earliest result was obtained by Anderson and Belnap who proved that the first degree fragment of all these logics is decidable. Kripke [11] proved that the pure implicational fragments R→ and E→ of R and E are decidable. His methods were extended by Belnap and Wallace to the implication-negation fragments of these systems [3]; Kripke's methods also extend easily to include the implication-conjunction fragments of R and E. Meyer in his thesis [14] extended the result for R to include a primitive necessity operator. He also proved decidable the system R-mingle, an extension of R, and ortho-R (OR), the logic obtained from R by omitting the distribution axiom. Various weak relevant logics are also known to be decidable by model-theoretic proofs of the finite model property (see Fine [5]). Finally, S. Giambrone [7] has solved the decision problem for various logics obtained by the omission of the contraction axiom (A → ⦁ A → B) → ⦁ A → B, including R+ − W (R+ minus contraction). It is worth noting that even where positive results were obtained, the decision methods were usually of a complexity considerably greater than in the case of other nonclassical logics such as intuitionistic logic or modal logic, a fact which already indicates the difficulty of the decision problem.

Download Full-text

On the Gödel class with identity

Journal of Symbolic Logic ◽

10.2307/2273627 ◽

1981 ◽

Vol 46 (2) ◽

pp. 354-364 ◽

Cited By ~ 5

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

Download Full-text

Random models and the Gödel case of the decision problem

Journal of Symbolic Logic ◽

10.2307/2273674 ◽

1983 ◽

Vol 48 (4) ◽

pp. 1120-1124 ◽

Cited By ~ 7

Author(s):

Yuri Gurevich ◽

Saharon Shelah

Keyword(s):

Decision Problem ◽

Finite Model ◽

Probabilistic Argument ◽

First Order ◽

Random Models

AbstractIn a paper of 1933 Gödel proved that every satisfiable first-order ∀2∃* sentence has a finite model. Actually he constructed a finite model in an ingenious and sophisticated way. In this paper we use a simple and straightforward probabilistic argument to establish existence of a finite model of an arbitrary satisfiable ∀2∃* sentence.

Download Full-text

On the Decision Problem for Two-Variable First-Order Logic

Bulletin of Symbolic Logic ◽

10.2307/421196 ◽

1997 ◽

Vol 3 (1) ◽

pp. 53-69 ◽

Cited By ~ 137

Author(s):

Erich Grädel ◽

Phokion G. Kolaitis ◽

Moshe Y. Vardi

Keyword(s):

Computational Complexity ◽

Decision Problem ◽

Order Logic ◽

First Order Logic ◽

Satisfiability Problem ◽

Finite Model ◽

Model Property ◽

Finite Model Property ◽

First Order ◽

Long Time

AbstractWe identify the computational complexity of the satisfiability problem for FO2, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO2 has the finite-model property, which means that if an FO2-sentence is satisiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable FO2-sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO2-sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO2 is NEXPTIME-complete.

Download Full-text