=Paper=
{{Paper
|id=Vol-3733/paper5
|storemode=property
|title=On Two-variable First-order Logic with a Partial Order
|pdfUrl=https://ceur-ws.org/Vol-3733/paper5.pdf
|volume=Vol-3733
|authors=Dariusz Marzec,Lidia Tendera
|dblpUrl=https://dblp.org/rec/conf/cilc/MarzecT24
}}
==On Two-variable First-order Logic with a Partial Order==
<pdf width="1500px">https://ceur-ws.org/Vol-3733/paper5.pdf</pdf>
<pre>
                         On two-variable first-order logic with a partial order
                         Dariusz Marzec1,*,† , Lidia Tendera1,*,†
                         1
                             Institute of Computer Science, University of Opole, Poland


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

                                         Keywords
                                         two-variable first-order logic, satisfiability problem, decidability, finite model property, transitivity, partial order,
                                         finite antichains, locally finite order




                         1. Introduction
                         Two-variable first-order logic, ℱ𝒪2 , is the restriction of classical first-order logic, ℱ𝒪, over relational
                         signatures to formulae with at most two distinct variables 𝑥 and 𝑦. The logic enjoys the finite model
                         property [1], and its satisfiability (hence also finite satisfiability) problem is NExpTime-complete [2].
                            It is easy to show that ℱ𝒪2 is not able to express transitivity of a binary relation or related properties,
                         such as that of being an order or an equivalence. In fact, the same limitation applies to many other
                         decidable fragments of first-order logic, including the guarded fragment, 𝒢ℱ, and the fluted fragment,
                         ℱℒ. Hence, following the approach employed in modal logic, one program of research is to study
                         properties of these logics over restricted classes of structures where some distinguished binary predicates
                         are interpreted as transitive relations, orders or equivalences. Equivalently, one considers signatures
                         containing undistinguished predicates and distinguished predicates having a predefined interpretation as
                         a transitive relation, order, etc. In this setting, however, it is easy to write infinity axioms. For instance,
                         the ℱ𝒪2 -formula
                                                                  𝜙0 = ∀𝑥¬𝑇 𝑥𝑥 ∧ ∀𝑥∃𝑦𝑇 𝑥𝑦,                                           (1)
                         saying that 𝑇 is serial and irreflexive, with 𝑇 being a distinguished transitive predicate, is satisfiable but
                         has only infinite models.
                            In this scenario decidability of the (finite) satisfiability problem usually depends on the number of
                         distinguished relations, unless additional syntactic restrictions apply (cf. [3] for an overview and [4]
                         for a comprehensive study). In particular, it has been established that three distinguished predicates
                         interpreted as either transitive relations, equivalence relations or linear orders suffice to obtain undecid-
                         ability of both the satisfiability and the finite satisfiability problems for each of the logics 𝒢ℱ 2 , ℱ𝒪2
                         and ℱℒ2 . These results can be strengthened: in case of 𝒢ℱ 2 and ℱ𝒪2 undecidability follows already
                         CILC 2024: 39th Italian Conference on Computational Logic, June 26–28, 2024, Rome, Italy
                         *
                           Corresponding author.
                         †
                           These authors contributed equally.
                         $ dariusz.marzec@uni.opole.pl (D. Marzec); tendera@uni.opole.pl (L. Tendera)
                          0000-0002-9659-1161 (D. Marzec); 0000-0003-0681-4040 (L. Tendera)
                                      © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).


CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
over structures with one transitive and one equivalence relation [5], and in case of ℱℒ2 it suffices
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
finite 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, ℱ𝒪2 1T. 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(ℱ𝒪2 1T) 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
first-order logic. We remark that the infinity axiom (1) belongs to this fragment, as the existential
quantifier in the subformula ∀𝑥∃𝑦𝑇 𝑥𝑦 is guarded by the atom 𝑇 𝑥𝑦. In this fragment transitive guards
might also be of the form 𝑇 𝑦𝑥, so the syntax allows one to describe tense frames defined in modal logic
by adding to usual Kripke frames ⟨𝑊, 𝑅⟩ the converse of 𝑅.
   In this paper we study the fragment ℱ𝒪2 1T 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 ℱ𝒪2 1T with transitive witnesses.
   Models for ℱ𝒪2 1T-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 ℱ𝒪2 1T 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 ℱ𝒪2 1PO, the two-variable fragment of first-order logic
with one partial order, and its subfragments.
   Regarding expressive power it turns out that ℱ𝒪2 1PO 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
finite 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
first-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 ℱ𝒪2 1PO 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 ℱ𝒪2 1PO 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
finite 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,
finite antichains. Since the structures enforced by ℱ𝒪2 1PO-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
𝑥, iff 𝑝 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].


2. Preliminaries
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 𝐵.
2.1. Poset terminology
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
𝑌 ∼ 𝑌 ′ iff 𝑌 ̸< 𝑌 ′ 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
finite model property then it is also locally finite and enjoys the finite antichain property.

2.2. Logics
We denote by ℱ𝒪2 the two-variable fragment of first-order logic (with equality) over relational signa-
tures. As predicates having arity other than 1 or 2 add no effective expressive power in the context of
ℱ𝒪2 and individual constants add no effective expressive power given the presence of the equality
predicate, we shall take all signatures to consist only of unary and binary predicates.
   By ℱ𝒪2 1T, we understand the set of ℱ𝒪2 -formulas over any signature 𝜎 = 𝜎0 ∪ {𝑇 }, where 𝑇 is a
distinguished binary predicate letter. The semantics for ℱ𝒪2 1T 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 ℱ𝒪2 1PO. Note that the properties of a binary relation to be irreflexive and
antisymmetric are two-variable formulas, hence ℱ𝒪2 1PO is in fact a fragment of ℱ𝒪2 1T. Finally, we
define ℱ𝒪2𝑢 1PO to be the subset of ℱ𝒪2 1PO in which no binary predicates other than = and 𝑇 appear.
When working with ℱ𝒪2 1PO 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 ℱ𝒪2 1T depending on how the existential quantifiers are
used; no restrictions are imposed on using universal quantifiers. The fragment with transitive witnesses,
ℱ𝒪2 1T𝑡𝑤 , consists of the formulas of ℱ𝒪2 1T 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 𝜓 ∈ ℱ 𝒪2 1T𝑡𝑤 . Similarly, the fragment with free witnesses, ℱ𝒪2 1T𝑓 𝑤 , 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 𝜓 ∈ ℱ𝒪2 1T𝑓 𝑤 . In case of
ℱ𝒪2 1PO the corresponding fragments are denoted by ℱ𝒪2 1PO𝑡𝑤 and ℱ𝒪2 1PO𝑓 𝑤 .
   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 ℱ𝒪2 1T𝑡𝑤 . Hence, the infinity
axiom (1) can be written in ℱ𝒪2 1T𝑡𝑤 but cannot be written in ℱ𝒪2 1T𝑓 𝑤 .
2.3. Types and normal forms
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 ℱ𝒪2 1T (or of ℱ𝒪2 1PO) is said to be in transitive normal form if it
conforms to the pattern
                                𝑚
                                ⋀︁       ⋀︁
                   ∀𝑥∀𝑦 𝜓0 ∧                       ∀𝑥 (𝑃𝑖,𝑑 𝑥 → ∃𝑦 (𝑇𝑑 (𝑥, 𝑦) ∧ 𝜓𝑖,𝑑 (𝑥, 𝑦))),             (2)
                                𝑖=1 𝑑∈{∼,<,>,≡}


where 𝜓0 is quantifier-free, the 𝑃𝑖,𝑑 are unary predicates and the 𝜓𝑖,𝑑 (𝑥, 𝑦) are quantifier- and equality-
free formulas not featuring either of the atoms 𝑇 𝑥𝑦 or 𝑇 𝑦𝑥 (they may contain the atoms 𝑇 𝑥𝑥 or
𝑇 𝑦𝑦).

  Without loss of generality we assume that an ℱ𝒪2 1PO-formula in transitive normal form fea-
tures 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 ℱ𝒪2 1PO𝑡𝑤 feature no conjuncts with 𝑇∼ , and normal form
formulas of ℱ𝒪2 1PO𝑓 𝑤 feature only ∀∃-conjuncts with 𝑇∼ . So, denoting the transitive relation 𝑇 by
the symbol < and employing the abbreviation

                                𝑥 ∼ 𝑦 := ¬(𝑥 < 𝑦) ∧ ¬(𝑦 < 𝑥) ∧ 𝑥 ̸= 𝑦,

any ℱ𝒪2 1PO𝑓 𝑤 -formula 𝜙 in transitive normal form (2) conforms to the pattern
                                          𝑚
                                          ⋀︁
                            ∀𝑥∀𝑦 𝜓0 ∧           ∀𝑥 (𝑃𝑖 𝑥 → ∃𝑦 (𝑥 ∼ 𝑦 ∧ 𝜓𝑖 (𝑥, 𝑦))),                        (3)
                                          𝑖=1

where 𝜓0 is quantifier-free, the 𝑃𝑖 s are unary predicates and the 𝜓𝑖 (𝑥, 𝑦) are quantifier- and equality-free
formulas not featuring <.

Lemma 1 ([15], Lemma 5.2). Let 𝜙 be an ℱ𝒪2 1T-formula. There exists an ℱ𝒪2 1T-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 ℱ𝒪2𝑢 1PO one more normal form has been introduced in [15] to simplify reasoning con-
cerning 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 ℱ𝒪2𝑢 1PO 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 ℱ𝒪2𝑢 1PO-formula. There exists an ℱ𝒪2𝑢 1PO-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.


3. Enforcing Infinite Intervals
In this section we show that ℱ𝒪2𝑢 1PO𝑓 𝑤 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 𝑥) ∧ ∀𝑥          𝐶𝑥 ∧                              (𝐶𝑥 → ¬𝐶 ′ 𝑥).          (4)
                                    𝐶∈𝜎0          𝐶,𝐶 ′ ∈𝜎0 :𝐶̸=𝐶 ′ ,{𝐶,𝐶 ′ }̸={𝐴0 ,𝐵0 }
Let Φ𝑠𝑝𝑖𝑟𝑎𝑙(𝐴) contain for every 𝑖 ∈ 𝐼 the following conjuncts

                                   𝐴𝑖 ◁▷ 𝐴𝑖+2 ,                                                        (5)
                                   ∀𝑥(𝐴𝑖 𝑥 → ∃𝑦(𝐴𝑖+1 𝑦 ∧ 𝑥 ∼ 𝑦)),                                      (6)
                                   ∀𝑥(𝐴𝑖 𝑥 → ∃𝑦(𝐴𝑖−1 𝑦 ∧ 𝑥 ∼ 𝑦)),                                      (7)

with the arithmetical operations in indices understood modulo 5.
   Assume D |= Φ0 ∧ Φ𝑠𝑝𝑖𝑟𝑎𝑙(𝐴) . Without loss of generality we may assume that there is 𝑎0 ∈ 𝐷
satisfying 𝐴0 . By (6) there is an incomparable element 𝑎1 ∈ 𝐷 satisfying 𝐴1 . By (7), there is an
element 𝑎−1 ∈ 𝐷 incomparable with 𝑎0 satisfying 𝐴4 . By (5), 𝑎1 and 𝑎−1 are comparable. Assume
D |= 𝑎−1 < 𝑎1 . Now, the conjuncts (6) and (7) enforce existence of new elements 𝑎2 incomparable with
𝑎1 satisfying 𝐴2 and 𝑎−2 incomparable with 𝑎−1 and satisfying 𝐴3 . Since, by (5), 𝐴2 is entangled with
𝐴0 and 𝐴4 , so we get 𝑎0 < 𝑎2 and 𝑎−1 < 𝑎2 . Here, we have no choice for the direction, as otherwise,
by transitivity, 𝑎1 and 𝑎2 were comparable. Similarly, again by (5), 𝐴3 is entangled with 𝐴0 and 𝐴1 , we
get 𝑎−2 < 𝑎0 and 𝑎−2 < 𝑎1 . Hence, by transitivity, 𝑎−2 < 𝑎2 . Now, by (6), there must be a new element
𝑎3 ∈ 𝐷 incomparable with 𝑎2 satisfying 𝐴3 . Simple induction shows that there is an infinite sequence
of distinct elements 𝑎𝑘 ∈ 𝐷 (𝑘 ∈ Z) such that, for every 𝑘 ∈ Z, 𝑎𝑘 satisfies 𝐴𝑘(mod 5) , 𝑎𝑘 ∼ 𝑎𝑘+1 and,
for every 𝑘 < 𝑙+1, 𝑎𝑘 < 𝑎𝑙 . Let us call this sequence an 𝐴-spiral of D. Note that the argument repeats
when 𝑎−1 > 𝑎1 , resulting in a spiral going in the opposite direction (for every 𝑘 < 𝑙+1, 𝑎𝑙 < 𝑎𝑘 ).
Hence, the formula Φ0 ∧ Φ𝑠𝑝𝑖𝑟𝑎𝑙(𝐴) is an axiom of infinity.
   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 ◁▷ 𝐵𝑖 .                                           (8)

This is consistent with the identification 𝐴0 = 𝐵0 , since we already have 𝐴0 ◁▷ 𝐴2 in (5).
   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 (6), require a free witness satisfying 𝐴1 may use 𝑎1 as that free
witness. Similarly for the higher 𝐵-spirals.
   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 different 𝐶-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 𝜙 ∈ ℱ𝒪2𝑢 1PO𝑓 𝑤 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.
Figure 1: A structure D which is a model of Φ inducing infinite intervals. The elements 𝑎𝑘 with 𝑘 ∈ Z form an
A-spiral and the elements 𝑏𝑘𝑙 with 𝑘, 𝑙 ∈ Z form B-spirals. Each element 𝑎𝑘 realizes the 1-type 𝐴𝑘 mod 5 and each
element 𝑏𝑘𝑙 realizes the 1-type 𝐵𝑙 mod 5 . The straight thick blue arrow indicates the direction of the A-spiral; in
particular, 𝑎0 < 𝑎2 , 𝑎0 < 𝑎3 and 𝑎1 < 𝑎3 . The straight thin yellow arrows indicate the directions of the B-spirals.
Additionally, the curved arrows indicate that all elements of a given B-spiral crossing the A-spiral at the element
𝑎5𝑗 with 𝑗 ∈ Z are greater than 𝑎5𝑗−3 and less than 𝑎5𝑗+2 w.r.t. the partial order <D .


4. Finite antichain property
It is not difficult to show that ℱ𝒪2 1PO can enforce models with infinite antichains (cf. Section 5.1
in [17]). In this section we show that ℱ𝒪2 1PO𝑓 𝑤 enjoys the finite antichain property. The proof of the
finite antichain property for ℱ𝒪2 1PO𝑓 𝑤 comprises two steps. We first show the property for the logic
ℱ𝒪2𝑢 1PO𝑓 𝑤 where signatures contain no binary predicates other than < or =, and then generalize the
proof to ℱ𝒪2 1PO𝑓 𝑤 .
   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.

Lemma 5. Every 𝜎-structure A has got a maximal factorization.

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.

Lemma 6. Let P be a maximal factorization of A. Then:
(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 ℱ𝒪2𝑢 1PO𝑓 𝑤 -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
Figure 2: A 𝜎-structure B with its 2-balanced factorization. The blocks of P′ are indicated with dashed rectangles,
the relation < is the transitive closure of the above directed graph and 𝛼1 , 𝛼2 , ..., 𝛼𝑁 are 1-types. The elements
which realize the 1-type 𝛼2 are formed from blocks being units and the element which realizes the 1-type 𝛼𝑁 is
formed from a block being a king.


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 ℱ𝒪2 1PO𝑓 𝑤 -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 ℱ𝒪2 1PO𝑓 𝑤 that we provide
now.
Theorem 9. Let 𝜙 be a satisfiable ℱ𝒪2 1PO𝑓 𝑤 -sentence. Then it has a model with bounded antichains.
Proof. Let Φ be a ℱ𝒪2 1PO𝑓 𝑤 -sentence in transitive normal form (3), where binary predicates other
than < and = are allowed. For convenience, we recall the form below
                                           𝑚
                                           ⋀︁
                             ∀𝑥∀𝑦 𝜓0 ∧           ∀𝑥 (𝑃𝑖 (𝑥) → ∃𝑦 (𝑥 ∼ 𝑦 ∧ 𝜓𝑖 (𝑥, 𝑦))).                          (9)
                                           𝑖=1

We proceed similarly to the proof of Theorem 7, applying the following changes. First, we require that
the constant 𝑀 in the proof equals 3𝑚. Secondly, we modify B′′ with its factorization P′′ as follows.
Let 𝑃, 𝑄 ∈ P′′ be (not necessarily distinct) blocks. We put binary relations other than <, so that each
element 𝑎 ∈ 𝑃 ∪ 𝑄 has all required witnesses for the ∀∃-conjuncts in 𝑃 ∪ 𝑄. Finally, we put binary
relations other than < so that only 2-types from A appear in 𝑃 ∪ 𝑄. It guarantees that we construct
a structure B′′ with its 𝑀 -balanced factorization such that it does not realize a 2-type which is not
realized in A (universal constraints are still satisfied) and we can find for each element 𝑎 of B′′ all (at
most 𝑚) appropriate witnesses 𝑏 for the ∀∃-conjuncts, no matter whether 𝑎, 𝑏 ∈ 𝐵 ′′ should share the
same 1-type or not. In the former case, a witness 𝑏 can be found inside the block 𝑃 of 𝑎. Namely, the
constant 𝑀 = 3𝑚 guarantees that we are able to define 2-types in B′′ so that for each element 𝑎′ ∈ 𝑃
there exist all witnesses (at most 𝑚) in the same block 𝑃 . In the latter case, the fact that 𝑃 ∼A 𝑄
               ′′
implies 𝑃 ∼B 𝑄, guarantees that we are able to find all (at most 𝑚) witnesses 𝑏 in B′′ . So, 𝑀 ≥ 2𝑚
allows us to define 2-types in B′′ so that for each element 𝑎′ ∈ 𝑃 there exist all witnesses (at most 𝑚)
in the block 𝑄 and for each element 𝑏′ ∈ 𝑄 there exist all witnesses (at most 𝑚) in the block 𝑃 .
   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 ℱ𝒪2 1PO𝑓 𝑤 -sentences.


5. Retaining the finite model property
In this section we show that in the logic ℱ𝒪2𝑢 1PO𝑓 𝑤 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 ℱ𝒪2𝑢 1PO𝑓 𝑤 -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 ℱ𝒪2𝑢 1PO𝑓 𝑤 -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 }       if |𝐴𝛼 | = 1 or 𝛼 is linearly ordered,
                      𝑔(𝛼) =                                                         ,
                                 {𝑎𝛼1 , 𝑎𝛼2 } otherwise,

where 𝑎𝛼1 , 𝑎𝛼2 (𝑎⋃︀
                   𝛼 ̸= 𝑎𝛼 ) are distinguished elements of 𝐴𝛼 .
                   1     2
   Define 𝐵 = 𝛼∈𝛼A 𝑔(𝛼), B = A↾𝐵 and <B =≺+ ∩ 𝐵 2 . Of course, since ≺+ is a partial order, <B
is also a partial order.
   It suffices 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 · |𝛼|.
Discussion
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(ℱ𝒪2 1PO). Namely, it
suffices 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.


Acknowledgments
This work is supported by the Polish National Science Centre grant 2018/31/B/ST6/03662.


References
 [1] M. Mortimer, On languages with two variables, Zeitschr. f. Logik und Grundlagen d. Math. 21
     (1975) 135–140.
 [2] E. Grädel, P. Kolaitis, M. Vardi, On the decision problem for two-variable first-order logic, Bull. of
     Symb. Logic 3 (1997) 53–69.
 [3] E. Kieroński, I. Pratt-Hartmann, L. Tendera, Two-variable logics with counting and semantic
     constraints, ACM SIGLOG News 5 (2018) 22–43. URL: https://doi.org/10.1145/3242953.3242958.
     doi:10.1145/3242953.3242958.
 [4] I. Pratt-Hartmann, Fragments of First-Order Logic, Oxford Logic Guides, Oxford University Press,
     United Kingdom, 2023.
 [5] E. Kieroński, J. Michaliszyn, I. Pratt-Hartmann, L. Tendera, Two-variable first-order logic with
     equivalence closure, SIAM Journal of Computing 43 (2014) 1012–1063.
 [6] I. Pratt-Hartmann, L. Tendera, The fluted fragment with transitive relations, Ann. Pure Appl. Log.
     173 (2022) 103042. URL: https://doi.org/10.1016/j.apal.2021.103042. doi:10.1016/j.apal.2021.
     103042.
 [7] W. Szwast, L. Tendera, The guarded fragment with transitive guards, Ann. Pure Appl. Log. 128
     (2004) 227–276. URL: https://doi.org/10.1016/j.apal.2004.01.003. doi:10.1016/j.apal.2004.01.
     003.
 [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 Českỳ 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.

</pre>