Positive and Monotone Fragments of FO and LTL
Abstract
We study the positive logic on finite words, and its fragments, pursuing and refining the work initiated in [11]. First, we transpose notorious logic equivalences into positive first-order logic: is equivalent to , and its two-variable fragment with (resp. without) successor available is equivalent to with (resp. without) the “next” operator available. This shows that despite previous negative results, the class of -definable languages exhibits some form of robustness. We then exhibit an example of an -definable monotone language on one predicate, that is not -definable, refining the example from [11] with predicates. Moreover, we show that such a counter-example cannot be -definable. Finally, we provide a new example distinguishing the positive and monotone versions of without quantifier alternation. This does not rely on a variant of the previously known counter-example, and witnesses a new phenomenon.
Keywords and phrases:
Positive logic, LTL, separation, first-order, monotoneCategory:
Track B: Automata, Logic, Semantics, and Theory of ProgrammingFunding:
Denis Kuperberg: ANR ReCiProg.Copyright and License:
![[Uncaptioned image]](x1.png)
2012 ACM Subject Classification:
Theory of computation Modal and temporal logics ; Theory of computation Regular languages ; Theory of computation Logic and verificationEditors:
Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele PuppisSeries and Publisher:

1 Introduction
In various contexts, monotonicity properties play a pivotal role. For instance the field of monotone complexity investigates negation-free formalisms, and turned out to be an important tool for complexity in general [7]. From a logical point of view, a sentence is called monotone (with respect to a predicate ) if increasing the set of values where is true in a structure cannot make the evaluation of the formula switch from true to false. This is crucial e.g. when defining logics with fixed points, where the fixed points binders can only be applied to formulas that are monotone in . Logics with fixed points are used in various contexts, e.g. to characterise the class PTime on ordered structures [8, 19], as extensions of linear logic such as MALL [2], or in the -calculus formalism used in automata theory and model-checking [3]. Because of the monotonicity constraint, it is necessary to recognise monotone formulas, and understand whether a syntactic restriction to positive (i.e. negation-free) formulas is semantically complete. Logics on words have also been generalised to inherently negation-free frameworks, such as in the framework of cost functions [4].
This motivates the study of whether the semantic monotone constraint can be captured by a syntactic one, namely the removing of negations, yielding the class of positive formulas. For instance, the formula states that an element labelled is present in the structure. It is both monotone and positive. However, its negation is neither positive nor monotone, since it states the absence of , and increasing the domain where predicate is true in a given structure could make the formula become false.
Lyndon’s preservation theorem [13] states that on arbitrary structures, every monotone formula of First-Order Logic () is equivalent to a positive one ( syntactic fragment). The case of finite structures was open for two decades until Ajtai and Gurevich [1] showed that Lyndon’s theorem does not hold in the finite, later refined by Stolboushkin [17] with a simpler proof. Recently, this preservation property of was more specifically shown to fail already on finite graphs and on finite words by Kuperberg [11], implying the failure on finite structures with a more elementary proof than [1, 17]. However, the relationship between monotone and positive formulas is still far from being understood. On finite words in particular, the positive fragment was shown [11] to have undecidable membership (with input an formula, or a regular language), which could be interpreted as a sign that this class is not well-behaved. This line of research can be placed in the larger framework of the study of preservation theorems in first-order logic, and their behaviour in the case of finite models, see [16] for a survey on preservation theorems.
In this work we will concentrate on finite words, and investigate this “semantic versus syntactic” relationship for fragments of and Linear Temporal Logic (). We will in particular lift the classical equivalence between and [9] to their positive fragments, showing that some of the robustness aspects of are preserved in the positive fragment, despite the negative results from [11]. This equivalence between and is particularly useful when considering implementations and real-world applications, as satisfiability is PSpace-complete while satisfiability is non-elementary. It is natural to consider contexts where specifications in LTL can talk about e.g. the activation of a sensor, but not its non-activation, which would correspond to a positive fragment of LTL. We could also want to syntactically force such an event to be “good” in the sense that if a specification is satisfied when a signal is off at some time, it should still be satisfied when the signal is on instead. It is therefore natural to ask whether a syntactic constraint on the positivity of formulas could capture the semantic monotonicity, in the full setting or in some fragments corresponding to particular kinds of specifications.
We will also pay a close look at the two-variable fragment of and its counterpart. It was shown in [11] that there exists a monotone -definable language that is not definable in positive . We give stronger variants of this counter-example language, and show that such a counter-example cannot be defined in . This is obtained via a stronger result characterising -monotone in terms of positive fragments of bounded quantifier alternation. We also give precise complexity results for deciding whether a regular language is monotone, refining results from [11]. Finally, we provide a counterexample showing that the positive and alternation-free fragment of does not capture all alternation-free monotone languages from .
The goal of this work is to understand at what point the phenomenon discovered in [11] comes into play: what are the necessary ingredients for such a counter-example (-monotone but not positive) to exist? And on the contrary, which fragments of are better behaved, and can capture the monotonicity property with a semantic constraint, and allow for a decidable membership problem in the positive fragment?
Outline and Contributions
We begin by introducing two logical formalisms in Section 2: First-Order Logic (2.1) and Temporal Logic (2.2).
Then, we lift some classical logical equivalences to positive logic in Section 3. First we show that , and are equivalent in Theorem 20. We prove that the fragment with (resp. without) successor predicate is equivalent to with (resp. without) and operators available in Theorem 26 (resp. Corollary 28).
In Section 4, we give a characterisation of monotonicity using monoids (Theorem 29) and we deduce from this an algorithm which decides the monotonicity of a regular language given by a monoid (Section 4.2), completing the automata-based algorithms given in [11]. This leads us to the Proposition 31 which states that deciding the monotonicity of a regular language is in LogSpace when the input is a monoid, while it is - when the input is a DFA. This completes the previous result from [11] showing PSpace-completeness for NFA input.
Finally, we study the relationship between semantic and syntactic positivity in Section 5. We give some refinements of the counter-example from [11] (a regular and monotone language -definable but not definable in ). Indeed, we show that the counter-example can be adapted to with the binary predicate “between” in Proposition 33, and we show that we need only one predicate to find a counter-example in in Proposition 34.
We also consider a characterisation of from Thérien and Wilke [18] stating that is equivalent to where and are fragments of with bounded quantifier alternation. We show that -monotone is characterised by .
We then show that monotone is included in . In other words no counter-example for can be found in (without successor available) in Corollary 36, and leave open the problem of expressive equivalence between and -monotone, as well as decidability of membership in for regular languages (see Open 37).
To conclude, we provide in Section 5.3 a negative answer to this problem in the context of the alternation-free fragment of , providing an example of a monotone language definable in without quantifier alternation, but not definable in the positive fragment of without alternation. This exhibits a new discrepancy between a positive fragment and its monotone counterpart, not relying on previous constructions.
Due to space constraints, some proofs are omitted or only sketched, and can be found in the long version.
2 and
We work with a set of atomic unary predicates , and consider the set of words on alphabet . To describe a language on this alphabet, we use logical formulas. Here we present the different logics and how they can be used to define languages.
2.1 First-order logics
Let us consider a set of binary predicates, , , , , and , which will be used to compare positions in words. We define the subsets of predicates , and , and a generic binary predicate is denoted . As we are going to see, equality can be expressed with other binary predicates in and when we have at least two variables. This is why we do not need to impose that belongs to or . The same thing stands for . Generally, we will always assume that predicates and are expressible.
Let us start by defining first-order logic :
Definition 1.
Let be a set of binary predicates. The grammar of is as follows:
where belongs to .
Closed formulas (those with no free variable) can be used to define languages. Generally speaking, a pair consisting of a word and a function from the free (non-quantified) variables of a formula to the positions of satisfies if satisfies the closed formula obtained from by replacing each free variable with its image by .
Definition 2.
Let , a formula with free variables, , …, , and a word. Let be a function of in . We say that satisfies , and we define by induction on as follows:
-
and we never have ,
-
if ,
-
if ,
-
if ,
-
if ,
-
if (note that we only ask inclusion here),
-
if and ,
-
if or ,
-
if there is of such that we have ,
-
if for any index of , ,
-
if we do not have .
For a closed formula, we simply note .
Here is an example:
Example 3.
The formula describes the set of non-empty words that admit at most one . For example, does not satisfy because two of its letters contain an , but does satisfy .
Remark 4.
The predicates and can be expressed in with three variables. If there are no restriction on variables, in particular if we can use three variables, all binary predicates in can be expressed from those in . Thus, we will consider the whole set of binary predicates available when the number of variables is not constrained, and we will note for or , which are equivalent, and similarly for .
Let us now turn our attention to , the set of first-order formulas without negation. We recall definitions from [11].
Definition 5.
The grammar of is that of without the last constructor, .
Let us also define monotonicity properties, starting with an order on words.
Definition 6.
A word is lesser than a word if and are of the same length, and for any index (common to and ), the -th letter of is included in the -th letter of . When a word is lesser than a word , we note .
Definition 7.
Let be a language. We say that is monotone when for any word such that is lesser than and , we have .
Definition 8.
If is a language, we define its monotone closure . This is the smallest monotone language containing .
Proposition 9 ([11]).
formulas are monotone in unary predicates, i.e. if a model satisfies a formula of , and , then satisfies .
We will also be interested in other logical formalisms, obtained either by restricting , or several variants of temporal logics.
First of all, let us review classical results obtained when considering restrictions on the number of variables. While an formula on words is always logically equivalent to a three-variable formula [9], two-variable formulas describe a class of languages strictly included in that described by first-order logic. In addition, the logic is equivalent to Linear Temporal Logic (see below).
Please note: these equivalences are only true in the framework of word models. In other circumstances, for example when formulas describe graphs, there are formulas with more than three variables that do not admit equivalents with three variables or fewer.
Definition 10.
The set is the subset of formulas using only three different variables, which can be reused. We also define for formulas with three variable and without negation. Similarly, we define and with two variables.
Example 11.
The formula (a formula with one free variable that indicates that the letter labeled by will be followed by a factor of the form ) is an formula, and even an formula: there is no negation, and it uses only three variables, , and , with a reuse of . On the other hand, it does not belong to .
2.2 Temporal logics
Some logics involve an implicit temporal dimension, where positions are identified with time instants. For example, Linear Temporal Logic (LTL) uses operators describing the future, i.e. the indices after the current position in a word. This type of logic can sometimes be more intuitive to manipulate, and present better complexity properties, as explained in the introduction. As mentioned above, is not equivalent to . On the other hand, it is equivalent to , a restriction of to its unary temporal operators.
To begin with, let us introduce , which is equivalent to .
Definition 12.
The grammar of is as follows:
Removing the last constructor gives the grammar of .
This logic does not use variables. To check that a word satisfies an formula, we evaluate the formula at the initial instant, that is to say, the word’s first position. The constructor then describes constraints about the next instant, i.e. the following position in the word. So the word , where is a letter, satisfies if and only if the suffix satisfies . The construction ( Until ) indicates that the formula must be verified at a given point in time and that must be verified until then. We define ( Releases ) as being equal to . This is similar to , but allowing for the option of never being satisfied and being true until the end. The formal definition of the semantics of LTL will be given in a more general setting with additional operators in Definition 16.
Remark 13.
Let us call the formula , for any pair of formulas. The advantage of is that and can be redefined from . The notation for is regularly found in the literature.
is included in Temporal Logic, . While the former speaks of the future, i.e. of the following indices in the word, thanks to , and , the latter also speaks of the past. Indeed, we introduce , (Yesterday, Since) and the respective past analogues of , and .
Definition 14.
The grammar of is as follows:
Similarly, the grammar of is that of extended with , and .
Remark 15.
As for , we will write for , and similarly for and . We also note , , and for , , and respectively. The formulas and mean respectively that the formula will be satisfied at least once in the future ( as Future), and that will always be satisfied in the future ( as Global). Similarly, the operators (as Past) and are the respective past analogues of and . Note that the current position is excluded here while it is included in the general convention (usually ).
When evaluating an or formula on a word , we start by default on the first position . However, we need to define more generally the evaluation of a formula on a word from any given position:
Definition 16.
Let be a formula, a word, and . We define by induction on :
-
and we never have ,
-
if ,
-
if and ,
-
if or ,
-
if ,
-
if there is such that and for all , ,
-
if ,
-
if we do not have ,
-
if ,
-
if there is such that and for all , .
-
if .
We will write as a shorthand for
Finally, let us introduce and , the Unary Temporal Logic and its positive version. The logic does not use the or operator, but only , and to talk about the future. Similarly, we cannot use or to talk about the past.
Definition 17.
The grammar of is as follows:
We define from this grammar by deleting the constructors and .
The grammar of is obtained by deleting the last constructor, and similarly, we define by deleting the negation in .
Remark 18.
In the above definition, and can be redefined with and thanks to negation, but are necessary in the case of .
3 Logical equivalences
When two formulas and are logically equivalent, i.e. admit exactly the same models, we denote it by . Note that a closed formula can be equivalent to an formula, since their models are simply words. Similarly, we can have when is an formula with one free variable (having models of the form ) and is a or formula, this time not using the default first position for semantics. We will use both these ways of stating equivalence in the following.
We want to lift to positive fragments some classical theorems of equivalence between logics, such as these classical results:
Theorem 19 ([9, 5]).
-
and define the same class of languages.
-
and define the same class of languages.
3.1 Equivalences to
We aim at proving the following theorem, lifting classical results from to :
Theorem 20.
The logics , and describe the same languages.
Lemma 21.
The set of languages described by is included in the set of languages recognised by .
The proof is direct, see long version for details. From to , we can interpret in all constructors of .
Let us introduce definitions that will be used in the proof of the next lemma.
Definition 22.
Let be the quantification rank of a formula of defined inductively by:
-
if contains no quantifier then ,
-
if is of the form or then ,
-
if is of the form or then .
Definition 23.
A separated formula is a positive Boolean combination of purely past formulas (not using future operators ), purely present formulas (not using any temporal operators) and purely future formulas (not using past operators ).
We will adapt previous work to show the following auxiliary result:
Lemma 24.
Let be a formula with possible nesting of past and future operators. There is a separated formula of that is equivalent to .
Now we are ready to show the main result of this section:
Lemma 25.
The set of languages described by is included in the set of languages recognised by .
Proof.
We follow [12, Prop. 1, Appendix B.3], which shows a translation from to by induction on the quantification rank. We have adapted this to suit our needs.
Let be an formula with a single free variable. Let us show by induction on that is equivalent to a formula of . Notice that we want to show this regardless of the set of unary predicates used, so we might use the induction hypothesis on formulas with an enriched signature, containing additional unary predicates.
Initialisation.
If is zero, then translates directly into the formula. Indeed, disjunctions and conjunctions translate immediately into . Furthermore, unary predicates of the form translate into and binary predicates trivialize into and (e.g. translates into and into ). For example, translates into .
Heredity.
Suppose that any single free variable formula of quantification rank strictly less than translates into a formula, and is strictly positive.
If is a disjunction or conjunction, we need to transform its various clauses. So, without loss of generality, let us assume that is of the form or .
Let us denote where is a natural number, the letters (which are considered as unary predicates) in applied to the free variable , i.e. ignoring those under the scope of a quantification reusing the variable name .
For any subset of , we note the formula in which each occurrence of is replaced by if belongs to and by otherwise, for any integer of .
We then have the logical equivalence:
We are going to show that the negations in the above formula are optional. Let us note:
Let us then show the equivalence of the formulas and using the monotonicity of as an formula. First, it is clear that any model satisfying satisfies .
Conversely, suppose is satisfied. We then have a subset of such that is satisfied. In particular, according to the values taken by the unary predicates in , there exists a subset of containing such that is satisfied. Now, is monotone in the different predicates . So is also satisfied, and is therefore satisfied.
The rest of the proof is similar to the proof from [12]: the quantifiers on commute with the disjunction on and the conjunction on of the formula . We can therefore fix a subset of and simply consider or . We then replace with a formula that depends only on by replacing each binary predicate of the form with a unary predicate . For example, we can replace , or by a unary predicate , or . We then obtain a formula on an enriched signature with these new unary predicates , or . We can apply to the induction hypothesis, since there is only one free variable. This yields a formula from , equivalent to . Notice that words on which is evaluated also have to specify the values of the unary predicates , or . If is the original set of unary predicates, let . For any , and valuation giving the value of the free variable in , there is a unique such that is the projection of on , and the values of the new predicates in reflect their intended semantic with respect to , e.g. is true if and only if . We then have for all such :
Let be the formula obtained: either or . This formula involves unary predicates of the form . We then use Lemma 24 to transform into a positive Boolean combination of purely past, present and future positive formulas, where predicates trivialize into or , on words of the form . For example, trivializes into in purely past formulas, into in purely present or future formulas.
This completes the induction. From a formula in , we can construct an equivalent formula in . Ultimately, we can return to a future formula. We want to evaluate in , so the purely past formulas, isolated by the separation lemma (Lemma 24), trivialize into or .
Now, to translate a closed formula from to , we can add a free variable by setting . Then, by the above, translates into a formula from , logically equivalent to . Putting together Lemma 21 and Lemma 25 achieves the proof of Theorem 20.
3.2 Equivalences in fragments of
Theorem 26.
The languages described by formulas with one free variable are exactly those described by formulas.
Proof.
First, let us show the to direction. In the proof of Lemma 21, as is classical, three variables are introduced only when translating . By the same reasoning as for , it is clear that translating introduces two variables. It remains to complete the induction of Lemma 21 with the cases of , , and , but again we can restrict ourselves to future operators by symmetry:
-
;
-
.
For the converse direction from to , we draw inspiration from [5, Theorem 1]. This proof is similar to that of [12] used previously in the proof of Lemma 25: we perform a disjunction on the different valuations of unary predicates in one free variable to build a formula with one free variable. However, the proof of Lemma 25 cannot be adapted as is, since it uses the separation theorem which does not preserve the membership of a formula to , see [6, Lem 9.2.2]. However, the article [5] uses negations, and we must therefore construct our own induction case for the universal quantifier that is treated in [5] via negations.
The beginning of the proof is identical to that of Lemma 25, starting with a formula or . Using the same notations, we can reduce to the case of a formula or with no unary predicate applied to in , since all those predicates have been replaced with or according to . Contrarily to the previous proof, we cannot directly replace binary predicates with unary predicates, because this relied on the separation theorem.
Let us consider, as in [5], the position formulas, , , , and , whose set is denoted .
We then have the logical equivalence:
where is obtained from the formula assuming the relative positions of and are described by . The above equivalence holds because forms a partition of the possibilities for the relative positions of and : exactly one of the five formulas from must hold. Since and are the only two variables, any binary predicate involving is a binary predicate involving and (or else it involves only and is trivial). Binary predicates are therefore trivialized according to the position described by .
Example 27.
For and for the position formula , we have . We do not replace the bound variable . We have obtained a formula with one free variable, so we can indeed use the induction hypothesis.
If we started with the existential form , we will use the disjunctive form . This allows us to have the quantifier commute with the disjunction, and obtain . Similarly, if starting with the universal form , we will use the conjunctive form .
We then need to translate and , which we note respectively and , in , for any position formula . We assume fixed in this context so it is omitted from this notation. However, it is important to note that and will still depend on . In each case, we note for the formula obtained by induction from :
This achieves the proof of Theorem 26.
Corollary 28.
The logic is equivalent to .
Proof.
For the right-to-left direction, it suffices to notice that the predicates used to translate the constructors of in the previous proof belong to .
For the left-to-right direction, simply replace the set in Theorem 26 proof by . Once again, we obtain an exhaustive system of mutually exclusive position formulas that allow us to trivialize binary predicates. The proof of Theorem 26 can thus be lifted immediately to this case.
We showed that several classical logical equivalence results can be transposed to their positive variants.
4 Characterisation of monotonicity
So far, we have focused on languages described by positive formulas, from which monotonicity follows. Here, we focus on the monotonicity property and propose a characterisation. We then derive a monoid-based algorithm that decides, given a regular language , whether it is monotone, refining results from [11] focusing on automata-based algorithms.
4.1 Characterisation by monoids
We assume the reader familiar with monoids (see long version for detailed definitions).
We will note a monoid and the syntactic monoid of a regular language and the syntactic order.
Theorem 29.
Let be a regular language, and be its syntactic order. The language is monotone if and only if we have:
where denotes the syntactic morphism onto the syntactic monoid.
Proof.
For the left-to-right direction let be a monotone language and . Let and be two elements of such that . Since is surjective, let and . Then since recognises . So by monotonicity of . Thus . We can conlude that due to the arbitrariness of and .
For the converse direction, suppose that verifies the condition of Theorem 29. We can remark that is compatible with the product of the monoid. Let and be two words such that . Then . By definition of the syntactic order, and since is in the accepting set of the monoid, we must have accepted as well, hence . Thus is monotone.
4.2 An algorithm to decide monotonicity
We immediately deduce from Theorem 29 an algorithm for deciding the monotonicity of a regular language from its syntactic monoid. Indeed, it is sufficient to check for any pair of letters such that is included in whether implies for any pair of elements of the syntactic monoid, where denotes the syntactic morphism onto the syntactic monoid.
This algorithm works for any monoid that recognises through a surjective , not just its syntactic monoid. Indeed, for any monoid, we start by restricting it to to guarantee that is surjective. Then, checking the above implication is equivalent to checking whether for all letters and such that is included in .
This is summarised in the following proposition:
Proposition 30.
There is an algorithm which takes as input a monoid recognising a regular language through a morphism and decides whether is monotone in .
It was shown in [11, Thm 2.5] that deciding monotonicity is PSpace-complete if the language is given by an NFA, and in P if it is given by a DFA.
Recall that in general, the syntactic monoid of a language may be exponentially larger than the minimal DFA of .
We give a more precise result for DFA, and give also a refined complexity result for monoid input.
Proposition 31.
Deciding whether a regular language is monotone is in LogSpace when the input is a monoid while it is when it is given by a DFA.
5 Semantic and syntactic monotonicity
The paper [11, Definition 4.2] exhibits a monotone language definable in but not in . The question then arises as to how simple such a counter-example can be. For instance, can it be taken in specific fragments of , such as ? This section presents a few lemmas that might shed some light on the subject, followed by some conjectures, and a new counterexample to the equivalence between syntactic and semantic monotonicity in the alternation-free fragment of .
5.1 Refinement of the counter-example in the general case
In [11, Sec. 4], the counter-example language that is monotone and -definable but not -definable uses three predicates , and and is as follows:
where ↑ is the monotone closure from Definition 8, and is the letter of containing all three predicates. Any word containing is therefore in , which intuitively corresponds to ignoring any phenomenon involving this letter, while ensuring monotonicity.
It uses the following words to find a strategy for Duplicator in (the positive game that terminates in rounds):
where is greater than , and is just a compact notation for the letter for any predicates and .
This in turns allows to show the failure on Lyndon’s preservation theorem on finite structures [11, Sec. 5]. Our goal in this section is to refine this counter-example to more constrained settings. We hope that by trying to explore the limits of this behaviour, we achieve a better understanding of the discrepancy between monotone and positive.
In Section 5.1.1, we give a smaller fragment of where the counter-example can still be encoded. In Section 5.1.2, we show that the counter-example can still be expressed with a single unary predicate. This means that it could occur for instance in where the specification only talks about one sensor being activated or not.
5.1.1 Using the between predicate
Here we investigate the robustness of the counter-example by restricting the fragment of in which it can be expressed.
First, let us define the “between” binary predicate introduced in [10].
Definition 32 ([10]).
For any unary predicate (not only predicates from but also Boolean combination of them), also designates a binary predicate, called between predicate, such that for any word and any valuation , if and only if there exists an index between and excluded such that .
We denote the set of between predicates and the set of positive between predicates, i.e. positive boolean combination of predicates of the form with .
It is shown in [10] that is strictly less expressive than .
Proposition 33.
There exists a monotone language definable in which is not definable in .
Proof.
We will use the following language:
Indeed, in [11, Sec. 4], it is explained that to recognise in , we need to look for some “anchor positions”. Such positions resolve the possible ambiguity introduced by double letters of the form , that could play two different roles for witnessing membership in . Indeed, if appears in a word, we cannot tell whether it stands for an or a . In contrast, anchor letters have only one possible interpretation. They may be singletons (, , ) or consecutive double letters such as which can only be interpreted one way, here as . For our language , we accept any word containing an anchor of the second kind. This means that in remaining words we will only be interested in singleton anchors. Thus, we need two variables only to locate consecutive anchors and between predicates to check if the letters between the anchors are double letters. See long version for a more detailed description of a formula.
In order to show that is not definable in , it suffices to remark that the argument showing that is not definable in suffices, because the words and used in the -game are still separated by . This shows that is not even definable in so a fortiori it cannot be definable in .
5.1.2 Only one unary predicate
Now, let us show another refinement. We can lift to a counter-example where the set of predicates is reduced to a singleton.
Proposition 34.
As soon as there is at least one unary predicate, there exists a monotone language definable in but not in .
Proof (Sketch).
Suppose reduced to a singleton. Then, is reduced to two letters which we note and with greater than . We will again rely on the proof from [11, Sec. 4]. We will encode each predicate from and a new letter (the separator) into as follows:
We will encode the language as follows:
It remains to verify that is monotone and -definable, and that it is not -definable. The choice of encoding guarantees that this is indeed the case and that we can rely on properties of the original language , without any ambiguities introduced by the encoding. See long version for details.
5.2 Stability through monotone closure
It has been shown by Thérien and Wilke [18] that -definable languages are exactly those that are both -definable and -definable where is the set of -formulas of the form where does not have any quantifier and -formulas are negations of -formulas. Hence, is the set of -formulas in prenex normal form with at most one quantifier alternation. Moreover, Pin and Weil [15] showed that describes the unions of languages of the form , where is a natural integer, are letters from and are subalphabets of .
In the following, we will use as default set of binary predicates for .
Even though we do not know yet whether captures the set of monotone -definable languages, we can state the following theorem:
Theorem 35.
The set of languages definable by both positive -formulas (written ) and positive -formulas (written ) is equal to the set of monotone -definable languages.
Proof (Sketch).
We start by showing that captures the set of monotone -definable languages. This can be done thanks to a syntactic characterisation of -definable languages given by Pin and Weil [15]: a language is -definable if and only if it is a union of languages of the form . Next, we introduce a dual closure operator that allows a finer manipulation of monotone languages. This allows us to lift the previous result to languages. Taken together, these results show that the set of languages definable by both positive -formulas and positive -formulas is exactly the set of monotone -definable languages. See long version for details.
This last result shows how close to capturing monotone -definable languages is. However, it does not seem easy to lift the equivalence to their positive fragments as we did for the other classical equivalences in Section 3. Indeed, the proof from [18] relies itself on the proof of [15] which is mostly semantic while we are dealing with syntactic equivalences.
Since languages in are in particular in , Theorem 35 implies that a counter-example separating -monotone from cannot be in as stated in the following corollary:
Corollary 36.
Any monotone language described by an formula is also described by an formula.
If the monotone closure of a language described by a formula of is in , nothing says on the other hand that is described by a formula of , or even of as the counterexample shows. The monotone closure cannot be defined by an formula. This can be checked using for instance Charles Paperman’s software Semigroup Online [14]. Notice that the software uses the following standard denominations: DA corresponds to , and LDA to .
We leave open the following problem, where can stand either for or for :
Open Problem 37.
-
Is a monotone language definable in if and only if it is definable in ?
-
Is it decidable whether a given regular language is definable in ?
Since we can decide whether a language is definable in and whether it is monotone, the first item implies the second one.
5.3 The alternation-free fragment of
We consider in this section the alternation-free fragment of , and its counterpart, as a first step towards understanding the full logic (recall that we are using as the default set of binary predicates here). The alternation hierarchy of has been studied extensively in recent years (for example in [20]), and might be an angle through which tackling Conjecture 37. The first level of this hierarchy (the alternation-free fragment) enjoys several characterisations. In particular, it corresponds to the variety of languages recognised by -trivial monoids, which entails in particular the decidability of membership for this fragment. We exhibit a counter-example to an analog of Conjecture 37 for this fragment, namely a language that is monotone and definable in without alternation, but not definable in without alternation. This constitutes a new counter-example separating monotonicity from positivity, and the first one that is not relying on the language from [11] but exploits instead a different phenomenon.
We will work over the set of unary predicates , and . To simplify notations, we will think of as the set of letters – representing the empty set and the singleton . The language is defined as the monotone closure of , that is . The language is monotone by definition. It is definable in without alternation: allows to describe the property of having a given subword appearing, or not appearing, in a word, and it is straightforward to give a description of in terms of this kind of property. See long version.
We now show that this language is indeed a counterexample to Conjecture 37 for the logic without alternation:
Proposition 38.
The language is not definable in without alternation.
Proof (Sketch).
We make use of the Ehrenfeucht-Fraïssé game for without alternation (see long version). Fix a natural number , and consider the words and . We show that Duplicator wins , which entails that there is no formula without alternation that can define . The idea is that Spoiler has to play in because is a subword of (so Duplicator can copy the moves of Spoiler); but when Spoiler plays in , Duplicator can try to mimic Spoiler’s moves in the block , and Spoiler can only win by showing that the two words have different sizes, which cannot be done in less that turns. The details of the proof can be found in long version.
Note that this counterexample contradicts the first item of an analog of Conjecture 37 for the alternation-free fragment of , but whether the alternation-free fragment of has decidable membership remains open.
Conclusion
We have investigated how the tension between semantic and syntactic positivity behaves in -definable languages. We paid a close look to how this plays out in relation to monoids, complexity of procedures, , and fragments of . We show that despite earlier negative results from [11] such as undecidabiilty of membership in , this logic retains some robustness, as equivalence with can be obtained, even at the level of specific fragments and . We show that the counter-example language from [11] can be lifted to show that some positive fragments of differ from their monotone counterpart, while for some other fragment, namely alternation-free , we provide a new counter-example relying on a different mechanism. We leave the question open for the fragment, that we consider to be an interesting challenge.
References
- [1] Miklos Ajtai and Yuri Gurevich. Monotone versus positive. J. ACM, 34(4):1004–1015, October 1987. doi:10.1145/31846.31852.
- [2] David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In Nachum Dershowitz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 92–106, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-75560-9_9.
- [3] Julian Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Handbook of Model Checking, pages 871–919. Springer, 2018. doi:10.1007/978-3-319-10575-8_26.
- [4] Thomas Colcombet. Regular Cost Functions, Part I: Logic and Algebra over Words. Logical Methods in Computer Science, Volume 9, Issue 3, August 2013. doi:10.2168/LMCS-9(3:3)2013.
- [5] Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. BRICS Report Series, 4(5), January 1997. doi:10.7146/brics.v4i5.18784.
- [6] Dov M. Gabbay, Ian Hodkinson, and Mark Reynolds. Temporal logic (vol. 1): mathematical foundations and computational aspects. Oxford University Press, Inc., USA, 1994.
- [7] Michelangelo Grigni and Michael Sipser. Monotone complexity. In Poceedings of the London Mathematical Society Symposium on Boolean Function Complexity, pages 57–75, USA, 1992. Cambridge University Press.
- [8] Neil Immerman. Relational queries computable in polynomial time. Information and Control, 68(1):86–104, 1986. doi:10.1016/S0019-9958(86)80029-8.
- [9] Hans Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California Los Angeles, 1968. Published as Johan Anthony Willem Kamp. URL: http://www.ims.uni-stuttgart.de/archiv/kamp/files/1968.kamp.thesis.pdf.
- [10] Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership. Log. Methods Comput. Sci., 16(3), 2020. URL: https://lmcs.episciences.org/6765.
- [11] Denis Kuperberg. Positive first-order logic on words and graphs. Log. Methods Comput. Sci., 19(3), 2023. doi:10.46298/lmcs-19(3:7)2023.
- [12] Denis Kuperberg and Michael Vanden Boom. On the expressive power of cost logics over infinite words. In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming, pages 287–298, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. doi:10.1007/978-3-642-31585-5_28.
- [13] Roger C. Lyndon. Properties preserved under homomorphism. Pacific J. Math., 9(1):143–154, 1959. URL: https://projecteuclid.org:443/euclid.pjm/1103039459.
- [14] Charles Paperman. Semigroup online. URL: https://paperman.name/semigroup/.
- [15] Jean-Éric Pin and Pascal Weil. Polynomial closure and unambiguous product. Theory of Computing Systems, 30:383–422, 1995. URL: https://api.semanticscholar.org/CorpusID:850708.
- [16] Benjamin Rossman. Homomorphism preservation theorems. J. ACM, 55, July 2008. doi:10.1145/1379759.1379763.
- [17] Alexei P. Stolboushkin. Finitely monotone properties. In LICS, San Diego, California, USA, June 26-29, 1995, pages 324–330. IEEE Computer Society, 1995. doi:10.1109/LICS.1995.523267.
- [18] Denis Thérien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation. In Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, STOC ’98, pages 234–240, New York, NY, USA, 1998. Association for Computing Machinery. doi:10.1145/276698.276749.
- [19] Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC ’82, pages 137–146, New York, NY, USA, 1982. Association for Computing Machinery. doi:10.1145/800070.802186.
- [20] Philipp Weis and Neil Immerman. Structure Theorem and Strict Alternation Hierarchy for FO2 on Words. In Thomas Schwentick, Denis Thérien, and Heribert Vollmer, editors, Circuits, Logic, and Games, volume 6451 of Dagstuhl Seminar Proceedings (DagSemProc), pages 1–22, Dagstuhl, Germany, 2007. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/DagSemProc.06451.6.