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

1983 ◽  
Vol 48 (4) ◽  
pp. 1120-1124 ◽  
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.

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

1997 ◽  
Vol 3 (1) ◽  
pp. 53-69 ◽  
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.

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

1974 ◽  
Vol 39 (3) ◽  
pp. 519-548 ◽  
Author(s):  
Stål O. Aanderaa ◽  
Harry R. Lewis
Keyword(s):  
Decision Problem ◽  
Combinatorial Problem ◽  
Finite Model ◽  
Unsolvable Problem ◽  
Sampling Problem ◽  
Solvable Class ◽  
Full Class ◽  
Infinite Model ◽  
Intricate Argument ◽  
Linear Sampling

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.

Small substructures and decidability issues for first-order logic with two variables

2012 ◽  
Vol 77 (3) ◽  
pp. 729-765 ◽  
Author(s):  
Emanuel Kieroński ◽  
Martin Otto
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Equivalence Relations ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
Surrounding Structure ◽  
Small Model ◽  
Exponential Size

AbstractWe study first-order logic with two variables FO2 and establish a small substructure property. Similar to the small model property for FO2 we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO2 under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO2 has the finite model property and is complete for non-deterministic exponential time, just as for plain FO2. With two equivalence relations, FO2 does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO2 is undecidable.

Church’s theorem and the decision problem

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.

scholarly journals On a Propositional Calculus Whose Decision Problem is Recursively Unsolvable

1970 ◽  
Vol 38 ◽  
pp. 145-152
Author(s):  
Akira Nakamura
Keyword(s):  
Decision Problem ◽  
Propositional Calculus ◽  
Predicate Calculus ◽  
Reduction Theorem ◽  
List Type ◽  
First Order ◽  
Order Predicate Calculus

The purpose of this paper is to present a propositional calculus whose decision problem is recursively unsolvable. The paper is based on the following ideas: (1) Using Löwenheim-Skolem’s Theorem and Surányi’s Reduction Theorem, we will construct an infinitely many-valued propositional calculus corresponding to the first-order predicate calculus.(2) It is well known that the decision problem of the first-order predicate calculus is recursively unsolvable.(3) Thus it will be shown that the decision problem of the infinitely many-valued propositional calculus is recursively unsolvable.

On the reduction of the decision problem. First paper. Ackermann prefix, a single binary predicate

1939 ◽  
Vol 4 (1) ◽  
pp. 1-9 ◽  
Author(s):  
László Kalmár
Keyword(s):  
Decision Problem ◽  
Reduction Process ◽  
The Other ◽  
First Order ◽  
Other Hand ◽  
Special Cases ◽  
Binary Predicate ◽  
Ternary Variables ◽  
Order Predicate Calculus ◽  
Predicate Variable

1. Although the decision problem of the first order predicate calculus has been proved by Church to be unsolvable by any (general) recursive process, perhaps it is not superfluous to investigate the possible reductions of the general problem to simple special cases of it. Indeed, the situation after Church's discovery seems to be analogous to that in algebra after the Ruffini-Abel theorem; and investigations on the reduction of the decision problem might prepare the way for a theory in logic, analogous to that of Galois.It has been proved by Ackermann that any first order formula is equivalent to another having a prefix of the form(1) (Ex1)(x2)(Ex3)(x4)…(xm).On the other hand, I have proved that any first order formula is equivalent to some first order formula containing a single, binary, predicate variable. In the present paper, I shall show that both results can be combined; more explicitly, I shall prove theTheorem. 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.2. Of course, this theorem cannot be proved by a mere application of the Ackermann reduction method and mine, one after the other. Indeed, Ackermann's method requires the introduction of three auxiliary predicate variables, two of them being ternary variables; on the other hand, my reduction process leads to a more complicated prefix, viz.,(2) (Ex1)…(Exm)(xm+1)(xm+2)(Exm+3)(Exm+4).

Some Aspects of Model Theory and Finite Structures

2002 ◽  
Vol 8 (3) ◽  
pp. 380-403 ◽  
Author(s):  
Eric Rosen
Keyword(s):  
Computer Science ◽  
Complexity Theory ◽  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Finite Model ◽  
Finite Model Theory ◽  
First Order ◽  
Single Sentence ◽  
Finite Structures

Model theory is concerned mainly, although not exclusively, with infinite structures. In recent years, finite structures have risen to greater prominence, both within the context of mainstream model theory, e.g., in work of Lachlan, Cherlin, Hrushovski, and others, and with the advent of finite model theory, which incorporates elements of classical model theory, combinatorics, and complexity theory. The purpose of this survey is to provide an overview of what might be called the model theory of finite structures. Some topics in finite model theory have strong connections to theoretical computer science, especially descriptive complexity theory (see [26, 46]). In fact, it has been suggested that finite model theory really is, or should be, logic for computer science. These connections with computer science will, however, not be treated here.It is well-known that many classical results of ‘infinite model theory’ fail over the class of finite structures, including the compactness and completeness theorems, as well as many preservation and interpolation theorems (see [35, 26]). The failure of compactness in the finite, in particular, means that the standard proofs of many theorems are no longer valid in this context. At present, there is no known example of a classical theorem that remains true over finite structures, yet must be proved by substantially different methods. It is generally concluded that first-order logic is ‘badly behaved’ over finite structures.From the perspective of expressive power, first-order logic also behaves badly: it is both too weak and too strong. Too weak because many natural properties, such as the size of a structure being even or a graph being connected, cannot be defined by a single sentence. Too strong, because every class of finite structures with a finite signature can be defined by an infinite set of sentences. Even worse, every finite structure is defined up to isomorphism by a single sentence. In fact, it is perhaps because of this last point more than anything else that model theorists have not been very interested in finite structures. Modern model theory is concerned largely with complete first-order theories, which are completely trivial here.

scholarly journals A decision problem for varieties of commutative semigroups

1993 ◽  
Vol 47 (3) ◽  
pp. 457-464
Author(s):  
W.L. Cao
Keyword(s):  
Decision Problem ◽  
Commutative Semigroups ◽  
First Order ◽  
Finite Set ◽  
Semigroup Identities

For a first order formula P: ∀x1, …, ∀xn, ∃y1, …, ∃ym (u(x1, …, xn, y1, …, ym) ≡ v(x1, …, xn, y1, …, ym)) where u and v are two words on the alphabet {x1, …, xn, y1, …, ym}, and a finite set E of semigroup identities with xy ≡ yx in it, we prove that it is decidable whether P follows from E, that is whether all the semigroups in the variety defined by E satisfy P.

Simulating polyadic modal logics by monadic ones

2003 ◽  
Vol 68 (2) ◽  
pp. 419-462 ◽  
Author(s):  
George Goguadze ◽  
Carla Piazza ◽  
Yde Venema
Keyword(s):  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
First Order Definability

AbstractWe define an interpretation of modal languages with polyadic operators in modal languages that use monadic operators (diamonds) only. We also define a simulation operator which associates a logic Λsim in the diamond language with each logic Λ in the language with polyadic modal connectives. We prove that this simulation operator transfers several useful properties of modal logics, such as finite/recursive axiomatizability, frame completeness and the finite model property, canonicity and first-order definability.

The decision problem for standard classes

1976 ◽  
Vol 41 (2) ◽  
pp. 460-464 ◽  
Author(s):  
Yuri Gurevich
Keyword(s):  
Decision Problem ◽  
Predicate Logic ◽  
Order Theory ◽  
First Order ◽  
First Order Theory

The standard classes of a first-order theory T are certain classes of prenex T-sentences defined by restrictions on prefix, number of monadic, dyadic, etc. predicate variables, and number of monadic, dyadic, etc. operation variables. In [3] it is shown that, for any theory T, (1) the decision problem for any class of prenex T-sentences specified by such restrictions reduces to that for the standard classes, and (2) there are finitely many standard classes K1, …, Kn such that any undecidable standard class contains one of K1, …, Kn. These results give direction to the study of the decision problem.Below T is predicate logic with identity and operation variables. The Main Theorem solves the decision problem for the standard classes admitting at least one operation variable.

Sign in / Sign up

Export Citation Format

Share Document