The main motivation for this work is the open question of decidability of the satisfiability problem for the two-variable fragment of first-order logic, ℱ 2, with one transitive relation. The problem can be reduced to the corresponding problem when the transitive relation is required to be a partial order. It is known that its finite satisfiability problem is decidable but the decidability of the general satisfiability problem has been resolved only for restricted variants. More precisely, the problem is decidable for the fragment with transitive witnesses in which existential quantifiers are required to be guarded by transitive atoms, a property in line with the standard translation of modal logic into first-order logic. We study the 'complementary' fragment with free witnesses where formulas, when written in negation normal form, contain existential quantifiers applied only to conjunctions of the form ∼ ∧ , where ∼ means that and are not comparable by the order. We show that ℱ 2 with a partial order and free witnesses is not locally finite. On the positive side, we show that the logic enjoys the finite antichain property that we believe is a crucial step towards showing decidability of its satisfiability problem. We also identify minimal syntactic restrictions needed to retain the finite model property.
over structures with one transitive and one equivalence relation [5], and in case of ℱ ℒ2 it sufices that one of the three transitive relation is an equality [6]. These undecidability results come mainly from the possible interactions between the transitive relations. When such interactions are restricted, decidability is retained even in the presence of arbitrarily many transitive relations, as in the guarded fragment with transitive guards, where transitive atoms are only allowed in guard positions [7].
On the positive side, ℱ 2 with one equivalence relation has the finite model property, and its satisfiability (= finite satisfiability) problem is NExpTime-complete [8]; ℱ 2 with two equivalence relations lacks the finite model property, but its satisfiability and finite satisfiability problems are both 2-NExpTime-complete [9].
When the distinguished predicates are required to be interpreted as linear orders, the picture is not fully transparent, as not all known complexity bounds are tight. Specifically, the satisfiability and finite satisfiability problems for ℱ 2 together with one linear order are both NEXPTIME-complete [10]; the ifnite satisfiability problem for ℱ 2 together with two linear orders is in 2-NExpTime [11] (falling to ExpSpace when all undistinguished predicates are unary [12]). Decidability of the satisfiability problem for ℱ 2 with two linear orders was shown recently using an automata based approach by Toruńczyk and Zeume [13]. More precisely, the paper shows decidability of the countable satisfiability problem for two-variable logic in the presence of a tree order, a linear order, and arbitrary atoms that are definable from the tree order using monadic second-order formulas.
Turning towards transitive relations the following is known. The satisfiability problem for ℱ 2 with one transitive relation is 2-ExpTime-complete [14]. Both the satisfiability and the finite satisfiability problems for ℱ ℒ—the full fluted fragment—with one transitive relation remain decidable in the presence of equality and arbitrarily many undistinguished relations [6].
The case that is not yet fully understood is ℱ 2 with one transitive relation, ℱ 21T. It is known that its finite satisfiability problem is decidable in 3-NExpTime [15] but the decidability of the general satisfiability problem has been resolved only for restricted variants. As mentioned above, the problem is decidable for ℱ 2 with one transitive relation. Moreover, decidability of the satisfiability problem follows also for ℱ 2 with one partial order, as (ir)reflexivity and antisymmetry of a binary relation are two-variable guarded properties. Decidability of the satisfiability problem is also known for ℱ 2 with one linear order or with one tree order but the case of any transitive relation seems to be more intricate.
In 2013 it was advertised that Sat(ℱ 21T) is decidable [16] but later it was discovered [17] that the
proof works only for the fragment with transitive witnesses in which existential quantifiers are required
to be guarded by transitive atoms, a property in line with the standard translation of modal logic into
ifrst-order logic. We remark that the infinity axiom (
In this paper we study the fragment ℱ 21T with free witnesses in which formulas, when written in negation normal form, contain existential quantifiers applied only to conjunctions of the form ¬ ∧ ¬ ∧ , enforcing that and are incomparable by . We note that this pattern is neither guarded nor fluted. The logic can be seen as complementary to ℱ 21T with transitive witnesses.
Models for ℱ 21T-formulas, taking into account the interpretation of the transitive relation, can be seen as partitioned into cliques. In [15] it was observed that this logic enjoys the small clique property: every satisfiable formula has a model in which the size of cliques is bounded. This property allows one to reduce the (finite) satisfiability problem for ℱ 21T to the (finite) satisfiability problem for ℱ 2 with one partial order encoding cliques by single elements satisfying some new unary predicates and connection types between cliques by pairs of elements satisfying new binary predicates. Hence, in the remaining part of the paper we concentrate on ℱ 21PO, the two-variable fragment of first-order logic with one partial order, and its subfragments.
Regarding expressive power it turns out that ℱ 21PO is able not only to enforce infinite models but also infinite antichains (cf. examples in [ 15, 17]). When restricting attention to the fragment with free witnesses, the finite model property is also lost [ 17]. However, as we show, the subfragment enjoys the ifnite antichain property : every satisfiable formula has a model in which the size of every antichain is exponentially bounded with respect to the length of the formula. The proof shows actually a bit more: every satisfiable formula has a model with a universe forming a simple block structure; the universe can be partitioned into a bounded number of chains consisting of small blocks containing elements of the same one-type. Elements inside the blocks are incomparable, and the partial order is induced by the order on the blocks. We believe that the finite antichain property will be crucial to show decidability. Notably, known undecidability proofs for elementary modal logics and for fragments of two-variable ifrst-order logic usually encode variants of the tiling problems that are based on two-dimensional grids having unbounded antichains.
We also illustrate the expressive power of ℱ 21PO with free witnesses, showing that in this logic one can write formulas enforcing models that are not locally finite. (A structure is locally finite if for any two elements , of its domain, the interval (, ) consisting of elements between and is finite.) We provide a formula using only unary undistinguished predicates, each of whose model embeds a copy of Z ( depends on the size of the signature). Such structures, for any >1, have infinitely many infinite intervals. Moreover, we identify minimal syntactic restrictions on the universal part of formulas in the logic that allow us to rescue the finite model property.
The paper is structured as follows. Section 2 contains the necessary preliminaries. The proof that the logic ℱ 21PO with free witnesses is not locally finite is given in Section 3. The finite antichain property of the logic is established in Section 4 and the restrictions needed to retain the finite model property in Section 5. We conclude with some directions for future research.
Related work. Partially related is the research on logics for data words and data trees that can be seen as logics over signatures consisting of unary predicates corresponding to data values and (at least) two distinguished binary predicates: an equivalence relation used to compare data values and the linear order for words or the tree order relation(s) for trees, see e.g. [18, 19]. However, in these papers the structures (words or trees) are finite and, hence, the results concern only the finite satisfiability problem.
More closely related seems to be the research on automata on various classes of infinite partial orders, in particular, on pomsets (i.e. labelled partially ordered sets) investigated in the area of modelling concurrent systems. Decidability of the satisfiability problem for logics over these classes is often established by showing decidability of non-emptiness of the corresponding automata. This research contains the study of series-parallel pomsets, also called N-free pomsets, originated by [20, 21] for ifnite graphs, generalized to width-bounded infinite graphs in [ 22], scattered and countable posets in [23, 24], and to synchronized series-parallel graphs in [25]. Positive results are obtained usually in the presence of additional assumptions on the structures such as bounded-width, scattered, well-ordered, ifnite antichains. Since the structures enforced by ℱ 21PO-sentences are not necessarily N-free, the branching automata introduced for such structures cannot be directly applied to recognize models of the logics we are concerned with in this article.
Somewhat related is also research on certain modal logics. For instance, Humberstone [26] and Goranko [27] study the bimodal logic of inaccessible worlds determined by complementary frames of the form ⟨, , 2− ⟩. In the logic the standard modal operator [ ] is used for worlds accessible by the relation , and a second modal operator [] is used for inaccessible worlds: [] holds at a world , if is true in all worlds which are not accessible from via . This condition is not expressible in guarded logic but it is expressible in ℱ 2 and in ℱ ℒ. Decidability of both the global and the local satisfiability problem for the bimodal logic of inaccessible worlds over transitive frames can be inferred from the above mentioned decidability of ℱ ℒ with one transitive relation [6].
We employ standard terminology and notation from model theory. Structures are denoted by (possibly decorated) fraktur letters A, B, and their domains by the corresponding Roman letters. Where a structure is clear from context, we frequently equivocate between predicates and their realizations, thus writing, for example, in place of the technically correct A. If A is a structure over a relational signature and ⊆ , then A↾ denotes the (induced) substructure of A with the universe .
Let (, <) be a poset, where < denotes a strict partial order, i.e. a binary relation that is irreflexive and transitive. Elements , ∈ are said to be comparable if either < or < . Elements , ∈ are said to be incomparable, denoted ∼ , if they are not comparable and distinct. An element ∈ is maximal, if there is no element ∈ such that < .
Let ∈ and ⊆ . We write < ( < ) if for every ∈ we have < ( < ). For subsets , ′ ⊆ we write < ′ if < ′ holds for every ∈ and ′ ∈ ′. We also write ∼ ′ if ̸< ′ and ′ ̸< hold.
A set ⊆ is an antichain, if all elements of are mutually incomparable; is a chain, if the partial order restricted to is total. An element ∈ is an upper bound of if for every ∈ , = ∨ < . For any , ∈ we define (, ) = { ∈ | < < } as the interval of (, ). A poset (, <) has the finite antichain property if every antichain in is finite; it is locally finite , if for every , ∈ the interval (, ) is finite.
We apply the above terminology to structures interpreting a signature in which one distinguished relation is a partial order < in a natural way. For instance, let A be a -structure and , ⊆ . We write <A , if for every ∈ , ∈ , A |= < . We say is a chain in A, if for every , ∈ , A |= = ∨ < ∨ < . We say is an antichain in A, if for every , ∈ , A |= = ∨ ∼ .
We say that a logic ℒ interpreting a partial order has the finite antichain property if every satisfiable formula of ℒ has a model that contains no infinite antichain. We say that ℒ is locally finite , if every satisfiable formula of ℒ has a model that contains no infinite intervals. Obviously, when ℒ enjoys the ifnite model property then it is also locally finite and enjoys the finite antichain property.
We denote by ℱ 2 the two-variable fragment of first-order logic (with equality) over relational signatures. As predicates having arity other than 1 or 2 add no efective expressive power in the context of ℱ 2 and individual constants add no efective expressive power given the presence of the equality predicate, we shall take all signatures to consist only of unary and binary predicates.
By ℱ 21T, we understand the set of ℱ 2-formulas over any signature = 0 ∪ { }, where is a distinguished binary predicate letter. The semantics for ℱ 21T is as for ℱ 2, subject to the restriction that is always interpreted as a transitive relation. When the distinguished predicate is additionally required to be irreflexive and antisymmetric (i.e. a strict partial order), we denote the corresponding set of ℱ 2-formulas by ℱ 21PO. Note that the properties of a binary relation to be irreflexive and antisymmetric are two-variable formulas, hence ℱ 21PO is in fact a fragment of ℱ 21T. Finally, we define ℱ 21PO to be the subset of ℱ 21PO in which no binary predicates other than = and appear. When working with ℱ 21PO and its fragments we often replace the predicate letter by the more intuitive symbol <, written in infix notation.
Crucial for this paper are two restrictions of ℱ 21T depending on how the existential quantifiers are used; no restrictions are imposed on using universal quantifiers. The fragment with transitive witnesses, ℱ 21T, consists of the formulas of ℱ 21T where, when written in negation normal form, existential quantifiers are ‘guarded’ by transitive atoms, i.e. they are applied to formulas with two free variables only of the form (, ) ∧ , where (, ) is one of the conjunctions: ∧ , ∧ ¬ , or ∧ ¬ , and ∈ ℱ 21T. Similarly, the fragment with free witnesses, ℱ 21T, consists of these formulas where, when written in negation normal form, existential quantifiers are applied to formulas with two free variables only of the form ¬ ∧ ¬ ∧ with ∈ ℱ 21T. In case of ℱ 21PO the corresponding fragments are denoted by ℱ 21PO and ℱ 21PO.
As an example, consider the formula ∀∃ . Strictly speaking, the existential quantifier does not
comply to any of the patterns mentioned above. However, using standard first-order tautologies, the
subformula ∃ can be replaced by a disjunction of two formulas in ℱ 21T. Hence, the infinity
axiom (
In previous work on ℱ 2, several variants of the standard Scott normal form have been introduced that allow one to reduce the satisfiability problem to the satisfiability problem for formulas in the normal form. They are usually defined as a conjunction of sentences in prenex normal form with quantifier prefixes ∀∀ and ∀∃. Before we recall the ones useful for this paper we introduce some more notions.
Let be any relational signature. A -literal is a formula of the form ¯ or ¬ ¯, where ¯ is an -tuple of variables and is a predicate of arity from . An (atomic) 1-type is a maximal consistent set of -literals containing only one variable and an (atomic) 2-type is a maximal consistent set of -literals containing two variables and and featuring the formula ̸= . We say that for a structure A some element ∈ realizes a 1-type when is the unique 1-type such that A |= []; we denote this 1-type by tpA[]. Similarly, we say that two distinct elements , ∈ realize a 2-type when is the unique 2-type such that A |= [, ]; we denote this 2-type by tpA[, ]. In addition, let be the set of all possible 1-types in and let be the set of all possible 2-types in . Observe that both and are exponentially bounded in | |. For a given -structure A, let A be the set of all 1-types realized in A and let A be the set of all 2-types realized in A. Moreover, for each 1-type realized in A, define as the set of all elements in which realize .
Below we recall the normal forms from [15] tailored especially for the fragments we exploit in this paper. We employ the abbreviations: ≡ (, ) := ∧ ∧ ̸= , <(, ) := ∧ ¬ ∧ ̸= , ∼ (, ) := ¬ ∧ ¬ ∧ ̸= , >(, ) := ¬ ∧ ∧ ̸= .
Definition 1. A formula of ℱ 21T (or of ℱ 21PO) is said to be in transitive normal form if it conforms to the pattern ⋀︁
⋀︁
=1 ∈{∼ ,<,>,≡}
∀ (, → ∃ ((, ) ∧ ,(, ))),
(
Without loss of generality we assume that an ℱ 21PO-formula in transitive normal form features only ∀∃-conjuncts with ∈ {∼ , <, >}. Indeed, when is a strict partial order, a formula ∀∃ ( () → ≡ (, ) ∧ (, )) is only a complicated way of writing the logical constant false.
Additionally, normal form formulas of ℱ 21PO feature no conjuncts with ∼ , and normal form formulas of ℱ 21PO feature only ∀∃-conjuncts with ∼ . So, denoting the transitive relation by the symbol < and employing the abbreviation
∼ := ¬( < ) ∧ ¬( < ) ∧ ̸= ,
any ℱ 21PO-formula in transitive normal form (
Lemma 1 ([15], Lemma 5.2). Let be an ℱ 21T-formula. There exists an ℱ 21T-formula * in transitive normal form such that: (i) |= * → ; (ii) every model of can be expanded to a model of * ; and (iii) the length of * is bounded polynomially with respect to the length of .
In case of ℱ 21PO one more normal form has been introduced in [15] to simplify reasoning concerning decidability of the finite satisfiability problem of the logic. We reuse the form with a slight modification so that it works for all domains not only finite ones.
Definition 2. A formula of ℱ 21PO is said to be in basic normal form if it is a conjunction of basic formulas of the form ∀( () → ∀( () → = )) ∀( () → ∀( () ∧ ̸= → ∼ )) ∀( () → ∀( () → ∼ )) ∀( () → ∀( () → < )) ∀( () → ∀( () → < ∨ ∼ )) ∀( () → ∀( () ∧ ̸= → ( < ∨ < ))) ∀( () → ∀( () ∧ ̸= → ( < ∨ < ))) ∀( () → ∃( < ∧ ())) ∀( () → ∃( < ∧ ())) ∀( () → ∃( ∼ ∧ ())) ∀. () ∃. () (B1) (B2a) (B2b) (B3) (B4) (B5a) (B5b) (B6) (B7) (B8) (B9) (B10) where , are distinct 1-types and is a quantifier-free formula not featuring =, <, ∼ .
Our modification concerns conjuncts (B6) and (B7) that in [15] had the forms ∀( () → ∃( () ∧ ¬ () ∧ < )) and, respectively, ∀( () → ∃( () ∧ ¬ () ∧ < )). These forms could be obtained by considering extremal elements satisfying the 1-type that in infinite structures might not exist. We also omit the conjuncts (B1b): ∀( () → ∀( () → = )) that for distinct 1-types and are equivalent to the logical constant false and can be expressed anyway.
The following Lemma can be proved exactly as Lemma 3.1 from [15].
Lemma 2. Let be an ℱ 21PO-formula. There exists an ℱ 21PO-formula * in basic normal form such that: (i) |= * → ; (ii) every model of can be expanded to a model of * , and (iii) the length of * is bounded polynomially in the length of .
We remark that the transformations in the proofs of Lemmas 1 and 2 do not influence the cardinalities of antichains or intervals in models.
In this section we show that ℱ 21PO is not locally finite. The formula Φ we write builds on the infinity axiom presented in [ 17, Section 5]. It will contain several conjuncts of the form (B5b) with various and , so we introduce the abbreviation: ◁▷
:= ∀( () → ∀( () → ( < ) ∨ ( < ))); we also say in such case that the 1-types and are entangled.
Let = {0, 1, 2, 3, 4} and 0 = {| ∈ } ∪ {| ∈ }. Let Φ0 be the formula saying that the unary predicates of 0 are mutually disjoint and exhaustive, with the exception of 0 and 0 that are equivalent (so, one is invited to think that 0 and 0 can be identified) ∀(0 ↔ 0) ∧ ∀ ⋁︁ ∈ 0 ∧
⋀︁ ,′∈ 0:̸=′,{,′}̸={0,0} ( → ¬′).
(
Assume D |= Φ0 ∧ Φ(). Without loss of generality we may assume that there is 0 ∈
satisfying 0. By (
Now, let Φ() be a copy of the formula Φ() obtained by replacing all occurences of the s by corresponding s. Suppose D |= Φ0 ∧ Φ() ∧ Φ(). Starting with an element 0(= 0) ∈ satisfying both 0 and 0, and repeating the above argument for the -spiral, we see that D contains an -spiral {}∈Z and a -spiral {}∈Z crossing at 0 = 0, each having a particular direction.
To enforce infinite intervals we add additional entanglements. Let Φ be the formula containing for every ∈ the entanglement:
2 ◁▷ .
This is consistent with the identification 0 = 0, since we already have 0 ◁▷ 2 in (
Finally, let Φ = Φ0 ∧ Φ() ∧ Φ() ∧ Φ and let D |= Φ. Suppose the direction of the
-spiral and of the -spiral agrees with the natural order on the indices of its elements, i.e. 0 < 2
and 0 < 2. Simple reasoning with transitivity shows that all elements of the -spiral lie below 2.
Note that 5 (satisfying 0 = 0) generates a further -spiral, all of whose elements are greater than
2 and less than 7. And so the process repeats. Note in this regard that, the elements 5 ( ∈ Z)
which satisfy both 0 and 0 and, by (
Hence, D contains infinitely many mutually disjoint -spirals sandwiched between 5− 3 and 5+2, i.e. the intervals (5− 3, 5+2) = { ∈ |5− 3 < < 5+2} are mutually disjoint and each of them contains a whole infinite -spiral. The argument obviously repeats when the direction of the -spiral is opposite. Fig. 1 depicts a possible model D of Φ. Moreover, one could employ additional unary predicates to enforce a diferent -spiral involving 0 but ’going’ in the third dimension, inducing infinitely many -spirals, of which each induces infinitely many -spirals, as described above. The process can be continued for any finite dimension. Hence, we have the following observation. Theorem 3. Let > 0. There is a satisfiable formula ∈ ℱ 21PO such that every model of embeds a copy of Z (lexicographically ordered).
Note that the formulas enforcing infinity axioms and infinite intervals presented in this section use only universal conjuncts of the form (B5b) that define entanglements between distinct 1-types. As we show in Section 5, this is not a coincidence.
It is not dificult to show that ℱ 21PO can enforce models with infinite antichains (cf. Section 5.1 in [17]). In this section we show that ℱ 21PO enjoys the finite antichain property. The proof of the ifnite antichain property for ℱ 21PO comprises two steps. We first show the property for the logic ℱ 21PO where signatures contain no binary predicates other than < or =, and then generalize the proof to ℱ 21PO .
We recall Zorn’s lemma for posets that will be used in the ensuing argument.
Proposition 4 (Zorn). Let (, <) be a partially ordered set. If every chain in has an upper bound in then, has a maximal element.
We also need some more notions. Let = 0 ∪ {<}.
Definition 3. Let A be a -structure. Define a factorization of A as a set P of disjoint non-empty subsets of such that: (i) ⋃︀ ∈P = ; (ii) for every ∈ P, there exists a 1-type ∈ , denoted tp( ), such that for every ∈ we have tpA[] = ; (iii) for every distinct , ∈ P such that tp( ) = tp(), we have <A or <A . We refer to the elements of P as blocks. A block of cardinality 1 is called a unit. A unit block of type , where is realized only once in A, is called a king. Moreover, if we assume that the size of the blocks in P other than kings is a constant , we say that P is an -balanced factorization of A.
Note that every partial order A has the trivial factorization P = { | is realized in A} in which elements realizing the same 1-type form a single block. If P and Q are two factorizations of A, then denote by P ⊑ Q the fact that for every block ∈ Q, there exists a block ∈ P such that ⊆ . It is easily verifiable that ⊑ is a partial order on the set of all factorizations of A. We say that a factorization P is maximal if for every factorization Q of A, P ⊑ Q implies P = Q. The following lemma ensures us that maximal factorization exists.
Proof. Recall that ⊑ is the partial order on the set of factorizations of A. We obtain the conclusion by an application of Zorn’s lemma. Let {P}∈N be a chain w.r.t. ⊑ and define P* as the sum of the intersections of the elements of the Cartesian product ∏︀ P, that is P* = ⋃︀ ∈∏︀ P {⋂︀ ∈ } ∖ {∅}. P* is an upper bound of the chain because for each ∈ N we have P ⊑ P* , which follows from the features of the intersection of sets. In addition, P* is a factorization of A: (i) We have ⋃︀ * ∈P* * = since every element ∈ belongs to exactly one subset for each of the factorizations in the chain {P}∈N. (ii) Each block * ∈ P* has only elements which share the same 1-type since each of the factorizations {P}∈N has only subsets in which elements share the same 1-type. (iii) For each distinct blocks * , * ∈ P* such that ( ) = (), we have either * <A * or * <A * . This is because for each * ∈ P* there exists exactly one ∈ P for each ∈ N such that * ⊆ and similarly, for each * ∈ P* there exists exactly one ∈ P for each ∈ N such that * ⊆ . Hence, * <A * or * <A * follows directly from <A or <A that holds for P.
The following lemma is crucial.
(i) for every ∈ P, if is not a unit then there exists , ∈ such that ∼ A ; (ii) for every distinct , ∈ P such that ∼ A there exists ∈ and ∈ such that ∼ A . Proof. Let P be a maximal factorization of A.
(i) Let ∈ P be such that for all distinct , ∈ we have either <A or <A . Note that the elements in are totally ordered w.r.t. <A since they are comparable. Let be an element in and define the subsets < = { ∈ | <A }, = {} and > = { ∈ | >A }. Note that < ∪ > ̸= ∅ due to the fact that is not a unit and hence | | ≥ 2. Obviously, = < ∪ ∪ >. Replacing in P the block by three blocks <, and > we get Q = (P ∖ { }) ∪ {<, , >} which is a new factorization of A such that P ⊑ Q and P ̸= Q which contradicts maximality of P.
(ii) Let , ∈ P be such that ̸= and for all ∈ and ∈ we have either <A or <A . For every ∈ , define the subsets < = { ∈ | <A } and > = { ∈ | <A }. Obviously, < ∪ > = . Note that we have either < = ∅ or > = ∅. Otherwise, replacing in P the block by two non-empty blocks < and > we get Q = (P ∖ {}) ∪ {>, <}—a new factorization of A such that P ⊑ Q and P ̸= Q which contradicts maximality of P.
Now, split into the subsets < = { ∈ | < = } and > = { ∈ | > = }. Again, we have either < = ∅ or > = ∅. Otherwise, replacing in P the block by two blocks < and > we get a factorization Q′ = (P ∖ { }) ∪ {>, <} such that P ⊑ Q′ and P ̸= Q′ which again contradicts maximality of P. Hence, it follows that for every , ∈ P we have either <A or <A or there exist elements ∈ and ∈ such that ∼ A , which terminates the proof.
Now, we prove as follows.
Theorem 7. Let be a satisfiable ℱ 21PO-formula in basic normal form and let ≥ 2. Then, has a model with an -balanced factorization.
Proof. Let A |= and P be a maximal factorization of A that exists by Lemma 5.
We first mark at most elements in every block of P. Namely, if | | < , we mark all elements of , otherwise we mark distinct elements in . We denote the set of marked elements in block by . Now, we use the marked elements to build a new structure B with a partial order <B as follows: (i) = ⋃︀ ∈P , (ii) for each ∈ P, for each ∈ set tpB[] = ( ), (iii) for each ∈ P, for each , ′ ∈ , if ̸= ′, set ∼ B ′, (iv) for each , ∈ P such that <A set <B , (v) for each , ∈ P such that ∼ A , for each ∈ , ∈ set ∼ B .
In other words, (i) says that the domain of B consists of all previously marked elements of A and (ii) ensures that the 1-types are preserved. In particular, B = A and ⊆ for every 1-type . (* ) Condition (iii) says that distinct elements within a block of P are not comparable in B. Condition (iv) says that the block order from P is preserved in B; and condition (v) means that if two blocks , ∈ P are not comparable in A, then × contains no pair of comparable elements in B. In particular, for every , ∈ we have: if B |= < then A |= < . Note that Lemma 6 guarantees that for two blocks , ∈ P, ∼ A implies that there exist two elements ∈ and ∈ such that ∼ A . Hence, ′ ∼ B ′ implies that the 2-type realized by ′ ∈ ′ and ′ ∈ ′ is also realized in A. Hence, conditions (iii), (iv) and (v) ensure that all 2-types realized in B are also realized in A: B ⊆ A. (* )
To show that <B is antisymmetric, suppose there exist , ∈ such that <B and <B . By (iii), ∈ , ∈ for some , ∈ P such that ̸= . By construction, we have <A and <A , which violates antisymmetry of <A.
To show that <B is transitive, suppose there exist ∈ , ∈ , ∈ such that B |= < ∧ < . By construction, <A and <A . Since <A is transitive, we have <A . Hence, by (iv), B |= < .
Now, let P′ = ⋃︀ ∈P{ }. The above construction ensures that P′ is a factorization of B. Moreover, it is a maximal factorization. Let ⊆ be an antichain in B. Observe that if two elements of realize the same 1-type in B, they belong to one block of P′. Hence, since the size of every block in P′ is bounded by , the size of a maximal antichain in B is bounded by · | |.
Now, we show that B satisfies .
All conjuncts of the form (B1), (B8), (B9) and (B10) are obviously true due to (* ).
All conjuncts of the form (B2a), (B2b), (B3), (B4), (B5a) and (B5b) are obviously true due to (* ).
We show that all conjuncts of the form (B8) are true in B. Let = ∀( → ∃( () ∧ ∼ )) be such a conjunct. Let ∈ be an element such that tpB[] = . Since tpB[] = tpA[] and A |= , there is ∈ such that A |= [] ∧ ∼ A . Let , ∈ P′ be the blocks containing, respectively, and . Note that by construction, P′ is a maximal factorization. If = , then contains two elements and by part (i) of Lemma 6, there is ′ ∈ such that B |= ∼ ′. In case, ̸= , by part (ii) of Lemma 6, there is ′ ∈ such that B |= ∼ ′. Hence, in any case there is an element ′ ∈ such that B |= [′] ∧ ∼ ′.
Now, we show that the structure B can be extended to B′′ with an -balanced factorization so that B′′ satisfies .
Let P′ be a maximal factorization of B. Note that each element ∈ which belongs to a block ∈ P′ other than a king can be copied, that is we can construct a new structure B′ as follows: ′ = ∪ {′}, where ′ is called a copy of , P′′ = (P′ ∖{ })∪{ ′ ∪{′}} for each , ∈ we set tpB′ [, ] = tpB[, ] and for each ∈ we set tpB′ [′, ] = tpB[, ]. In the case if for all pairs of distinct elements , ∈ realizing the same 1-type , we have <B or <B , we set <B′ ′. Such structure B′ is obviously a model of . Note that P′′ might not be a maximal factorization. Repeating the operation of copying elements an appropriate number of times, we obtain a structure B′′ with an -balanced factorization which is a model of .
Observe that a model of the formula obtained according to Theorem 7 for = 2 has antichains bounded in 2 · | |. Thus, we obtain the following finite antichain property.
Corollary 8. Let be a ℱ 21PO-formula in basic normal form. If is satisfiable, then it has a model with bounded antichains.
A possible -structure with its -balanced factorization is shown in Fig. 2. Such structures play a major role in the proof of the finite antichain property for the whole logic ℱ 21PO that we provide now.
Theorem 9. Let be a satisfiable ℱ 21PO-sentence. Then it has a model with bounded antichains.
Proof. Let Φ be a ℱ 21PO-sentence in transitive normal form (
Hence, B′′ is a model of Φ with antichains bounded in 3 · | |. Since all the transformations required to obtain normal forms do not influence cardinalities of antichains, the above observation can be generalized to arbitrary ℱ 21PO-sentences.
In this section we show that in the logic ℱ 21PO the entanglements between distinct 1-types are crucial for losing the finite model property. Namely, we show the following theorem. Theorem 10. Let be an ℱ 21PO-formula in basic normal form not featuring conjuncts of the form (B5b). If is satisfiable then it has a finite model.
Proof. Let be a satisfiable ℱ 21PO-formula and let A be a model of where <A is interpreted as the partial order.
For each pair of 1-types and , we say that is less than if contains a conjunct ∀( → ∀( () → < )), being of the form (B3), and for each 1-type , we say that is linearly ordered if contains a conjunct ∀( → ∀( () ∧ ̸= → ( < ∨ < ))), being of the form (B5a). Let ≺ A be a binary relation on such that for each pair of distinct elements , ∈ realizing the 1-types tpA[] = and tpA[] = , is less than . Let ≺ + be the transitive closure of ≺ A. The relation ≺ + is a partial order because it is transitive and ≺ + is antisymmetric due to the fact that for each element , ∈ , ≺ + implies <A .
Now, for each ∈ A, define ( ) = {︃{1 }
, 2 } {1 if | | = 1 or is linearly ordered, otherwise, , where 1 , 2 (1 ̸= 2 ) are distinguished elements of .
Define = ⋃︀ ∈ A ( ), B = A↾ and <B=≺ + ∩ 2. Of course, since ≺ + is a partial order, <B is also a partial order.
It sufices to prove that B satisfies .
All conjuncts of the form (B1), (B9), (B10) are true because B = A and ⊆ for every 1-type All conjuncts of the form (B5a) are true since by the definition of B, for all 1-types which are linearly ordered, | | = 1. Otherwise, if | | > 1, then | | = 2 and for each distinct , ∈ we have ∼ B . Hence, all conjuncts of the form (B2a) are also true in B.
Let us prove (B2b), (B3), (B4). By the definition of B, the relation ≺ + cannot imply the situation that for any distinct 1-types , ∈ B, there exist ′ ∈ ( ) and ′ ∈ ( ) such that the 2-type B[′, ′] contradicts any of the conjuncts of the form (B2b), (B3), (B4). In the case of (B2b) and (B4), the definition of B implies that ′ ∼ B ′ and in the case of (B3), the definition of B implies that ′ <B ′.
We show that all conjuncts of the form (B8) are true in B. Let = ∀( → ∃( () ∧ ∼ )) be such a conjunct. For each ∈ with its 1-type tpA[] = , there exists a distinct element ∈ with its (not necessarily distinct) 1-type tpA[] = such that A |= [] ∧ ∼ A . Consider two cases. 1. ̸= . We have ∼ A and , are not connected by the relation ≺ +. Then, by the definition of B, for all ′ ∈ ( ) with their 1-type and for all ′ ∈ ( ) with their 1-type (where ′ ̸= ′), we have ′ ∼ B ′. This implies that for each ′ ∈ ( ) there exists a witness ′′ ∈ ( ) such that B |= [] ∧ ′ ∼ ′′. 2. = . By the definition of B, we know that |( )| = 2 since cannot be linearly ordered and | | ≥ 2. So, for each ′ ∈ ( ) there exists a witness ′ ∈ ( ) such that ′ ̸= ′ and B |= [′] ∧ ′ ∼ ′.
Thus, we conclude that B is a finite model of which has the size at most 2 · | |. One might argue that the restricted fragment identified in Theorem 10 that enjoys the finite model property is very limited. However, it allows one to express the mutual exclusion property of events in concurrent systems: for two events and the formula ¬∃∃( ∧ ∧ ∼ ) says that and cannot access the same critical section at the same time. This formula, when written in negation normal form, constitutes an acceptable conjunct of the form (B5a). In this fragment one can also express cross product of two classes of elements corresponding to natural statements such as “elephants are bigger than mice” that are not guarded (cf. e.g. [28] for more motivation and results about description logics with such statements).
In view of the finite model property established in Theorem 10 it is worth pointing out that the problematic universal formulas are the entanglements of the form ◁▷ , with ̸= , that require to order every pair of elements from two distinct classes but, in contrast to the situation between elephants and mice, the order is not predefined. Formulas of this form define models that are not N-free. For instance, the spirals defined in Section 3 contain elements that are exactly in the forbidden configuration, e.g. in the structure D depicted in Fig. 1 we have 2 > 0 < 3 > 1. Hence, branching automata mentioned in the Introduction, developed to deal with N-free posets, are not directly applicable to recognize models of such formulas.
So, in this article, we have also identified a minimal fragment of the two-variable logic with one partial order that is critical for answering the question on decidability of Sat(ℱ 21PO). Namely, it sufices to concentrate on: (i) signatures without equality comprising arbitrarily many unary predicates and one binary predicate required to be interpreted as a partial order; (ii) sentences in basic normal form as given in Definition 2 where only entanglements ◁▷ of the form (B5b) and conjuncts of the form (B8) appear. We believe that the fragment is decidable and we plan to study its satisfiability problem on scattered structures. The finite antichain property established in this paper suggests that some automata techniques might be generalized to handle such structures.
This work is supported by the Polish National Science Centre grant 2018/31/B/ST6/03662. [8] E. Kieroński, M. Otto, Small substructures and decidability issues for first-order logic with two variables., in: LICS, 2005, pp. 448–457. [9] E. Kieroński, J. Michaliszyn, I. Pratt-Hartmann, L. Tendera, Two-variable first-order logic with equivalence closure, in: Logic in Computer Science, IEEE, 2012, pp. 431–440. [10] M. Otto, Two-variable first-order logic over ordered domains, Journal of Symbolic Logic 66 (2001) 685–702. [11] T. Zeume, F. Harwath, Order invariance of two-variable logic is decidable, in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science LICS 2016, New York, NY, USA, July 5-8, 2016, 2016, pp. 807–816. [12] T. Schwentick, T. Zeume, Two-variable logic with two order relations - (extended abstract), in: A. Dawar, H. Veith (Eds.), CSL, volume 6247 of Lecture Notes in Computer Science, Springer, 2010, pp. 499–513. [13] S. Toruńczyk, T. Zeume, Register automata with extrema constraints, and an application to two-variable logic, Log. Methods Comput. Sci. 18 (2022). URL: https://doi.org/10.46298/lmcs-18(1: 42)2022. doi:10.46298/LMCS-18(1:42)2022. [14] E. Kieroński, Results on the guarded fragment with equivalence or transitive relations, in: C. L. Ong (Ed.), Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, Springer, 2005, pp. 309–324. URL: https://doi.org/10.1007/11538363_22. doi:10.1007/11538363\_22. [15] I. Pratt-Hartmann, Finite satisfiability for two-variable, first-order logic with one transitive relation is decidable, Math. Log. Q. 64 (2018) 218–248. URL: https://doi.org/10.1002/malq.201700055. doi:10.1002/malq.201700055. [16] W. Szwast, L. Tendera, FO2 with one transitive relation is decidable, in: 30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013, February 27 - March 2, 2013, Kiel, Germany, 2013, pp. 317–328. doi:10.4230/LIPIcs.STACS.2013.317. [17] W. Szwast, L. Tendera, On the satisfiability problem for fragments of two-variable logic with one transitive relation, J. Log. Comput. 29 (2019) 881–911. URL: https://doi.org/10.1093/logcom/exz012. doi:10.1093/LOGCOM/EXZ012. [18] M. Bojańczyk, A. Muscholl, T. Schwentick, L. Segoufin, Two-variable logic on data trees and XML reasoning, J. ACM 56 (2009) 13:1–13:48. URL: https://doi.org/10.1145/1516512.1516515. doi:10.1145/1516512.1516515. [19] B. Bednarczyk, W. Charatonik, E. Kieroński, Extending two-variable logic on trees, in: V. Goranko, M. Dam (Eds.), 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, pp. 11:1–11:20. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.11. doi:10.4230/ LIPICS.CSL.2017.11. [20] K. Lodaya, P. Weil, Series-parallel posets: Algebra, automata and languages, in: M. Morvan, C. Meinel, D. Krob (Eds.), STACS 98, Springer Berlin Heidelberg, Berlin, Heidelberg, 1998, pp. 555–565. [21] K. Lodaya, P. Weil, Series–parallel languages and the bounded-width property, Theoretical Computer Science 237 (2000) 347–380. URL: https://www.sciencedirect.com/science/article/pii/ S0304397500000311. doi:https://doi.org/10.1016/S0304-3975(00)00031-1. [22] D. Kuske, Infinite series-parallel posets: Logic and languages, in: U. Montanari, J. D. P. Rolim, E. Welzl (Eds.), Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings, volume 1853 of Lecture Notes in Computer Science, Springer, 2000, pp. 648–662. URL: https://doi.org/10.1007/3-540-45022-X_55. doi:10.1007/ 3-540-45022-X\_55. [23] N. Bedon, C. Rispal, Series-parallel languages on scattered and countable posets, in: Mathematical Foundations of Computer Science 2007: 32nd International Symposium, MFCS 2007 Česky` Krumlov, Czech Republic, August 26-31, 2007 Proceedings 32, Springer, 2007, pp. 477–488. [24] N. Bedon, Complementation of branching automata for scattered and countable n-free posets.,
International Journal of Foundations of Computer Science 29 (2018). [25] R. Alur, C. Stanford, C. Watson, A robust theory of series parallel graphs, Proc. ACM Program.
Lang. 7 (2023). URL: https://doi.org/10.1145/3571230. doi:10.1145/3571230. [26] I. L. Humberstone, Inaccessible worlds, Notre Dame J. Formal Log. 24 (1983) 346–352. URL: https://doi.org/10.1305/ndjfl/1093870378. doi: 10.1305/NDJFL/1093870378. [27] V. Goranko, Modal definability in enriched languages, Notre Dame J. Formal Log. 31 (1990) 81–105.
URL: https://doi.org/10.1305/ndjfl/1093635335. doi: 10.1305/NDJFL/1093635335. [28] S. Rudolph, M. Krötzsch, P. Hitzler, All elephants are bigger than all mice, in: F. Baader, C. Lutz, B. Motik (Eds.), Proceedings of the 21st International Workshop on Description Logics (DL2008), Dresden, Germany, May 13-16, 2008, volume 353 of CEUR Workshop Proceedings, CEUR-WS.org, 2008. URL: https://ceur-ws.org/Vol-353/RudolphKraetzschHitzler.pdf.