The Complexity of Second-Order HyperLTL

The complexity of undecidable problems is typically captured in terms of the arithmetical and analytical hierarchy, where decision problems (encoded as subsets of $\mathbb{N}$) are classified based on their definability by formulas of higher-order arithmetic, namely by the type of objects one can quantify over and by the number of alternations of such quantifiers. We refer to Roger’s textbook [35] for fully formal definitions and refer to Figure 1 for a visualization.

The class ${\mathrm{\Sigma }}_1^0$ contains the sets of natural numbers of the form

where quantifiers range over natural numbers and $\psi$ is a quantifier-free arithmetic formula. Note that this is exactly the class of recursively enumerable sets. The notation ${\mathrm{\Sigma }}_1^0$ signifies that there is a single block of existential quantifiers (the subscript $1$) ranging over natural numbers (type $0$ objects, explaining the superscript $0$). Analogously, ${\mathrm{\Sigma }}_1^1$ is induced by arithmetic formulas with existential quantification of type $1$ objects (sets of natural numbers) and arbitrary (universal and existential) quantification of type $0$ objects. So, ${\mathrm{\Sigma }}_1^0$ is part of the first level of the arithmetical hierarchy while ${\mathrm{\Sigma }}_1^1$ is part of the first level of the analytical hierarchy. In general, level ${\mathrm{\Sigma }}_n^0$ (level ${\mathrm{\Pi }}_n^0$) of the arithmetical hierarchy is induced by formulas with at most $n-1$ alternations between existential and universal type $0$ quantifiers, starting with an existential (universal) quantifier. Similar hierarchies can be defined for arithmetic of any fixed order by limiting the alternations of the highest-order quantifiers and allowing arbitrary lower-order quantification. In this work, the highest order we are concerned with is three, i.e., quantification over sets of sets of natural numbers.

$\mathrm{HyperLTL}$ satisfiability is ${\mathrm{\Sigma }}_1^1$-complete [19], $\mathrm{HyperLTL}$ finite-state satisfiability is ${\mathrm{\Sigma }}_1^0$-complete [16, 20], and, as mentioned above, ${\mathrm{Hyper}}^2\mathrm{LTL}$ model-checking is ${\mathrm{\Sigma }}_1^1$-hard [4], but, prior to this current work, no upper bounds were known for ${\mathrm{Hyper}}^2\mathrm{LTL}$.

Another yardstick is truth for order $k$ arithmetic, i.e., the question whether a given sentence of order $k$ arithmetic evaluates to true. In the following, we are in particular interested in the case $k=3$, i.e., we consider formulas with arbitrary quantification over type $0$ objects, type $1$ objects, and type $2$ objects (sets of sets of natural numbers). Note that these formulas span the whole third hierarchy, as we allow arbitrary nesting of existential and universal third-order quantification.

In this work, we determine the exact complexity of ${\mathrm{Hyper}}^2\mathrm{LTL}$ satisfiability, finite-state satisfiability, and model-checking, for the full logic and the two fragments introduced by Beutner et al. [4], as well as for two variations of the semantics.

An important stepping stone for us is the investigation of the cardinality of models of ${\mathrm{Hyper}}^2\mathrm{LTL}$. It is known that every satisfiable $\mathrm{HyperLTL}$ sentence has a countable model, and that some have no finite models [18]. This restricts the order of arithmetic that can be simulated in $\mathrm{HyperLTL}$ and explains in particular the ${\mathrm{\Sigma }}_1^1$-completeness of $\mathrm{HyperLTL}$ satisfiability [19]. We show that (unsurprisingly) second-order quantification allows to write formulas that only have uncountable models by generalizing the lower bound construction of $\mathrm{HyperLTL}$ to ${\mathrm{Hyper}}^2\mathrm{LTL}$. Note that the cardinality of the continuum is a trivial upper bound on the size of models, as they are sets of traces.

With this tool at hand, we are able to show that ${\mathrm{Hyper}}^2\mathrm{LTL}$ satisfiability is equivalent to truth in third-order arithmetic, i.e., much harder than $\mathrm{HyperLTL}$ satisfiability. This increase in complexity is not surprising, as second-order quantification can be expected to increase the complexity considerably. But what might be surprising at first glance is that the problem is not ${\mathrm{\Sigma }}_1^2$-complete, i.e., at the same position of the third hierarchy that $\mathrm{HyperLTL}$ satisfiability occupies in one full hierarchy below (see Figure 1). However, arbitrary second-order trace quantification corresponds to arbitrary quantification over type 2 objects, which allows to capture the full third hierarchy. Furthermore, we also show that ${\mathrm{Hyper}}^2\mathrm{LTL}$ finite-state satisfiability is equivalent to truth in third-order arithmetic, and therefore as hard as general satisfiability. This should be contrasted with the situation for $\mathrm{HyperLTL}$ described above, where finite-state satisfiability is ${\mathrm{\Sigma }}_1^0$-complete (i.e., recursively enumerable) and thus much simpler than general satisfiability, which is ${\mathrm{\Sigma }}_1^1$-complete.

Finally, our techniques for ${\mathrm{Hyper}}^2\mathrm{LTL}$ satisfiability also shed light on the exact complexity of ${\mathrm{Hyper}}^2\mathrm{LTL}$ model-checking, which we show to be equivalent to truth in third-order arithmetic as well, i.e., all three problems we consider have the same complexity. In particular, this increases the lower bound on ${\mathrm{Hyper}}^2\mathrm{LTL}$ model-checking from ${\mathrm{\Sigma }}_1^1$ to truth in third-order arithmetic. Again, this has be contrasted with the situation for $\mathrm{HyperLTL}$, where model-checking is decidable, albeit Tower-complete [33, 31].

So, quantification over arbitrary sets of traces makes verification very hard. However, Beutner et al. [4] noticed that many of the applications of ${\mathrm{Hyper}}^2\mathrm{LTL}$ described above do not require full second-order quantification, but can be expressed with restricted forms of second-order quantification. To capture this, they first restrict second-order quantification to smallest/largest sets satisfying a guard (obtaining the fragment ${\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{mm}}$)¹¹1In [4] this fragment is termed ${\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{fp}}$. For clarity, since it is not fixed point based, but uses minimality/maximality constraints, we use the subscript “mm” instead of “fp”. and then further restrict those to least fixed points induced by $\mathrm{HyperLTL}$ definable operators (obtaining the fragment $\mathrm{lfp}\text{-}{\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{mm}}$). By construction, these least fixed points are unique, i.e., second-order quantification degenerates to least fixed point computation.

As an example, consider again ${\phi }_{\mathrm{𝑐𝑘}}$ above. The internal constraint

defines a condition on what traces have to be in the set $X$, and how they are added gradually to $X$, a behavior that can be captured by a fixed point computation for the (monotone) operator induced by the formula above. Since the last part $\forall {\pi }^{\prime }\in X.\phi ({\pi }^{\prime })$ of ${\phi }_{\mathrm{𝑐𝑘}}$ universally quantifies over all traces in $X$, and since $X$ is existentially quantified, it is enough to consider the minimal set that satisfies the internal constraint: if some set satisfies a universal condition, then so does the minimal set. This minimal set is exactly the least fixed point of the operator induced by the formula above. Similar behavior is exhibited by many other applications of the logic, which gives the motivation to explore the fragment $\mathrm{lfp}\text{-}{\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{mm}}$.

Nevertheless, we show that ${\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{mm}}$ retains the same complexity as ${\mathrm{Hyper}}^2\mathrm{LTL}$, i.e., all three problems are still equivalent to truth in third-order arithmetic: Just restricting to guarded second-order quantification does not decrease the complexity.

For all results mentioned so far, it is irrelevant whether we allow second-order quantifiers to range over sets of traces that may contain traces that are not in the model (standard semantics) or whether we restrict these quantifiers to subsets of the model (closed-world semantics). But if we consider $\mathrm{lfp}\text{-}{\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{mm}}$ satisfiability under closed-world semantics, the complexity finally decreases to ${\mathrm{\Sigma }}_1^1$-completeness. Stated differently, one can add least fixed points of $\mathrm{HyperLTL}$ definable operators to $\mathrm{HyperLTL}$ without increasing the complexity of the satisfiability problem. Finally, for $\mathrm{lfp}\text{-}{\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{mm}}$ finite-state satisfiability and model-checking, we prove ${\mathrm{\Sigma }}_2^2$-membership and ${\mathrm{\Sigma }}_1^1$ lower bounds for both semantics, thereby confining the complexity to the second level of the third hierarchy.

Table 1 lists our results and compares them to $\mathrm{LTL}$ and $\mathrm{HyperLTL}$. Recall that Beutner et al. showed that $\mathrm{lfp}\text{-}{\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{mm}}$ yields (partial) model checking and monitoring algorithms [4, 5]. Our results confirm the usability of the $\mathrm{lfp}\text{-}{\mathrm{Hyper}}^2{\mathrm{LTL}}_{\mathrm{mm}}$ fragment also from a theoretical point of view, as all problems relevant for verification have significantly lower complexity (albeit, still highly undecidable).

Proofs omitted due to space restrictions can be found in the full version [21].

Let ${𝒱}_1$ be a set of first-order trace variables (i.e., ranging over traces) and ${𝒱}_2$ be a set of second-order trace variables (i.e., ranging over sets of traces) such that ${𝒱}_1\cap {𝒱}_2=\mathrm{\varnothing }$. We typically use $\pi$ (possibly with decorations) to denote first-order variables and $X,Y,Z$ (possibly with decorations) to denote second-order variables. Also, we assume the existence of two distinguished second-order variables $X_a,X_d\in {𝒱}_2$ such that $X_a$ refers to the set ${(2^{\mathrm{AP}})}^{\omega }$ of all traces, and $X_d$ refers to the universe of discourse (the set of traces the formula is evaluated over).

The formulas of ${\mathrm{Hyper}}^2\mathrm{LTL}$ are given by the grammar

where p ranges over $\mathrm{AP}$, $\pi$ ranges over ${𝒱}_1$, $X$ ranges over ${𝒱}_2$, and $𝐗$ (next) and $𝐔$ (until) are temporal operators. Conjunction ($\wedge$), exclusive disjunction $(\oplus )$, implication ($\to$), and equivalence $(\leftrightarrow )$ are defined as usual, and the temporal operators eventually ($𝐅$) and always ($𝐆$) are derived as $𝐅\psi =\neg \psi 𝐔\psi$ and $𝐆\psi =\neg 𝐅\neg \psi$. We measure the size of a formula by its number of distinct subformulas.

The semantics of ${\mathrm{Hyper}}^2\mathrm{LTL}$ is defined with respect to a variable assignment, i.e., a partial mapping $\mathrm{\Pi }:{𝒱}_1\cup {𝒱}_2\to {(2^{\mathrm{AP}})}^{\omega }\cup 2^{{(2^{\mathrm{AP}})}^{\omega }}$ such that

• $\mathrm{■}$

  if $\mathrm{\Pi }(\pi )$ for $\pi \in {𝒱}_1$ is defined, then $\mathrm{\Pi }(\pi )\in {(2^{\mathrm{AP}})}^{\omega }$ and

• $\mathrm{■}$

  if $\mathrm{\Pi }(X)$ for $X\in {𝒱}_2$ is defined, then $\mathrm{\Pi }(X)\in 2^{{(2^{\mathrm{AP}})}^{\omega }}$.

Given a variable assignment $\mathrm{\Pi }$, a variable $\pi \in {𝒱}_1$, and a trace $t$, we denote by $\mathrm{\Pi }[\pi \mapsto t]$ the assignment that coincides with $\mathrm{\Pi }$ on all variables but $\pi$, which is mapped to $t$. Similarly, for a variable $X\in {𝒱}_2$, and a set $T$ of traces, $\mathrm{\Pi }[X\mapsto T]$ is the assignment that coincides with $\mathrm{\Pi }$ everywhere but $X$, which is mapped to $T$. Furthermore, $\mathrm{\Pi }[j,\mathrm{\infty })$ denotes the variable assignment mapping every $\pi \in {𝒱}_1$ in $\mathrm{\Pi }$’s domain to $\mathrm{\Pi }(\pi )(j)\mathrm{\Pi }(\pi )(j+1)\mathrm{\Pi }(\pi )(j+2)\mathrm{\cdots }$, the suffix of $\mathrm{\Pi }(\pi )$ starting at position $j$ (the assignment of variables $X\in {𝒱}_2$ is not updated).

For a variable assignment $\mathrm{\Pi }$ we define

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash {\text{p}}_{\pi }$ if $\text{p}\in \mathrm{\Pi }(\pi )(0)$,

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash \neg \psi$ if $\mathrm{\Pi }\vDash ̸\psi$,

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash {\psi }_1\vee {\psi }_2$ if $\mathrm{\Pi }\vDash {\psi }_1$ or $\mathrm{\Pi }\vDash {\psi }_2$,

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash 𝐗\psi$ if $\mathrm{\Pi }[1,\mathrm{\infty })\vDash \psi$,

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash {\psi }_1𝐔{\psi }_2$ if there is a $j\ge 0$ such that $\mathrm{\Pi }[j,\mathrm{\infty })\vDash {\psi }_2$ and for all we have $\mathrm{\Pi }[j^{\prime },\mathrm{\infty })\vDash {\psi }_1$ ,

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash \exists \pi \in X.\phi$ if there exists a trace $t\in \mathrm{\Pi }(X)$ such that $\mathrm{\Pi }[\pi \mapsto t]\vDash \phi$ ,

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash \forall \pi \in X.\phi$ if for all traces $t\in \mathrm{\Pi }(X)$ we have $\mathrm{\Pi }[\pi \mapsto t]\vDash \phi$,

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash \exists X.\phi$ if there exists a set $T\subseteq {(2^{\mathrm{AP}})}^{\omega }$ such that $\mathrm{\Pi }[X\mapsto T]\vDash \phi$, and

• $\mathrm{■}$

  $\mathrm{\Pi }\vDash \forall X.\phi$ if for all sets $T\subseteq {(2^{\mathrm{AP}})}^{\omega }$ we have $\mathrm{\Pi }[X\mapsto T]\vDash \phi$.

Throughout the paper, we use the following shorthands to simplify our formulas:

• $\mathrm{■}$

  We write $\pi {=}_{{\mathrm{AP}}^{\prime }}{\pi }^{\prime }$ for a set ${\mathrm{AP}}^{\prime }\subseteq \mathrm{AP}$ for the formula $𝐆{\bigwedge }_{\text{p}\in {\mathrm{AP}}^{\prime }}({\text{p}}_{\pi }\leftrightarrow {\text{p}}_{{\pi }^{\prime }})$ expressing that the ${\mathrm{AP}}^{\prime }$-projection of $\pi$ and the ${\mathrm{AP}}^{\prime }$-projection of ${\pi }^{\prime }$ are equal.

• $\mathrm{■}$

  We write $\pi ⊳X$ for the formula $\exists {\pi }^{\prime }\in X.\pi {=}_{\mathrm{AP}}{\pi }^{\prime }$ expressing that the trace $\pi$ is in $X$. Note that this shorthand cannot be used under the scope of temporal operators, as we require formulas to be in prenex normal form.

A sentence is a formula in which only the variables $X_a,X_d$ can be free. The variable assignment with empty domain is denoted by ${\mathrm{\Pi }}_{\mathrm{\varnothing }}$. We say that a set $T$ of traces satisfies a ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentence $\phi$, written $T\vDash \phi$, if ${\mathrm{\Pi }}_{\mathrm{\varnothing }}[X_a\mapsto {(2^{\mathrm{AP}})}^{\omega },X_d\mapsto T]\vDash \phi$, i.e., if we assign the set of all traces to $X_a$ and the set $T$ to the universe of discourse $X_d$. In this case, we say that $T$ is a model of $\phi$. A transition system $𝔗$ satisfies $\phi$, written $𝔗\vDash \phi$, if $\mathrm{Tr}(𝔗)\vDash \phi$.

Although ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentences are required to be in prenex normal form, ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentences are closed under Boolean combinations, which can easily be seen by transforming such a sentence into an equivalent one in prenex normal form (which might require renaming of variables). Thus, in examples and proofs we will often use Boolean combinations of ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentences.

Second-order quantification in ${\mathrm{Hyper}}^2\mathrm{LTL}$ as defined by Beutner et al. [4] (and introduced above) ranges over arbitrary sets of traces (not necessarily from the universe of discourse) and first-order quantification ranges over elements in such sets, i.e., (possibly) again over arbitrary traces. To disallow this, we introduce closed-world semantics for ${\mathrm{Hyper}}^2\mathrm{LTL}$, only considering formulas that do not use the variable $X_a$. We change the semantics of set quantifiers as follows, where the closed-world semantics of atomic propositions, Boolean connectives, temporal operators, and trace quantifiers is defined as before:

• $\mathrm{■}$

  $\mathrm{\Pi }{\vDash }_{\mathrm{cw}}\exists X.\phi$ if there exists a set $T\subseteq \mathrm{\Pi }(X_d)$ such that $\mathrm{\Pi }[X\mapsto T]\vDash \phi$, and

• $\mathrm{■}$

  $\mathrm{\Pi }{\vDash }_{\mathrm{cw}}\forall X.\phi$ if for all sets $T\subseteq \mathrm{\Pi }(X_d)$ we have $\mathrm{\Pi }[X\mapsto T]\vDash \phi$.

We say that $T\subseteq {(2^{\mathrm{AP}})}^{\omega }$ satisfies $\phi$ under closed-world semantics, if ${\mathrm{\Pi }}_{\mathrm{\varnothing }}[X_d\mapsto T]{\vDash }_{\mathrm{cw}}\phi$. Hence, under closed-world semantics, second-order quantifiers only range over subsets of the universe of discourse. Consequently, first-order quantifiers also range over traces from the universe of discourse.

Thus, all complexity upper bounds we derive for standard semantics also hold for closed-world semantics and all lower bounds for closed-world semantics hold for standard semantics.

To capture the complexity of undecidable problems, we consider formulas of arithmetic, i.e., predicate logic with signature , evaluated over the structure . A type $0$ object is a natural number in $\mathbb{N}$, a type $1$ object is a subset of $\mathbb{N}$, and a type $2$ object is a set of subsets of $\mathbb{N}$.

Our benchmark is third-order arithmetic, i.e., predicate logic with quantification over type $0$, type $1$, and type $2$ objects. In the following, we use lower-case roman letters (possibly with decorations) for first-order variables, upper-case roman letters (possibly with decorations) for second-order variables, and upper-case calligraphic roman letters (possibly with decorations) for third-order variables. Note that every fixed natural number is definable in first-order arithmetic, so we freely use them as syntactic sugar. Truth of third-order arithmetic is the following problem: given a sentence $\phi$ of third-order arithmetic, does satisfy $\phi$?

Arithmetic formulas with a single free first-order variable define sets of natural numbers. We are interested in the classes

• $\mathrm{■}$

  ${\mathrm{\Sigma }}_1^1$ containing sets of the form $\{x\in \mathbb{N}\mid \exists X_1\subseteq \mathbb{N}.\mathrm{\cdots }\exists X_k\subseteq \mathbb{N}.\psi (x,X_1,\mathrm{\dots },X_k)\}$, where $\psi$ is a formula of arithmetic with arbitrary quantification over type $0$ objects (but no second-order quantifiers), and

• $\mathrm{■}$

  ${\mathrm{\Sigma }}_2^2$ containing sets of the following form, where $\psi$ is a formula of arithmetic with arbitrary quantification over type $0$ and type $1$ objects (but no third-order quantifiers): $\{x\in \mathbb{N}\mid \exists {𝒳}_1\subseteq 2^{\mathbb{N}}.\mathrm{\cdots }\exists {𝒳}_k\subseteq 2^{\mathbb{N}}.\forall {𝒴}_1\subseteq 2^{\mathbb{N}}.\mathrm{\cdots }\forall {𝒴}_{k^{\prime }}\subseteq 2^{\mathbb{N}}.\psi (x,{𝒳}_1,\mathrm{\dots },{𝒳}_k,{𝒴}_1,\mathrm{\dots },{𝒴}_{k^{\prime }})\}.$

We first prove that there is a satisfiable $X_a$-free ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentence ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ whose unique model (under standard semantics) has cardinality $𝔠$. To this end, we fix $\mathrm{AP}=\{\text{+},\text{-},\text{s},\text{x}\}$ and consider the conjunction ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}={\phi }_0\wedge \mathrm{\cdots }\wedge {\phi }_4$ of the following formulas:

• $\mathrm{■}$

  ${\phi }_0=\forall \pi \in X_d.{\bigvee }_{\text{p}\in \{\text{+},\text{-},\text{s}\}}𝐆({\text{p}}_{\pi }\wedge {\bigwedge }_{{\text{p}}^{\prime }\in \{\text{+},\text{-},\text{s}\}\setminus \{\text{p}\}}\neg {\text{p}}_{\pi }^{\prime })$: In each trace of a model, one of the propositions in $\{\text{+},\text{-},\text{s}\}$ holds at every position and the other two propositions in $\{\text{+},\text{-},\text{s}\}$ hold at none of the positions. Consequently, we speak in the following about type p traces for $\text{p}\in \{\text{+},\text{-},\text{s}\}$.

• $\mathrm{■}$

  ${\phi }_1=\forall \pi \in X_d.({\text{+}}_{\pi }\vee {\text{-}}_{\pi })\to \neg {\text{x}}_{\pi }𝐔({\text{x}}_{\pi }\wedge 𝐗𝐆\neg {\text{x}}_{\pi })$: Type p traces for $\text{p}\in \{\text{+},\text{-}\}$ in the model have the form ${\{\text{p}\}}^n\{\text{x},\text{p}\}{\{\text{p}\}}^{\omega }$ for some $n\in \mathbb{N}$.

• $\mathrm{■}$

  ${\phi }_2={\bigwedge }_{\text{p}\in \{\text{+},\text{-}\}}\exists \pi \in X_d.{\text{p}}_{\pi }\wedge {\text{x}}_{\pi }$: for both $\text{p}\in \{\text{+},\text{-}\}$, the type p trace ${\{\text{p}\}}^0\{\text{x},\text{p}\}{\{\text{p}\}}^{\omega }$ is in every model.

• $\mathrm{■}$

  ${\phi }_3={\bigwedge }_{\text{p}\in \{\text{+},\text{-}\}}\forall \pi \in X_d.\exists {\pi }^{\prime }\in X_d.{\text{p}}_{\pi }\to ({\text{p}}_{{\pi }^{\prime }}\wedge 𝐅({\text{x}}_{\pi }\wedge 𝐗{\text{x}}_{{\pi }^{\prime }}))$: for both $\text{p}\in \{\text{+},\text{-}\}$, if the type p trace ${\{\text{p}\}}^n\{\text{x},\text{p}\}{\{\text{p}\}}^{\omega }$ is in a model for some $n\in \mathbb{N}$, then also ${\{\text{p}\}}^{n+1}\{\text{x},\text{p}\}{\{\text{p}\}}^{\omega }$.

The formulas ${\phi }_1,{\phi }_2,{\phi }_3$ are similar to the formulas ${\psi }_1,{\psi }_2,{\psi }_3$ from Example 6. So, every model of ${\phi }_0\wedge \mathrm{\cdots }\wedge {\phi }_3$ contains $\{{\{\text{+}\}}^n\{\text{x},\text{+}\}{\{\text{+}\}}^{\omega }\mid n\in \mathbb{N}\}$ and $\{{\{\text{-}\}}^n\{\text{x},\text{-}\}{\{\text{-}\}}^{\omega }\mid n\in \mathbb{N}\}$ as subsets, and no other type + or type - traces.

Now, consider a set $T$ of traces over $\mathrm{AP}$ (recall that second-order quantification ranges over arbitrary sets, not only over subsets of the universe of discourse). We say that $T$ is contradiction-free if there is no $n\in \mathbb{N}$ such that ${\{\text{+}\}}^n\{\text{x},\text{+}\}{\{\text{+}\}}^{\omega }\in T$ and ${\{\text{-}\}}^n\{\text{x},\text{-}\}{\{\text{-}\}}^{\omega }\in T$. Furthermore, a trace $t$ over $\mathrm{AP}$ is consistent with a contradiction-free $T$ if

(C1)

${\{\text{+}\}}^n\{\text{x},\text{+}\}{\{\text{+}\}}^{\omega }\in T$ implies $\text{x}\in t(n)$ and

(C2)

${\{\text{-}\}}^n\{\text{x},\text{-}\}{\{\text{-}\}}^{\omega }\in T$ implies $\text{x}\notin t(n)$.

Note that $T$ does not necessarily specify the truth value of x in every position of $t$, i.e., in those positions $n\in \mathbb{N}$ where neither ${\{\text{+}\}}^n\{\text{x},\text{+}\}{\{\text{+}\}}^{\omega }$ nor ${\{\text{-}\}}^n\{\text{x},\text{-}\}{\{\text{-}\}}^{\omega }$ are in $T$. Nevertheless, for every trace $t$ over $\{\text{x}\}$ there is a contradiction-free $T$ such that the $\{\text{x}\}$-projection of every trace $t^{\prime }$ over $\mathrm{AP}$ that is consistent with $T$ is equal to $t$. Thus, each of the uncountably many traces over $\{\text{x}\}$ is induced by some subset of the model.

• $\mathrm{■}$

  Hence, we define ${\phi }_4$ as the formula

  	$\forall X.$	$\stackrel{X\text{ is contradiction-free}}{\overbrace{[\forall \pi \in X.\forall {\pi }^{\prime }\in X.({\text{+}}_{\pi }\wedge {\text{-}}_{{\pi }^{\prime }})\to \neg 𝐅({\text{x}}_{\pi }\wedge {\text{x}}_{{\pi }^{\prime }})]}}\to$
  		$\exists {\pi }^{\prime \prime }\in X_d.\forall {\pi }^{\prime \prime \prime }\in X.{\text{s}}_{{\pi }^{\prime \prime }}\wedge \underset{\text{(C1)}}{\underbrace{({\text{+}}_{{\pi }^{\prime \prime \prime }}\to 𝐅({\text{x}}_{{\pi }^{\prime \prime \prime }}\wedge {\text{x}}_{{\pi }^{\prime \prime }}))}}\wedge \underset{\text{(C2)}}{\underbrace{({\text{-}}_{{\pi }^{\prime \prime \prime }}\to 𝐅({\text{x}}_{{\pi }^{\prime \prime \prime }}\wedge \neg {\text{x}}_{{\pi }^{\prime \prime }}))}},$

  expressing that for every contradiction-free set of traces $T$, there is a type s trace $t^{\prime \prime }$ in the model (note that ${\pi }^{\prime \prime }$ is required to be in $X_d$) that is consistent with $T$.

While ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ is not in prenex normal form, it can easily be turned into an equivalent formula in prenex normal form (at the cost of readability).

Now, the set

of traces satisfies ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$. On the other hand, every model of ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ must indeed contain $T_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ as a subset, as ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ requires the existence of all of its traces in the model. Finally, due to ${\phi }_0$ and ${\phi }_1$, a model (over $\mathrm{AP}$) cannot contain any traces that are not in $T_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$, i.e., $T_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ is the unique model of ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$.

To conclude, we just remark that

has indeed cardinality $𝔠$, as ${(2^{\{\text{x}\}})}^{\omega }$ has cardinality $𝔠$.

Finally, let us consider closed-world semantics. We can restrict the second-order quantifier in ${\phi }_4$ (the only one in ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$) to subsets of the universe of discourse, as the set $T=\{{\{\text{+}\}}^n\{\text{x},\text{+}\}{\{\text{+}\}}^{\omega }\mid n\in \mathbb{N}\}\cup \{{\{\text{-}\}}^n\{\text{x},\text{-}\}{\{\text{-}\}}^{\omega }\mid n\in \mathbb{N}\}$ of traces (which is a subset of every model) is already rich enough to encode every subset of $\mathbb{N}$ by an appropriate contradiction-free subset of $T$. Thus, ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ has the unique model $T_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ even under closed-world semantics. $◀$

We begin with the lower bound by reducing truth in third-order arithmetic to ${\mathrm{Hyper}}^2\mathrm{LTL}$ satisfiability: we present a polynomial-time translation from sentences $\phi$ of third-order arithmetic to ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentences ${\phi }^{\prime }$ such that if and only if ${\phi }^{\prime }$ is satisfiable.

Given a third-order sentence $\phi$, we define

where

• $\mathrm{■}$

  ${\phi }_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}[X_d/X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}]$ is the ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentence from the proof of Theorem 7 where every occurrence of $X_d$ is replaced by $X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ and thus enforces every subset of $\mathbb{N}$ to be encoded in the interpretation of $X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}$ (as introduced in the proof of Theorem 7),

• $\mathrm{■}$

  ${\phi }_{(+,\cdot )}^{\prime }$ is the ${\mathrm{Hyper}}^2\mathrm{LTL}$ formula obtained from the $\mathrm{HyperLTL}$ formula ${\phi }_{(+,\cdot )}$ by replacing each quantifier $\exists \pi$ ($\forall \pi$, respectively) by $\exists \pi \in X_{\mathrm{𝑎𝑟𝑖𝑡ℎ}}$ ($\forall \pi \in X_{\mathrm{𝑎𝑟𝑖𝑡ℎ}}$, respectively) and thus enforces that $X_{\mathrm{𝑎𝑟𝑖𝑡ℎ}}$ is interpreted by a set whose ${\mathrm{AP}}_{\mathrm{𝑎𝑟𝑖𝑡ℎ}}$-projection is $T_{(+,\cdot )}$, and

where $\mathrm{ℎ𝑦𝑝}(\phi )$ is defined inductively as follows:

• $\mathrm{■}$

  For third-order variables $𝒴$,

  $$\mathrm{ℎ𝑦𝑝}(\exists 𝒴.\psi )=\exists X_{𝒴}.(\forall \pi \in X_{𝒴}.\exists {\pi }^{\prime }\in X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}.(\pi {=}_{\{\text{+},\text{-},\text{s},\text{x}\}}{\pi }^{\prime })\wedge {\text{s}}_{\pi })\wedge \mathrm{ℎ𝑦𝑝}(\psi ).$$

• $\mathrm{■}$

  For third-order variables $𝒴$,

  $$\mathrm{ℎ𝑦𝑝}(\forall 𝒴.\psi )=\forall X_{𝒴}.(\forall \pi \in X_{𝒴}.\exists {\pi }^{\prime }\in X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}.(\pi {=}_{\{\text{+},\text{-},\text{s},\text{x}\}}{\pi }^{\prime })\wedge {\text{s}}_{\pi })\to \mathrm{ℎ𝑦𝑝}(\psi ).$$

• $\mathrm{■}$

  For second-order variables $Y$, $\mathrm{ℎ𝑦𝑝}(\exists Y.\psi )=\exists {\pi }_Y\in X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}.{\text{s}}_{{\pi }_Y}\wedge \mathrm{ℎ𝑦𝑝}(\psi )$.

• $\mathrm{■}$

  For second-order variables $Y$, $\mathrm{ℎ𝑦𝑝}(\forall Y.\psi )=\forall {\pi }_Y\in X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}.{\text{s}}_{{\pi }_Y}\to \mathrm{ℎ𝑦𝑝}(\psi )$.

• $\mathrm{■}$

  For first-order variables $y$,

  $$\mathrm{ℎ𝑦𝑝}(\exists y.\psi )=\exists {\pi }_y\in X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}.{\text{s}}_{{\pi }_y}\wedge [(\neg {\text{x}}_{{\pi }_y})𝐔({\text{x}}_{{\pi }_y}\wedge 𝐗𝐆\neg {\text{x}}_{{\pi }_y})]\wedge \mathrm{ℎ𝑦𝑝}(\psi ).$$

• $\mathrm{■}$

  For first-order variables $y$,

  $$\mathrm{ℎ𝑦𝑝}(\forall y.\psi )=\forall {\pi }_y\in X_{\mathrm{𝑎𝑙𝑙𝑆𝑒𝑡𝑠}}.({\text{s}}_{{\pi }_y}\wedge [(\neg {\text{x}}_{{\pi }_y})𝐔({\text{x}}_{{\pi }_y}\wedge 𝐗𝐆\neg {\text{x}}_{{\pi }_y})])\to \mathrm{ℎ𝑦𝑝}(\psi ).$$

• $\mathrm{■}$

  $\mathrm{ℎ𝑦𝑝}({\psi }_1\vee {\psi }_2)=\mathrm{ℎ𝑦𝑝}({\psi }_1)\vee \mathrm{ℎ𝑦𝑝}({\psi }_2)$.

• $\mathrm{■}$

  $\mathrm{ℎ𝑦𝑝}(\neg \psi )=\neg \mathrm{ℎ𝑦𝑝}(\psi )$.

• $\mathrm{■}$

  For second-order variables $Y$ and third-order variables $𝒴$,

  $$\mathrm{ℎ𝑦𝑝}(Y\in 𝒴)=\exists \pi \in X_{𝒴}.{\pi }_Y{=}_{\{\text{x}\}}\pi .$$

• $\mathrm{■}$

  For first-order variables $y$ and second-order variables $Y$, $\mathrm{ℎ𝑦𝑝}(y\in Y)=𝐅({\text{x}}_{{\pi }_y}\wedge {\text{x}}_{{\pi }_Y})$.

• $\mathrm{■}$

  For first-order variables $y,y^{\prime }$, .

• $\mathrm{■}$

  For first-order variables $y_1,y_2,y$,

  $$\mathrm{ℎ𝑦𝑝}(y_1+y_2=y)=\exists \pi \in X_{\mathrm{𝑎𝑟𝑖𝑡ℎ}}.{\text{add}}_{\pi }\wedge 𝐅({\text{arg1}}_{\pi }\wedge {\text{x}}_{{\pi }_{y_1}})\wedge 𝐅({\text{arg2}}_{\pi }\wedge {\text{x}}_{{\pi }_{y_2}})\wedge 𝐅({\text{res}}_{\pi }\wedge {\text{x}}_{{\pi }_y}).$$

• $\mathrm{■}$

  For first-order variables $y_1,y_2,y$,

  $$\mathrm{ℎ𝑦𝑝}(y_1\cdot y_2=y)=\exists \pi \in X_{\mathrm{𝑎𝑟𝑖𝑡ℎ}}.{\text{mult}}_{\pi }\wedge 𝐅({\text{arg1}}_{\pi }\wedge {\text{x}}_{{\pi }_{y_1}})\wedge 𝐅({\text{arg2}}_{\pi }\wedge {\text{x}}_{{\pi }_{y_2}})\wedge 𝐅({\text{res}}_{\pi }\wedge {\text{x}}_{{\pi }_y}).$$

While ${\phi }^{\prime }$ is not in prenex normal form, it can easily be brought into prenex normal form, as there are no quantifiers under the scope of a temporal operator.

As we are evaluating ${\phi }^{\prime }$ w.r.t. standard semantics and the variable $X_d$ (interpreted with the model) does not occur in ${\phi }^{\prime }$, satisfaction of ${\phi }^{\prime }$ is independent of the model, i.e., for all sets $T,T^{\prime }$ of traces, $T\vDash {\phi }^{\prime }$ if and only if $T^{\prime }\vDash {\phi }^{\prime }$. So, let us fix some set $T$ of traces. An induction shows that satisfies $\phi$ if and only if $T$ satisfies ${\phi }^{\prime }$. Altogether we obtain the desired equivalence between and ${\phi }^{\prime }$ being satisfiable.

For the upper bound, we conversely reduce ${\mathrm{Hyper}}^2\mathrm{LTL}$ satisfiability to truth in third-order arithmetic: we present a polynomial-time translation from ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentences $\phi$ to sentences ${\phi }^{\prime }$ of third-order arithmetic such that $\phi$ is satisfiable if and only if . Here, we assume $\mathrm{AP}$ to be fixed, so that we can use $|\mathrm{AP}|$ as a constant in our formulas (which is definable in arithmetic).

Let $\mathrm{𝑝𝑎𝑖𝑟}:\mathbb{N}\times \mathbb{N}\to \mathbb{N}$ denote Cantor’s pairing function defined as $\mathrm{𝑝𝑎𝑖𝑟}(i,j)=\frac{1}{2}(i+j)(i+j+1)+j$, which is a bijection. Furthermore, fix some bijection $e:\mathrm{AP}\to \{0,1,\mathrm{\dots },|\mathrm{AP}|-1\}$. Then, we encode a trace $t\in {(2^{\mathrm{AP}})}^{\omega }$ by the set $S_t=\{\mathrm{𝑝𝑎𝑖𝑟}(j,e(\text{p}))\mid j\in \mathbb{N}\text{ and }\text{p}\in t(j)\}\subseteq \mathbb{N}$. As $\mathrm{𝑝𝑎𝑖𝑟}$ is a bijection, we have that $t\ne t^{\prime }$ implies $S_t\ne S_{t^{\prime }}$. While not every subset of $\mathbb{N}$ encodes some trace $t$, the first-order formula

checks if a set does encode a trace. Here, we use $\mathrm{𝑝𝑎𝑖𝑟}$ as syntactic sugar, which is possible as the definition of $\mathrm{𝑝𝑎𝑖𝑟}$ only uses addition and multiplication.

As (certain) sets of natural numbers encode traces, sets of (certain) sets of natural numbers encode sets of traces. This is sufficient to reduce ${\mathrm{Hyper}}^2\mathrm{LTL}$ to third-order arithmetic, which allows the quantification over sets of sets of natural numbers. Before we present the translation, we need to introduce some more auxiliary formulas:

• $\mathrm{■}$

  Let $𝒴$ be a third-order variable (i.e., $𝒴$ ranges over sets of sets of natural numbers). Then, the formula

  $${\phi }_{\mathrm{𝑜𝑛𝑙𝑦𝑇𝑟𝑎𝑐𝑒𝑠}}(𝒴)=\forall Y.Y\in 𝒴\to {\phi }_{\mathrm{𝑖𝑠𝑇𝑟𝑎𝑐𝑒}}(Y)$$

  checks if a set of sets of natural numbers only contains sets encoding a trace.

• $\mathrm{■}$

  Further, the formula

  $${\phi }_{\mathrm{𝑎𝑙𝑙𝑇𝑟𝑎𝑐𝑒𝑠}}(𝒴)={\phi }_{\mathrm{𝑜𝑛𝑙𝑦𝑇𝑟𝑎𝑐𝑒𝑠}}(𝒴)\wedge \forall Y.{\phi }_{\mathrm{𝑖𝑠𝑇𝑟𝑎𝑐𝑒}}(Y)\to Y\in 𝒴$$

  checks if a set of sets of natural numbers contains exactly the sets encoding a trace.

Now, we are ready to define our encoding of ${\mathrm{Hyper}}^2\mathrm{LTL}$ in third-order arithmetic. Given a ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentence $\phi$, let

where $\mathrm{𝑎𝑟}(\phi )$ is defined inductively as presented below. Note that ${\phi }^{\prime }$ requires ${𝒴}_a$ to contain exactly the encodings of all traces (i.e., it corresponds to the distinguished ${\mathrm{Hyper}}^2\mathrm{LTL}$ variable $X_a$ in the following translation) and ${𝒴}_d$ is an existentially quantified set of trace encodings (i.e., it corresponds to the distinguished ${\mathrm{Hyper}}^2\mathrm{LTL}$ variable $X_d$ in the following translation).

In the inductive definition of $\mathrm{𝑎𝑟}(\phi )$, we will employ a free first-order variable $i$ to denote the position at which the formula is to be evaluated to capture the semantics of the temporal operators. As seen above, in ${\phi }^{\prime }$, this free variable is set to zero in correspondence with the ${\mathrm{Hyper}}^2\mathrm{LTL}$ semantics.

• $\mathrm{■}$

  $\mathrm{𝑎𝑟}(\exists X.\psi )=\exists {𝒴}_X.{\phi }_{\mathrm{𝑜𝑛𝑙𝑦𝑇𝑟𝑎𝑐𝑒𝑠}}({𝒴}_X)\wedge \mathrm{𝑎𝑟}(\psi )$. Here, the free variable of $\mathrm{𝑎𝑟}(\exists X.\psi )$ is the free variable of $\mathrm{𝑎𝑟}(\psi )$.

• $\mathrm{■}$

  $\mathrm{𝑎𝑟}(\forall X.\psi )=\forall {𝒴}_X.{\phi }_{\mathrm{𝑜𝑛𝑙𝑦𝑇𝑟𝑎𝑐𝑒𝑠}}({𝒴}_X)\to \mathrm{𝑎𝑟}(\psi )$. Here, the free variable of $\mathrm{𝑎𝑟}(\forall X.\psi )$ is the free variable of $\mathrm{𝑎𝑟}(\psi )$.

• $\mathrm{■}$

  $\mathrm{𝑎𝑟}(\exists \pi \in X.\psi )=\exists Y_{\pi }.Y_{\pi }\in {𝒴}_X\wedge \mathrm{𝑎𝑟}(\psi )$. Here, the free variable of $\mathrm{𝑎𝑟}(\exists \pi \in X.\psi )$ is the free variable of $\mathrm{𝑎𝑟}(\psi )$.

• $\mathrm{■}$

  $\mathrm{𝑎𝑟}(\forall \pi \in X.\psi )=\forall Y_{\pi }.Y_{\pi }\in {𝒴}_X\to \mathrm{𝑎𝑟}(\psi )$. Here, the free variable of $\mathrm{𝑎𝑟}(\forall \pi \in X.\psi )$ is the free variable of $\mathrm{𝑎𝑟}(\psi )$.

• $\mathrm{■}$

  $\mathrm{𝑎𝑟}({\psi }_1\vee {\psi }_2)=\mathrm{𝑎𝑟}({\psi }_1)\vee \mathrm{𝑎𝑟}({\psi }_2)$. Here, we require that the free variables of $\mathrm{𝑎𝑟}({\psi }_1)$ and $\mathrm{𝑎𝑟}({\psi }_2)$ are the same (which can always be achieved by variable renaming), which is then also the free variable of $\mathrm{𝑎𝑟}({\psi }_1\vee {\psi }_2)$.

• $\mathrm{■}$

  $\mathrm{𝑎𝑟}(\neg \psi )=\neg \mathrm{𝑎𝑟}(\psi )$. Here, the free variable of $\mathrm{𝑎𝑟}(\neg \psi )$ is the free variable of $\neg \mathrm{𝑎𝑟}(\psi )$.

• $\mathrm{■}$

  $\mathrm{𝑎𝑟}(𝐗\psi )=\exists i^{\prime }(i^{\prime }=i+1)\wedge \mathrm{𝑎𝑟}(\psi )$, where $i^{\prime }$ is the free variable of $\mathrm{𝑎𝑟}(\psi )$ and $i$ is the free variable of $\mathrm{𝑎𝑟}(𝐗\psi )$.

• $\mathrm{■}$

  , where $i_j$ is the free variable of $\mathrm{𝑎𝑟}({\psi }_j)$, and $i$ is the free variable of $\mathrm{𝑎𝑟}({\psi }_1𝐔{\psi }_2)$.

• $\mathrm{■}$

  $\mathrm{𝑎𝑟}({\text{p}}_{\pi })=\mathrm{𝑝𝑎𝑖𝑟}(i,e(\text{p}))\in Y_{\pi }$, i.e., $i$ is the free variable of $\mathrm{𝑎𝑟}({\text{p}}_{\pi })$.

Now, an induction shows that ${\mathrm{\Pi }}_{\mathrm{\varnothing }}[X_a\to {(2^{\mathrm{AP}})}^{\omega },X_d\mapsto T]\vDash \phi$ if and only if satisfies $(\mathrm{𝑎𝑟}(\phi ))(0)$ when the variable ${𝒴}_a$ is interpreted by the encoding of ${(2^{\mathrm{AP}})}^{\omega }$ and ${𝒴}_d$ is interpreted by the encoding of $T$. Hence, $\phi$ is indeed satisfiable if and only if satisfies ${\phi }^{\prime }$. $◀$

In the lower bound proof above, we have turned a sentence $\phi$ of third-order arithmetic into a ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentence ${\phi }^{\prime }$ such that if and only if ${\phi }^{\prime }$ is satisfiable. In fact, we have constructed ${\phi }^{\prime }$ such that if it is satisfiable, then every set of traces satisfies it, in particular ${(2^{\mathrm{AP}})}^{\omega }$. Recall that Remark 3 states that ${(2^{\mathrm{AP}})}^{\omega }$ satisfies ${\phi }^{\prime }$ under standard semantics if and only if ${(2^{\mathrm{AP}})}^{\omega }$ satisfies ${\phi }^{\prime }$ under closed-world semantics. Thus, altogether we obtain that if and only if ${\phi }^{\prime }$ is satisfiable under closed-world semantics, i.e, the lower bound holds even under closed-world semantics. Together with Lemma 2, this settles the complexity of ${\mathrm{Hyper}}^2\mathrm{LTL}$ satisfiability under closed-world semantics.

The ${\mathrm{Hyper}}^2\mathrm{LTL}$ finite-state satisfiability problem asks, given a ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentence $\phi$, whether there is a finite transition system satisfying $\phi$. Note that we do not ask for a finite set $T$ of traces satisfying $\phi$. In fact, the set of traces of the finite transition system may still be infinite or even uncountable. Nevertheless, the problem is potentially simpler, as there are only countably many finite transition systems (and their sets of traces are much simpler). However, we show that the finite-state satisfiability problem is as hard as the general satisfiability problem, as ${\mathrm{Hyper}}^2\mathrm{LTL}$ allows the quantification over arbitrary (sets of) traces, i.e., restricting the universe of discourse to the traces of a finite transition system does not restrict second-order quantification at all (as the set of all traces is represented by a finite transition system). This has to be contrasted with the finite-state satisfiability problem for $\mathrm{HyperLTL}$ (defined analogously), which is ${\mathrm{\Sigma }}_1^0$-complete (a.k.a. recursively enumerable), as $\mathrm{HyperLTL}$ model-checking of finite transition systems is decidable [11].

For the lower bound under standard semantics, we reduce truth in third-order arithmetic to ${\mathrm{Hyper}}^2\mathrm{LTL}$ finite-state satisfiability: we present a polynomial-time translation from sentences $\phi$ of third-order arithmetic to ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentences ${\phi }^{\prime }$ such that $(\mathbb{N},+,\cdot ,$ if and only if ${\phi }^{\prime }$ is satisfied by a finite transition system.

So, let $\phi$ be a sentence of third-order arithmetic. Recall that in the proof of Theorem 9, we have shown how to construct from $\phi$ the ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentence ${\phi }^{\prime }$ such that the following three statements are equivalent:

• $\mathrm{■}$

  .

• $\mathrm{■}$

  ${\phi }^{\prime }$ is satisfiable.

• $\mathrm{■}$

  ${\phi }^{\prime }$ is satisfied all sets $T$ of traces (and in particular by some finite-state transition system).

Thus, the lower bound follows from Theorem 9.

For the upper bound, we conversely reduce ${\mathrm{Hyper}}^2\mathrm{LTL}$ finite-state satisfiability to truth in third-order arithmetic: we present a polynomial-time translation from ${\mathrm{Hyper}}^2\mathrm{LTL}$ sentences $\phi$ to sentences ${\phi }^{\prime \prime }$ of third-order arithmetic such that $\phi$ is satisfied by a finite transition system if and only if .

Recall that in the proof of Theorem 9, we have constructed a sentence

of third-order arithmetic where ${𝒴}_a$ represents the distinguished ${\mathrm{Hyper}}^2\mathrm{LTL}$ variable $X_a$, ${𝒴}_d$ represents the distinguished ${\mathrm{Hyper}}^2\mathrm{LTL}$ variable $X_d$, and where $\mathrm{𝑎𝑟}(\phi )$ is the encoding of $\phi$ in ${\mathrm{Hyper}}^2\mathrm{LTL}$.

To encode the general satisfiability problem it was sufficient to express that ${𝒴}_d$ only contains traces. Here, we now require that ${𝒴}_d$ contains exactly the traces of some finite transition system, which can easily be expressed in second-order arithmetic²²2With a little more effort, and a little less readability, first-order suffices for this task, as finite transition systems can be encoded by natural numbers. as follows.