We investigate the decidability of a family of logics mixing diference-logic constraints and unary uninterpreted predicates. The focus is set on logics whose domain of interpretation is R, but the language has a recognizer for integer values. We first establish the decidability of the logic allowing unary uninterpreted predicates, order constraints between real and integer variables, and diference-logic constraints between integer variables. Afterwards, we prove the undecidability of the logic where unary uninterpreted predicates and diference-logic constraints between real variables are allowed.
SMT (satisfiability modulo theories) solving has been very successfully used in various applications, most notably in verification (see e.g., [ 1]). Most SMT solvers were conceived as decision procedures for quantifier-free fragments including interpreted symbols and arithmetic operators. Support for quantifiers was mainly based on heuristics. Although some techniques were later introduced in SMT solvers (e.g., [2, 3, 4]) to reach decidability for quantified but purely arithmetic fragments, that is, without uninterpreted predicates, there has been little attention to the problem of decidability of quantified fragments mixing uninterpreted symbols and arithmetic.
In a previous paper [5] we discussed how to mix arithmetic and predicate symbols while avoiding undecidability. We focused on logics allowing uninterpreted unary predicates and diference-logic constraints, and investigated the expressive power of such logics over the domains N, Z, Q and R. We highlighted that when the domain is N or Z, the logic is equivalent to the monadic second-order theory of N with one successor relation (usually referred to as S1S). It is thus decidable and some efective decision procedures already exist. We also provided some directions to solve the case where the domain of interpretation is R, namely developing an encoding for the models of the predicates variables, and advocating for the use of the automata defined in [6].
In this paper we show that diference logic on the reals together with unary uninterpreted predicates is already undecidable. However, the mixed integer-real theory of order with unary uninterpreted predicates is decidable, even when allowing diference-logic constraints on integer variables. Basically, adding the “+1” function on the reals makes the logic undecidable.
After some prerequisites and the introduction of the studied fragments in Section 2, we first prove in Section 3 the decidability of the fragment with uninterpreted unary predicates, order constraints between real and integer variables and diference-logic constraints involving only integer variables. Section 4 is dedicated to a proof of undecidability of the fragment interpreted over R, where uninterpreted unary predicates, order between real values, and diference-logic constraints on real variables are allowed.
We refer to e.g., [7] for a general introduction to first-order logic with equality, and assume that the reader is familiar with the notions of signature, term, variable, and formula. We use the usual logical connectives (∨, ∧, ¬, ⇒, ⇔) and first-order quantification ∃. and ∀. , respectively equivalent to writing ∃ ( ) and ∀ ( ), i.e., the dot stands for an opening parenthesis that is closed at the end of the formula. Variable symbols are denoted by , , , . . .
Our signature contains interpreted arithmetic symbols 0, 1, +, − , <, ≤ , ≥ , >, and constants in N that stand for terms 1 + 1 + · · · + 1. We furthermore use a unary interpreted predicate ∈ Z to denote that has an integer value. The signature also contains uninterpreted predicate symbols , , . . . In the whole article, we only consider unary predicate symbols. Our language is the set of all well-formed formulas (in the usual sense) built using symbols from the signature. Further specific restrictions will be introduced later.
An interpretation specifies a domain (i.e., a set of elements), assigns a value in the domain to each free variable, and assigns relations of appropriate arity on the domain to predicate symbols in the signature. Throughout the article, the interpretation domain is always R. The arithmetic symbols 0, 1, +, − , <, ≤ , ≥ , > are interpreted as expected on R, and ∈ Z is true if and only if has an integer value2. An interpretation assigns an arbitrary subset of the domain R to each unary predicate. By extension, an interpretation assigns a value in R to every term, and a truth value to every formula. We denote the interpretation of a variable by [], and the interpretation of a predicate by [ ]. A model of a formula is an interpretation that assigns true to this formula. A formula is satisfiable on a domain (here R) if it has a model on that domain.
We consider several fragments where the language is restricted, in particular in the way that the arithmetic relations can be used. A fragment is decidable if there exists an efective procedure to check whether a given formula in this fragment is satisfiable.
In the various fragments introduced below, all arithmetic atoms are of the following form: 2In the current context, this choice of notation for mixed integer-real arithmetic is simpler than using a multi-sorted logic.
constant in Z, and ◁▷ ∈ {<, ≤ , =, ≥ , >}. • order constraints of the form ◁▷ , where and are variables and ◁▷ ∈ {<, ≤ , =, ≥ , >}; • diference-logic constraints of the form − ◁▷ , where and are variables, is a As a reminder, the language of our formulas only contain unary predicates. The only atoms besides the arithmetic ones are of the form () where is an uninterpreted predicate symbol and is a variable, and ∈ Z where is a variable. For convenience, the set of comparison operators is not minimal (we allow negations in formulas). Also, we sometimes write diferencelogic constraints in their equivalent form ◁▷ + .
We now introduce our fragments of interest. Their names are derived from the SMT-LIB nomenclature, where acronyms stand for the theories that appear in the combinations: • UF1: the theory of uninterpreted functions, with the restriction that only monadic (i.e., unary) predicates are allowed; • RO: the theory of order on the reals only; • IRO: the theory of order on the reals and integers; • IDL: diference logic on the integers; • RDL: diference logic on the reals.
UF1· RO. constraints between variables interpreted over R. Diference-logic constraints and atoms of the
The fragment UF1· RO is the fragment with unary uninterpreted predicates and order form ∈ Z are not allowed.
Example: The formula
∀ ∃ , . < < ∧ ∀ . ( < < ∧ ()) ⇒ = describes a predicate that is true only on isolated real numbers.
UF1· IRO. The fragment UF1· IRO is the extension of UF1· RO where atoms of the form ∈ Z are allowed. This fragment can express order relations between real and integer variables.
Example: The formula ∀, . [︀ < ∧ ∈ Z ∧ ∈ Z ︀] ⇒ ∃. < < ∧ () describes a predicate that is true for at least one value located between any two integers. they can only involve integer-guarded variables.
UF1· IDL· IRO. The fragment UF1· IDL· IRO is an extension of the fragment UF1· IRO (and therefore of UF1· RO). It is also interpreted over R. Order constraints between variables and atoms of the form ∈ Z are allowed. Additionally, diference-logic constraints are allowed, but
In order to enforce this integer-guard restriction on diference-logic constraints, UF1· IDL· IRO formulas must be well-guarded, i.e., diference-logic constraints can only appear in the two following contexts: • ∈ Z ∧ ∈ Z ∧ − ◁▷ , • ( ∈ Z ∧ ∈ Z) ⇒ − ◁▷ , where and are variables, ∈ N is a constant, and ◁▷ ∈ {<, ≤ , =, ≥ , >}.
Example: The formula
︀[ ∀, . (︀ ∈ Z ∧ ∈ Z ∧ − = 2)︀ ⇒ ︀( () ⇔ ())︀] ∧ ︀[ ∃, . ∈ Z ∧ ∈ Z ∧ () ∧ ¬ ()]︀ ∧ ︀[ ∀. ¬( ∈ Z) ⇒ ()]︀ describes a predicate that is either true on all odd numbers and false on all even numbers, or the opposite, as well as true on all non-integer numbers.
UF1· RDL. The fragment UF1· RDL is the fragment interpreted over R, where order constraints, diference-logic constraints and unary predicate atoms are allowed without any restriction. The use of atoms of the form ∈ Z is forbidden. Since order constraints are a special case of diference-logic constraints, the name of the fragment only refers to RDL and not RO.
Example: The formula
∀ ∃. − > 0 ∧ − < 3 ∧ () describes a predicate such that any sub-interval of R of length greater or equal to 3 contains a value for which is true.
Note: It might appear to the reader that a missing logic in this nomenclature is UF1· IRDL, with diference-logic constraints on both real and integer variables. We will later show that UF1· RDL is already undecidable, so it makes little sense to introduce any extension of it.
It has been established in [8, 9, 10, 11, 12] that the monadic first-order logic of order over R (UF1· RO) is decidable. We show here that its extension UF1· IDL· IRO (and therefore UF1· IRO) is also decidable, by reduction to UF1· RO.
Theorem 1. UF1· IDL· IRO and UF1· IRO are decidable.
Note that the decidability of UF1· IRO is a direct consequence of the decidability of UF1· IDL· IRO, since UF1· IDL· IRO is an extension of UF1· IRO. The remaining of this section is thus dedicated to the proof that UF1· IDL· IRO is decidable.
We first show how to define in UF1· RO a predicate int over R that is <-isomorphic to Z, i.e., there exists a bijection between the sets described by int and Z that preserves the order relation over their elements. Integer guards in UF1· IDL· IRO will later be translated using int. Intuitively, an integer-guarded variable in a UF1· IDL· IRO formula will correspond to a variable taking its value in the set described by int in the translated UF1· RO formula.
We axiomatize int in UF1· RO as follows: ∙ Every element of int is isolated:
∀ ∃ , . < < ∧ ∀. [ < < ∧ int()] ⇒ = . ∙ Every point in R has a successor in int:
∀ ∃ . < ∧ int() ∧ ∀. < < ⇒ ¬int(). ∙ Similarly, every point in R has a predecessor in int:
∀ ∃ . < ∧ int() ∧ ∀. < < ⇒ ¬int().
Notice that the successor and predecessor axioms ensure that int is not the empty predicate. Furthermore, it is worth mentioning that defining the successor (resp. predecessor) axiom by stating that every point in int has a successor (resp. predecessor) in int would not be correct, as int would also describe sets that are not <-isomorphic to Z, e.g., the set {(, ) | ∈ Z, ∈ {1, 2}} with the order relation (, ) < (ℓ, ) if and only if either < , or = and < ℓ.
The set of all integers is a model for int, therefore the above axiomatization is consistent. The set of elements satisfying int is necessarily infinite and does not admit a maximal or a minimal element. This is a direct consequence of the successor and predecessor axioms. More interestingly, this set is also necessarily countable. Indeed, since each point is isolated, there exists an application that maps the elements satisfying int to disjoint open intervals. Any set of disjoint intervals in R with non-zero length is necessarily countable [13], since each of them contains a rational value that does not belong to the others.
It is now possible to define a predecessor and a successor relation on the real numbers satisfying int with the following formulas: • pred(, ) = int() ∧ int() ∧ < ∧ ∀. < < ⇒ ¬int(),
i.e., is the predecessor of ; • succ(, ) = int() ∧ int() ∧ < ∧ ∀. < < ⇒ ¬int(),
i.e., is the successor of .
Note that these two definitions are redundant, i.e., the formula pred(, ) holds if and only if succ(, ) holds.
We next prove that the set of elements satisfying int is <-isomorphic to the integers. For convenience in the proof, we define 0int as an arbitrary existentially quantified value that belongs to the set described by int.
Lemma 1. For any model of int, the set { | ∈ [int]} is <-isomorphic to Z. Proof. Given a model of the axiomatization of int, we need to define a bijection between the set = { | ∈ [int]} and Z that preserves order.
Let us define an application from to Z. We set (0int) = 0, and then define recursively: • () = () + 1 for each , ∈ such that > 0int and pred(, ), • () = () − 1 for each , ∈ such that < 0int and succ(, ).
Thanks to the fact that every point has a unique predecessor and successor, it follows that ranges over the whole set Z. It is clear that preserves order. It remains to show that is well defined for every element in .
If there exists some element ∈ for which is not defined, it means that is not wellfounded, in the sense that there exists either an element > 0int such that the interval [0int, ] contains an infinite number of elements satisfying int, or there exists an element < 0int such that the interval [, 0int] contains an infinite number of elements satisfying int. Since both cases are symmetric, we only address the former. There must exist a strictly increasing infinite series of elements in bounded by . Let us consider its limit ∈ R. Because there must exist an element of smaller than and arbitrarily close to , it follows that cannot have a predecessor, which contradicts an axiom. Therefore is well-defined, and every element of is associated to an integer number. The application is therefore a bijection.
We are now able to describe the satisfiability-preserving translation of formulas from UF1· IDL· IRO to UF1· RO. Consider a UF1· IDL· IRO formula . Without loss of generality, we assume that int does not appear in . The translation of is defined as
AXIOMS(int) ∧ J K where AXIOMS(int) is the conjunction of the axioms of int, and J· K is a translation operator. This translation operator J· K distributes over all Boolean operators and quantifiers, and corresponds to the identity for most considered atoms, except for: • J ∈ ZK = int(); • J − ◁▷ K = ∃0, . . . . ( = 0) ∧ ( ◁▷ ) ∧ ⋀︀0≤ < succ(+1, ), for ∈ N and ◁▷ ∈ {<, ≤ , =, ≥ , >}. We assume that 0, . . . are fresh variables w.r.t. and .
Example:
J − ≤ 2K = ∃0, 1, 2. = 0 ∧ succ(1, 0) ∧ succ(2, 1) ∧ ≤ 2.
Notice that we only deal with the case ∈ N since every atom of the form − ◁▷ with ∈ Z ∖ N and ◁▷ ∈ {<, ≤ , =, ≥ , >} can be rewritten as − ◁▷′ − with the following correspondences: (◁▷, ◁▷′) ∈ {(=, =), (<, >), (>, <), (≥ , ≤ ), (≤ , ≥ )}.
Given a UF1· IDL· IRO formula , the translation that we have introduced generates a corresponding UF1· RO formula . To establish that they are equisatisfiable, we need to prove that if admits a model, then also admits one, and reciprocally. This is quite straightforward: ∙ If is satisfiable, let be one of its models. Then, since shares the same free variables and predicates than with the only addition of int, we can directly construct a model ′ of that is similar to for the shared variables and predicates, and int is interpreted so that int() holds whenever ∈ Z. This is always possible since the only constraints on int generated by the construction of are the axioms stated above. ∙ If is satisfiable, then there exists a model of . Let us construct a model ′ of . Let 0int ∈ R be an arbitrary element of [int] (similarly to before). We define an automorphism of R, such that (0int) = 0, and recursively () = () + 1 for , ∈ [int], > 0int, and pred(, ); and () = () − 1 for , ∈ [int], < 0int, and succ(, ). The automorphism maps each open interval between the -th and ( +1)-th successors (resp. predecessors) of 0int in [int], onto the open interval (, + 1) (resp. (− ( +1), )) while preserving order. ′ is defined by ′[] = ( []) for each free variable of the formula , and ′[ ] = {() | ∈ [ ]} for each uninterpreted predicate of . No unary predicate atom can be violated by ′ by definition. Furthermore, no order constraint can be violated by ′ either since preserves order. Regarding the diference-logic constraints, the intermediate variables introduced in the translation are necessarily mapped to values in [int] since the succ relation enforces this property. Hence for each such variable, we have ( []) ∈ Z. Intuitively, this ensures that in ′ the diference between the values taken by the integer variables is consistent with the diference-logic constraints.
Hence ′ is a model of .
The result presented in the previous section establishes a lower bound of some sort for the decidability of our family of fragments. A natural follow up problem is to establish a corresponding upper bound, i.e., to define a slight extension of this logic that yields non-trivial undecidability. We show here that as soon as diference-logic constraints on reals are allowed, the logic becomes undecidable. More precisely, we establish the undecidability of UF1· RDL by reducing the halting problem of a Turing machine to the satisfiability problem over UF1· RDL.
Theorem 2. Satisfiability is undecidable for UF1 · RDL.
The remaining of this section is dedicated to the proof of the undecidability of UF1· RDL. We consider w.l.o.g. Turing machines defined over an alphabet with only two symbols and no explicit blank symbol [14]. This choice leads to a simpler proof, but the same approach can easily be extended to Turing machines with larger alphabets.
The proof is by reduction from the halting problem for a Turing machine starting from a blank tape (i.e., a tape filled with the symbol 0). Consider a Turing machine ℳ = (, Σ , , , ), where • is a finite set of states, • the alphabet Σ is w.l.o.g. assumed to be {0, 1}, • ∈ is the initial state, • ∈ is the halting state, • : ( ∖ { }) × Σ → × Σ × { , } is the transition relation, assumed to be total.
A configuration of such a Turing machine is a triplet containing the current state , the content of the tape = {0, 1}Z and finally the position of the head ℎ ∈ Z. Since the machine starts from a blank tape, the initial configuration is 0 = ( , {0}Z, 0).
A run of length ∈ N ∪ {+∞} of such a Turing machine is a (possibly infinite) sequence of configurations ()∈[0,] , such that for any two consecutive configurations = (, , ℎ) and +1 = (+1, +1, ℎ+1) there exists a transition (, , ′, ′, ) ∈ such that: • = and ′ = +1, • [ℎ] = , i.e., the tape cell at position ℎ contains the symbol , • +1[ℎ] = ′, • +1[] = [], for every ∈ Z, ̸= ℎ, • ℎ+1 = ℎ + 1 if = , and ℎ+1 = ℎ − 1 if = .
A halting run is a finite run such that the state of its last configuration is the halting state and such that no previous configuration has as its state. ,
The reduction consists in encoding a run of ℳ of length ∈ N ∪ {+∞} with predicates interpreted over real values. For this, we need to be able to represent configurations, and verify whether there exists a transition of ℳ that allows to go from one to another.
This requires to be able to represent the state, the head position and the entire tape content for each consecutive configuration of the run . Furthermore, we also need to compare two consecutive contents of the tape and ensure that the only change occurs at the position of the head, as well as to handle the motion of the head.
This can be done as follows:
∙ Let = ⌈log2(||)⌉. Every state ∈ can be encoded without ambiguity by
a tuple (,1, ,2, . . . , , ) of Boolean values. The states visited by can thus be
described by predicates 1, 2, . . . , such that for each ∈ [0, ], the tuple
(1(), 2(), . . . , ()) encodes the state reached by after steps. For convenience
we introduce the formula State() = ⋀︀1≤ ≤ () = , that is true if and only if
the machine is in state at step , where the shorthand () = , means ¬ () if
, = ⊥ and () otherwise.
∙ For each ∈ [0, ], the content of the tape after steps is described by the value of a
predicate interpreted over the open interval (, + 1). This is achieved by defining an
order-preserving mapping between Z and the open interval (
Recall that in this fragment the use of integer guards is forbidden. In order to have similar landmarks as natural and integer numbers, we will have to construct our own sets of elements that are <-isomorphic to N and Z.
We now show how to translate ℳ into a formula of the logic, that is satisfiable if and only if ℳ admits a halting run.
First, we define 0 as an arbitrary existentially quantified value in R, and 1 as the real such that 0 + 1 = 1.
Then we define a predicate nat that is <-isomorphic to N. We construct nat as follows: ∀ . nat() ⇔ [ = 0 ∨ ( ≥ 1 ∧ ∃ . nat() ∧ = + 1)] The state of the initial configuration is encoded on 0, and the states of the successive configurations are encoded on the successive elements belonging to the set described by nat.
We also define a predicate with a characteristic set that maps Z into (
∀ . (0 < < 1) ⇒ (∃ . < < 1 ∧ () ∧ ∀ . < < ⇒ ¬()). • Predecessor:
∀ . (0 < < 1) ⇒ (∃ . 0 < < ∧ () ∧ ∀ . < < ⇒ ¬()).
Notice that the successor and predecessor axioms ensure that is not the empty predicate.
We can now extend into over the union of intervals (, + 1) for such that nat() holds:
∀ . () ⇔ [︀ (0 < < 1 ∧ ()) ∨ ( > 1 ∧ ∃ . = + 1 ∧ ())]︀ The conditions on the initial configuration of
ℳ are encoded by the following formula: STARTℳ = State (0) ∧ (∀ . () ⇒ ¬ ())
∧ ∃ . () ∧ () ∧ ∀ . (() ∧ ()) ⇒ =
Notice that we do not specify the value of the head and tape predicates outside of the set described by . In other words, we ignore how these predicates behave outside of . The same goes for the value of the state predicates ( )1≤ ≤ outside of nat.
The conditions on the transition relation of ℳ are more complex. Intuitively, if at a given step ∈ [1, ] we have not yet encountered the halting state , then we must ensure that the configuration at step can be obtained from the configuration at the previous step − 1, by following a transition (, , ′, ′, ) ∈ . The overall formula for these conditions is the following:
STEPℳ = ∀ . (︀ > 0 ∧ nat() ∧ NotEndedℳ())︀ ⇒ ∃ . = +1 ∧ Transitionℳ(, ) The subformula NotEndedℳ() expresses that no previous landmark to (i.e., a value such that < and nat() holds) encodes the halting state. The formula is defined by:
NotEndedℳ() = ∀ . ( < ∧ nat()) ⇒ ¬State ()
The subformula Transitionℳ(, ) expresses that there exists a transition (, , ′, ′, ) ∈ that allows to move from the configuration corresponding to the landmark to the configuration corresponding to in one step. For convenience, we decompose the conditions on the transition relation as follows: ∧
(,, ′, ′, )∈ Transitionℳ(, ) = UniqueHeadℳ(, ) ⋁︁ [︁States,′ (, ) ∧ Tape, ′ (, ) ∧ Head (, ) ]︁
For a given transition (, , ′, ′, ) ∈ , the conditions on the states, tape and head are expressed as follows: • The landmarks and should be such that 1(), 2(), . . . , () encode and 1(), 2(), . . . , () encode ′:
States,′ (, ) = State() ∧ State′ () • The tape must contain at the current position of the head for the step corresponding to . Additionally, for the step corresponding to , the tape contains ′ at the previous position of the head, and is unchanged at all other positions.
Tape, ′ (, ) = ∧ ︀[ ∀. ( < < ∧ ¬() ∧ ()) ⇒ ∃′. ′ = +1 ∧ (′) = ()]︀
︀[ ∀. ( < < ∧ () ∧ ()) ⇒ ( () = ∧ ∃′. ′ = +1 ∧ (′) = ′)]︀ • The head is moved in the direction specified by . This can be expressed by exploiting the predecessor and successor relations on (defined in the exact same manner than pred(, ) and succ(, ) for int in the previous section).
Head (, ) = ∀. [︀ ( < < ∧ () ∧ ())
⇒ ∃′, ′′. (′ = + 1) ∧ (′′, ′) ∧ (′′)]︀ where = {︃succ if =
pred if = • We must also ensure that the position of the head is unique for the configuration corresponding to :
UniqueHeadℳ(, ) = ∃.[︀ < < ∧ () ∧ ()
∧ ∀′. (︀ < ′ < ∧ (′) ∧ (′))︀ ⇒ ′ = ]︀ Finally, the existence of a halting run is expressed by the formula:
ENDℳ = ∃. nat() ∧ State ()
The global formula that expresses that the Turing machine ℳ halts on some run encoded by the predicates ( = 1, . . . ), and is the following:
HALTℳ(1, . . . , , ) = STARTℳ ∧ STEPℳ ∧ ENDℳ
This concludes the proof of Theorem 2.
In this work, we have established a lower and an upper bound for decidability in a family of logics mixing weak forms of arithmetic and uninterpreted unary predicates.
We proved the decidability of the fragment UF1· IDL· IRO, where uninterpreted unary predicates, order constraints between real and integer variables and diference-logic constraints between integer variables are allowed. This result is a consequence of the already established decidability of its restriction UF1· RO (where only uninterpreted unary predicates and order constraints between real values are allowed).
The other result establishes the undecidability of the fragment UF1· RDL, where uninterpreted unary predicates and diference-logic constraints between real variables are allowed. Notice that this result can be adapted straightforwardly to the logic interpreted over the domain Q.
Since the submission of this article, we additionally proved that the restriction of UF1· RDL where only a single unary uninterpreted predicate is allowed is also undecidable. This further refines the decidability frontier.
A complexity upper bound for a decision procedure of UF1· RO is also known [11, 12]. Our long term goal is to design a practical decision procedure for this decidable logic, and to adapt it for UF1· IDL· IRO. [4] E. Ábrahám, J. H. Davenport, M. England, G. Kremer, Deciding the consistency of nonlinear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Journal of Logical and Algebraic Methods in Programming 119 (2021). [5] B. Boigelot, P. Fontaine, B. Vergain, Deciding satisfiability for fragments with unary predicates and diference arithmetic, in: Proceedings, 6th International Workshop on Satisfiability Checking and Symbolic Computation, 2021. [6] V. Bruyère, O. Carton, Automata on linear orderings, Journal of Computer and System
Sciences 73 (2007) 1–24. [7] H. B. Enderton, A mathematical introduction to logic (2nd edition), Academic Press, Boston, 2001. [8] J. P. Burgess, Y. Gurevich, The decision problem for linear temporal logic, Notre Dame
Journal of Formal Logic 26 (1985) 115–128. [9] H. Läuchli, J. Leonard, On the elementary theory of linear order, Fundamenta Mathematicae 59 (1966) 109–116. [10] W. Thomas, Ehrenfeucht games, the composition method, and the monadic theory of ordinal words, in: Structures in Logic and Computer Science, Springer, 1997, pp. 118–143. [11] M. Reynolds, The complexity of temporal logic over the reals, Annals of Pure and Applied
Logic 161 (2010) 1063–1096. [12] A. Rabinovich, Temporal logics over linear time domains are in PSPACE, Information and
Computation 210 (2012) 40–67. [13] W. Sierpiński, Cardinal and ordinal numbers (2nd edition), PWN, Warszawa, 1965. [14] C. E. Shannon, A universal Turing machine with two internal states, Automata studies 34 (1956) 157–165.