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.

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.

Decidability of cylindric set algebras of dimension two and first-order logic with two variables

1999 ◽  
Vol 64 (4) ◽  
pp. 1563-1572 ◽  
Author(s):  
Maarten Marx ◽  
Szabolcs Mikulás
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Universal Theory ◽  
Finite Model ◽  
Finite Model Property ◽  
First Order ◽  
Combinatorial Theorem ◽  
Finite Base ◽  
Dimension 2 ◽  
Cylindric Set Algebras

AbstractThe aim of this paper is to give a new proof for the decidability and finite model property of first-order logic with two variables (without function symbols), using a combinatorial theorem due to Herwig. The results are proved in the framework of polyadic equality set algebras of dimension two (Pse2). The new proof also shows the known results that the universal theory of Pse2 is decidable and that every finite Pse2 can be represented on a finite base. Since the class Cs2 of cylindric set algebras of dimension 2 forms a reduct of Pse2, these results extend to Cs2 as well.

On the Restraining Power of Guards

1999 ◽  
Vol 64 (4) ◽  
pp. 1719-1742 ◽  
Author(s):  
Erich Grädel
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Finite Model ◽  
Model Property ◽  
Tree Model ◽  
First Order ◽  
Bounded Number ◽  
Decidable Classes ◽  
Guarded Fragment ◽  
Almost All

AbstractGuarded fragments of first-order logic were recently introduced by Andréka, van Benthem and Németi; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable fragments of first-order logic.Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the guarded fragment (GF) and the loosely guarded fragment (LGF) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is Exptime-complete. We further establish a tree model property for both the guarded fragment and the loosely guarded fragment, and give a proof of the finite model property of the guarded fragment.It is also shown that some natural, modest extensions of the guarded fragments are undecidable.

scholarly journals First-Order Logic with Two Variables and Unary Temporal Logic

1997 ◽  
Vol 4 (5) ◽  
Author(s):  
Kousha Etessami ◽  
Moshe Y. Vardi ◽  
Thomas Wilke
Keyword(s):  
Computational Complexity ◽  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Model Property ◽  
First Order ◽  
The Past ◽  
Small Model ◽  
Input Formula

We investigate the power of first-order logic with only two variables over<br />omega-words and finite words, a logic denoted by FO2. We prove that FO2 can<br />express precisely the same properties as linear temporal logic with only the unary temporal operators: “next”, “previously”, “sometime in the future”, and “sometime in the past”, a logic we denote by unary-TL. Moreover, our translation from FO2 to unary-TL converts every FO2 formula to an equivalent unary-TL formula that is at most exponentially larger, and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is optimal.<br />While satisfiability for full linear temporal logic, as well as for<br />unary-TL, is known to be PSPACE-complete, we prove that satisfiability<br />for FO2 is NEXP-complete, in sharp contrast to the fact that satisfiability<br />for FO3 has non-elementary computational complexity. Our NEXP time<br />upper bound for FO2 satisfiability has the advantage of being in terms of<br />the quantifier depth of the input formula. It is obtained using a small model property for FO2 of independent interest, namely: a satisfiable FO2 formula has a model whose “size” is at most exponential in the quantifier depth of the formula. Using our translation from FO2 to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.

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.

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.

y = 2x VS. y = 3x

1997 ◽  
Vol 62 (2) ◽  
pp. 661-672 ◽  
Author(s):  
Alexei Stolboushkin ◽  
Damian Niwiński
Keyword(s):  
Circuit Complexity ◽  
Order Logic ◽  
First Order Logic ◽  
Linear Ordering ◽  
Finite Model ◽  
Logical Relation ◽  
Open Problems ◽  
First Order ◽  
Standing Question

AbstractWe show that no formula of first order logic using linear ordering and the logical relation y = 2x can define the property that the size of a finite model is divisible by 3. This answers a long-standing question which may be of relevance to certain open problems in circuit complexity.

Finite Variable Logics in Descriptive Complexity Theory

1998 ◽  
Vol 4 (4) ◽  
pp. 345-398 ◽  
Author(s):  
Martin Grohe
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Complexity Classes ◽  
Finite Model ◽  
Polynomial Space ◽  
Finite Model Theory ◽  
First Order ◽  
First Order Theory ◽  
Finite Structures

Throughout the development of finite model theory, the fragments of first-order logic with only finitely many variables have played a central role. This survey gives an introduction to the theory of finite variable logics and reports on recent progress in the area.For each k ≥ 1 we let Lk be the fragment of first-order logic consisting of all formulas with at most k (free or bound) variables. The logics Lk are the simplest finite-variable logics. Later, we are going to consider infinitary variants and extensions by so-called counting quantifiers.Finite variable logics have mostly been studied on finite structures. Like the whole area of finite model theory, they have interesting model theoretic, complexity theoretic, and combinatorial aspects. For finite structures, first-order logic is often too expressive, since each finite structure can be characterized up to isomorphism by a single first-order sentence, and each class of finite structures that is closed under isomorphism can be characterized by a first-order theory. The finite variable fragments seem to be promising candidates with the right balance between expressive power and weakness for a model theory of finite structures. This may have motivated Poizat [67] to collect some basic model theoretic properties of the Lk. Around the same time Immerman [45] showed that important complexity classes such as polynomial time (PTIME) or polynomial space (PSPACE) can be characterized as collections of all classes of (ordered) finite structures definable by uniform sequences of first-order formulas with a fixed number of variables and varying quantifier-depth.

A Modal Logic for Similarity Relations in Pawlak Knowledge Representation Systems

1991 ◽  
Vol 15 (1) ◽  
pp. 61-79
Author(s):  
Dimiter Vakarelov
Keyword(s):  
Modal Logic ◽  
Knowledge Representation ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
Similarity Relations ◽  
Representation Systems ◽  
Knowledge Representation Systems

One of the main results of the paper is a characterization of certain kind similarity relations in Pawlak knowledge representation systems by means of first order sentences. As an application we obtain a complete finite axiomatization of the corresponding poly modal logic, called in the paper MLSim. It is proved that MLSim possesses finite model property and is decidable.

scholarly journals A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes

2017 ◽  
Vol 28 (4) ◽  
pp. 508-532 ◽  
Author(s):  
PAOLO BOTTONI ◽  
DANIELE GORLA ◽  
STEFANO KASANGIAN ◽  
ANNA LABELLA
Keyword(s):  
Temporal Logic ◽  
Computational Models ◽  
Logical Structure ◽  
Order Logic ◽  
First Order Logic ◽  
Equivalence Relations ◽  
First Order ◽  
Concurrent Processes ◽  
The Difference ◽  
Algebraic Modelling

The study of algebraic modelling of labelled non-deterministic concurrent processes leads us to consider a category LB, obtained from a complete meet-semilattice B and from B-valued equivalence relations. We prove that, if B has enough properties, then LB presents a two-fold internal logical structure, induced by two doctrines definable on it: one related to its families of subobjects and one to its families of regular subobjects. The first doctrine is Heyting and makes LB a Heyting category, the second one is Boolean. We will see that the difference between these two logical structures, namely the different behaviour of the negation operator, can be interpreted in terms of a distinction between non-deterministic and deterministic behaviours of agents able to perform computations in the context of the same process. Moreover, the sorted first-order logic naturally associated with LB can be extended to a modal/temporal logic, again using the doctrinal setting. Relations are also drawn to other computational models.

Sign in / Sign up

Export Citation Format

Share Document