NEXP-Completeness and Universal Hardness Results for Justification Logic

Abstract

We provide a lower complexity bound for the satisfiability problem of a multi-agent justification logic, establishing that the general NEXP upper bound from our previous work is tight. We then use a simple modification of the corresponding reduction to prove that satisfiability for all multi-agent justification logics from there is $\varSigma _2^p$-hard – given certain reasonable conditions. Our methods improve on these required conditions for the same lower bound for the single-agent justification logics, proven by Buss and Kuznets in 2009, thus answering one of their open questions.

An extended version with omitted proofs can be found in [5].

Appendix: Supplementary Proofs

Proof

(Proof of Proposition 2 ). For 2, notice that the calculus rules correspond to the closure conditions of the aef, so if ${\mathcal {E}}_m \models e$ ⁷ iff $\varPhi \vdash _{*^\mathcal {F}} e$, then ${\mathcal {E}}_m$ is an aef, so the “if” direction is established; by induction on the calculus derivation, we can also establish for every aef ${\mathcal {E}}$, if ${\mathcal {E}}_m \models e$, then ${\mathcal {E}}\models e$. 1 is a direct consequence.   $\square$

Proof

(Proof of Corollary 2 ). If

$$ \bigwedge _{j=1}^k (x_j\! :_{i} \![p_j]^\top \vee x_j\! :_{i} \![p_j]^\bot ) \wedge \bigwedge _{j=k+1}^l (x_{j}\! :_{i} \![p_{j}]^\top \wedge x_{j}\! :_{i} \![p_{j}]^\bot ) \wedge S(\lnot \phi ) \wedge \lnot T^J(\lnot \phi ) [\lnot \phi ]^\top $$

is not satisfiable, then

$$ \bigwedge _{j=1}^k (x_j\! :_{i} \![p_j]^\top \vee x_j\! :_{i} \![p_j]^\bot ) \wedge \bigwedge _{j=k+1}^l (x_{j}\! :_{i} \![p_{j}]^\top \wedge x_{j}\! :_{i} \![p_{j}]^\bot ) \wedge S(\lnot \phi ) \vdash T^J(\lnot \phi ) [\lnot \phi ]^\top , $$

and then for every choice $c_1:\{1,\ldots , k\}\longrightarrow \{\top ,\bot \}$,

$$ \bigwedge _{j=1}^k (x_j\! :_{i} \![p_j]^{c_1(j)}) \wedge \bigwedge _{j=k+1}^l (x_{j}\! :_{i} \![p_{j}]^\top \wedge x_{j}\! :_{i} \![p_{j}]^\bot ) \wedge S(\lnot \phi ) \vdash T^J(\lnot \phi ) [\lnot \phi ]^\top , $$

and then since every variable from ${x}_1, \ldots , {x}_{k+l}$ appears at most once in $T^J$ and $T^J$ does not include !, by Lemma 2 there is some choice $c_2:\{1,\ldots , l\}\longrightarrow \{\top ,\bot \}$ such that

$$ \bigwedge _{j=1}^k (x_j\! :_{i} \![p_j]^{c_1(j)}) \wedge \bigwedge _{j=k+1}^l (x_{j}\! :_{i} \![p_{j}]^{c_2(j)}) \wedge S(\lnot \phi ) \vdash T^J(\lnot \phi ) [\lnot \phi ]^\top . $$

Therefore, for every assignment of truth-values on ${p}_1, \ldots , {p}_{k}$ there truth-values for $p_{k+1},\ldots ,p_{l+k}$ that make $\phi$ false.

On the other hand, if

$$ \bigwedge _{j=1}^k (x_j\! :_{i} \![p_j]^\top \vee x_j\! :_{i} \![p_j]^\bot ) \wedge \bigwedge _{j=k+1}^l (x_{j}\! :_{i} \![p_{j}]^\top \wedge x_{j}\! :_{i} \![p_{j}]^\bot ) \wedge S(\lnot \phi ) \wedge \lnot T^J(\lnot \phi ) [\lnot \phi ]^\top $$

is satisfiable, then there is some choice $c_1:\{1,\ldots , k\}\longrightarrow \{\top ,\bot \}$, such that

$$ \bigwedge _{j=1}^k (x_j\! :_{i} \![p_j]^{c_1(j)}) \wedge \bigwedge _{j=k+1}^l (x_{j}\! :_{i} \![p_{j}]^\top \wedge x_{j}\! :_{i} \![p_{j}]^\bot ) \wedge S(\lnot \phi ) \wedge \lnot T^J(\lnot \phi ) [\lnot \phi ]^\top $$

is satisfiable, and then since every variable from ${x}_1, \ldots , {x}_{k+l}$ appears at most once in $T^J$, for every choice $c_2:\{1,\ldots , l\}\longrightarrow \{\top ,\bot \}$,

$$ \bigwedge _{j=1}^k (x_j\! :_{i} \![p_j]^{c_1(j)}) \wedge \bigwedge _{j=k+1}^l (x_{j}\! :_{i} \![p_{j}]^{c_2(j)}) \wedge S(\lnot \phi ) \not \vdash T^J(\lnot \phi ) [\lnot \phi ]^\top . $$

Therefore, there is some truth assignment on ${p}_1, \ldots , {p}_{k}$ such that every truth assignment on $p_{k+1},\ldots ,p_{l+k}$ makes $\phi$ true.    $\square$

Table 3. Tableau rules for $M_H$. To test $\phi$ for $M_H$-satisfiability, start from a branch which only contains $(0,0)\ T\ \phi$ and keep expanding according to the rules above. A branch with $\sigma \ T\ \psi$ and $\sigma \ F\ \psi$ is propositionally closed. A (possibly infinite) branch which is not propositionally closed, but is closed under the rules is an accepting branch.

Proof

( Brief proof of Proposition 4 ). We first prove that the tableau procedure from Table 3 is sound and complete. From an accepting branch for $\phi$ we can construct a model for $\phi$: let W be the set of prefixes that have appeared in the branch; let $a \in \mathcal {V}(p)$ iff $a\ T\ p$ has appeared in the branch, let for $i=1,2,3,4$, $r_i = \{(a,a.(g,i)) \in W\times W \}$, for $i = 1,2$, $R_i=r_i$, $R_3$ is the transitive closure of $r_3$, and $R_4$ is the transitive closure of $r_3 \cup r_4$. It is not hard to verify that model $\mathcal {M}= (W,R_1,R_2,R_3,R_4)$ satisfies all necessary conditions and that $\mathcal {M},(0,0) \models \phi$ – by inductively proving that if $a\ T\ \psi$ in the branch then $\mathcal {M},a \models \psi$ and if $a\ F\ \psi$ in the branch then $\mathcal {M},a \not \models \psi$.

On the other hand, from a model $\mathcal {M}= (W,R_1,R_2,R_3,R_4)$ for $\phi$ we can make appropriate nondeterministic choices to construct an accepting branch for $\phi$. We map (0, 0) to a state $w^{(0,0)}$ such that $\mathcal {M},w^{(0,0)} \models \phi$; then, when $\sigma .(g,i)$ appears first, it must be because of a formula of the form $\sigma \ T\ \Diamond _i \psi$ (or $\sigma \ F\ \Box _i \psi$, but it is essentially the same case). If $\mathcal {M},w^\sigma \models \Diamond _i \psi$, then there must be some state $w^{\sigma } R_i w$, such that $\mathcal {M}\models \psi$ and thus we name $w = w^{\sigma .(g,i)}$. It is not hard to see that we can make such choices when applying the rules, so that if $a\ T\ \psi$ in the branch then $\mathcal {M},w^a \models \psi$ if $a\ F\ \psi$ in the branch then $\mathcal {M},w^a \not \models \psi$. In fact the rules of Table 3 preserve this condition right away; we just need to make sure that the same thing happens with the propositional rules – for instance, rule $\frac{\sigma \ T\ \psi \vee \chi }{\sigma \ T\ \psi \ \mid \ \sigma \ \mathcal {T}\ \chi }$ can make an appropriate choice depending on whether $\mathcal {M},w^\sigma \models \psi$ or $\mathcal {M},w^\sigma \models \chi$. Thus the constructed branch cannot be propositionally closed.

What remains is to show that this tableau procedure can be simulated by an alternating algorithm which uses polynomial space – thus $M_H$-satisfiability is in A $\mathsf{PSPACE}= \mathsf{EXP}$. This can be done by applying the following method: always keep the formulas prefixed by a certain prefix $\sigma$ in memory (at first $\sigma = (0,0)$). First apply all the tableau rules you can on the formulas prefixed by $\sigma$ – possibly use existential nondeterministic choices for this. Then, using a universal choice, pick one of the prefixes $\sigma ' = \sigma .(g,i)$ that were just constructed and replace the formulas you have in memory by the ones prefixed by $\sigma '$. Repeat these steps until we either have $\sigma \ T\ \psi$ and $\sigma \ F\ \psi$ in memory or we see “enough” prefixes. In this case, “enough” would mean “more than $2^{6|\phi |}$”, as $\phi$ has up to $|\phi |$ subformulas, so in a branch there can only be up to $6|\phi |$ formulas prefixed by some fixed $\sigma$ – thus the algorithm only needs to use $O(|\phi |)$ memory and if it goes through $6|\phi |+1$ prefixes, then two of these have prefixed exactly the same set of formulas. If the algorithm accepts $\phi$, then we can easily reconstruct an accepting branch by just taking the union of the constructed formulas, while if there is an accepting branch, then the algorithm can explore only parts of that branch.   $\square$

1.1 Proof of Theorem 2

The reduction we use is from (a variation of) the SCHÖNFINKEL-BERNAYS ${\mathsf {SAT}}$ problem: given a first-order formula $\phi$ of the form

$$\begin{aligned} \exists x_1 \cdots \exists x_k \forall y_1 \cdots \forall y_{k'} \psi , \end{aligned}$$

where $\psi$ contains no quantifiers or function symbols, is $\phi$ satisfiable by a first-order model?

SCHÖNFINKEL-BERNAYS ${\mathsf {SAT}}$ is known to be $\mathsf{NEXP}$-complete [17]. Furthermore, it is not hard to see that if

$$\begin{aligned} \exists x_1 \cdots \exists x_k \forall y_1 \cdots \forall y_{k'} \psi , \end{aligned}$$

is satisfiable, then it is satisfiable by a model of at most k elements. For the coming reduction, we instead use for convenience a simplified version of this problem, which we call BINARY SCHÖNFINKEL-BERNAYS ${\mathsf {SAT}}$ and is the same problem, only instead we ask if $\exists x_1 \cdots \exists x_k \forall y_1 \cdots \forall y_{k'} \psi$ is satisfiable by a first-order model of exactly two elements.

For the reductions that follow we use the following notation: for a non-negative integer $x\in \mathbb {N}$, let $bin(x) = bin_0(g),\ldots , bin_{\log g}(g)$ be its binary representation. Furthermore, like in Sect. 3, for every propositional and first-order formula $\psi$ we introduce propositional variables $[\psi ]^\top$ and $[\psi ]^\bot$.

Lemma 4

BINARY SCHÖNFINKEL-BERNAYS ${\mathsf {SAT}}$ is NEXP-complete.

Proof

Let $\phi$ be a first-order formula of the form

$$\begin{aligned} \exists x_1 \cdots \exists x_k \forall y_1 \cdots \forall y_{k'} \psi , \end{aligned}$$

where $\psi$ contains no quantifiers or function symbols. Furthermore, we assume that $\psi$ contains no constants. We can replace each $x_a$ by $\mathbf {x}_a = x_a^{1},x_a^{2},\ldots ,x_a^{\lceil \log k \rceil }$ and each $y_b$ by $\mathbf {y}_b = y_b^{1},y_b^{2},\ldots ,y_b^{\lceil \log k \rceil }$ in the quantifiers and wherever they appear in a relation. Therefore $\exists x_a$ is replaced by $\exists x_a^1 \exists x_a^2 \cdots \exists x_a^{\lceil \log k \rceil }$ ($\exists \mathbf {x_a}$ for short) and $\forall x_a$ is replaced by $\forall x_a^1 \forall x_a^2 \cdots \forall x_a^{\lceil \log k \rceil }$ ($\forall \mathbf {y_a}$ for short) and$R({z}_1, \ldots , {z}_{r})$ is replaced by $R({\mathbf {z}}_1, \ldots , {\mathbf {z}}_{r})$. Furthermore, every expression $z = z'$ where $z,z'$ are variables, is replaced by $\bigwedge _{1 \le a \le \lceil \log k \rceil } z^a = z'^{a}$ ($\mathbf {z}=\mathbf {z'}$ for short). The result of all these replacements in $\psi$ is called $\psi '$. The new formula is:

$$\begin{aligned} \phi ' = \exists \mathbf {x}_1 \cdots \exists \mathbf {x}_k \forall \mathbf {y}_1 \cdots \forall \mathbf {y}_{k'} \left( \bigwedge _{b = 1}^{k'} \bigvee _{a=1}^{k} \mathbf {x_a} = \mathbf {y_b} \rightarrow \psi '\right) \end{aligned}$$

We can also define a corresponding transformation of first-order models: assume that the universe of model $\mathcal {M}$ for $\phi$ is a set of at most k natural numbers (each of which is at most $k-1$ and an interpretation for some $x_a$); then $\mathcal {M}'$ is the model with $\{0,1\}$ as its universe, where for every relation R (on tuples of naturals) of $\mathcal {M}$ there is some $R'$, which is essentially the same relation, but on the binary representations of the elements of $\mathcal {M}$. That is,

$$R' = \{(bin(a_1),\ldots ,bin{(a_r)}) \in \{0,1\}^* \mid ({a}_1, \ldots , {a}_{r}) \in R \}$$

It is not hard to see that if $\mathcal {M}$ satisfies the original formula, then $\mathcal {M}'$ satisfies the new one: each $\mathbf {x}_a$ can be interpreted as the binary representation of the interpretation of $x_a$ in $\mathcal {M}$ and notice that the added equality assertions effectively limit the $\mathbf {y}$’s to range over the interpretations of the $\mathbf {x}$’s, which are then exactly the image of the elements of $\mathcal {M}$.

On the other hand, if $\phi '$ is satisfied by a model with $\{0,1\}$ as its universe, then $\phi$ is satisfied by the model which has the $\lceil \log k \rceil$-tuples of $\{0,1\}$ that are the interpretations of ${\mathbf {x}}_1, \ldots , {\mathbf {x}}_{k}$ as elements and as relations the restrictions of the two-element model’s relations on these tuples.   $\square$

Given a first-order formula $\phi$ as above, we construct a justification formula, $\phi ^J$, in polynomial time, such that $\phi$ is satisfiable by a two-element model if and only if $\phi$ is satisfiable by a J-model. The reader will notice several similarities to the proof of Theorem 1.

Let

$$\begin{aligned} \phi = \exists x_1 \cdots \exists x_k \forall y_1 \cdots \forall y_{k'} \psi \end{aligned}$$

be such a formula, where $\psi$ contains no quantifiers or function symbols. Let ${R}_1, \ldots , {R}_{m}$ be the relation symbols appearing in $\psi$, ${a}_1, \ldots , {a}_{m}$ their respective arities. Then, let $\alpha = \{ i \in \mathbb {N}\mid \exists r \le m \text { s.t. } i \le a_r \}$; then, $|\alpha | = \max \{{a}_1, \ldots , {a}_{m}\}$. We also define: $X = \{{x}_1, \ldots , {x}_{k} \}$; $Y = \{{y}_1, \ldots , {y}_{k'} \}$; $Z = X \cup Y$; $\rho _0 = k + k'$.

For this reduction, in addition to the terms introduced in Sect. 3, we define the following justification terms. If we expect a term to justify a tautological scheme of fixed length, then we can just assume the term exists and has some constant size. Otherwise we construct the term in a way that gives it size polynomial with respect to the formula it (provably) justifies. Again we need certain terms to encode manipulations of long conjunctions (which we can see as strings) and we start with these.

• addhyp is such that $\vdash addhyp\! :_{1} \!(\phi \rightarrow (\psi \rightarrow \phi ))$;

• replaceleft is such that $\vdash replaceleft\! :_{1} \!((\phi \rightarrow \phi ') \rightarrow ((\phi \wedge \psi ) \rightarrow (\phi ' \wedge \psi ))),$ while

• replaceright is such that $\vdash replaceright\! :_{1} \!((\psi \rightarrow \psi ') \rightarrow ((\phi \wedge \psi ) \rightarrow (\phi \wedge \psi ')))$;

• We define $replace^k_{l}$ in the following way:

  $$ replace^k_k = replaceright, $$

  while for $l<k$,

  $$ replace^k_{l} = trans \cdot replace^{k-1}_l \cdot replaceleft. $$

  Then it is not hard to see by induction on $k-l$ that

  $$ \vdash replace^k_l\! :_{1} \! ((\phi _l \rightarrow \phi '_l) \rightarrow ((\phi _1 \wedge \cdots \wedge \phi _l \wedge \cdots \wedge \phi _k) \rightarrow (\phi _1 \wedge \cdots \wedge \phi '_l \wedge \cdots \wedge \phi _k))). $$

• We define mphypoth to be such that

  $$ \vdash mphypoth\! :_{1} \! ((\phi \rightarrow \psi ) \rightarrow ((\phi \rightarrow (\psi \rightarrow \chi )) \rightarrow (\phi \rightarrow \chi ))). $$

• We use justification variables ${var}_1, \ldots , {var}_{a_r}, rel_r$ for every $r \in [m]$.

• For $1 \le r \le m$ we define $gather_r$ in the following way:

  $$\begin{aligned} gather_r = [append \cdot [append \cdots [ append \cdot var_1 ] \cdots var_{a_r}] \cdot rel_r], \end{aligned}$$

  For every $1 \le j \ \le a_r + 1$, let $v_j, v' _j \in \{ \top ,\bot \}$. Then, for propositional variables ${p}_1, \ldots , {p}_{a_r}$,

  $$\begin{aligned} \bigwedge _ {j = 1}^{a_r}var_j\! :_{1} \![p_j]^{v_j} \wedge rel_r\! :_{1} \! [R_r]^{v_{a_r + 1}} \vdash gather_r\! :_{1} \! ([p_1]^{v'_1} \wedge \cdots \wedge [p_{a_r}]^{v'_{a_r}} \wedge [R_r]^{v'_{a_r+1}}) \end{aligned}$$

  if and only if for every $1 \le j \le a_r + 1$, $v_j = v'_j$ (see the proof of Lemma 3). In fact it is not hard to see that if

  $$ \bigwedge _ {j = 1}^{a_r}var_j\! :_{1} \![p_j]^{v_j} \wedge rel_r\! :_{1} \! [R_r]^{v_{a_r + 1}} \vdash gather_r\! :_{1} \! \chi , $$

  then $\bigwedge _ {j = 1}^{a_r}[p_j]^{v_j} \wedge [R_r]^{v_{a_r + 1}} \vdash \chi$: operator ! does not appear in $gather_r$, so the right-hand side of a corresponding $*$-calculus derivation for $*_1(gather_r,\chi )$ is a propositional derivation of $\chi$ from $[p_1]^{v_1}, \ldots , [p_{a_r}]^{v_{a_r}}, [R_r]^{v_{a_r+1}}$ and some propositional tautologies.

  To give some intuition, conjunction $\bigwedge _ {j = 1}^{a_r}var_j\! :_{1} \![p_j]^{v_j} \wedge rel_r\! :_{1} \! [R_r]^{v_{a_r + 1}}$ means that $({v}_1, \ldots , {v}_{a_r}) \in R_r$ in a corresponding first-order model.

• We use justification variables $value_z$ and $match(z,p_l)$ for all $z \in Z$, $l \in \alpha$. For every $z \in X$, we define $V_z = value_z\! :_{1} \![z]^\top \vee value_z\! :_{1} \![z]^\bot$; for every $z \in Y$, $V_z = value_z\! :_{1} \![z]^\top \wedge value_z\! :_{1} \![z]^\bot$.

  We also define

  $$ Match = \bigwedge _{\begin{array}{c} l\in \alpha \\ z \in Z \\ \triangle \in \{ \top , \bot \} \end{array}} match(z,p_l)\! :_{1} \!([z]^\triangle \rightarrow ([p_l]^\triangle \rightarrow ok_l)). $$

• For every $R_r(\mathbf {z})$ which appears in $\psi$ and $0\le b \le a_r$ , we define

• $match_b^{R_r(\mathbf {z})}$ in the following way:

  $match_0^{R_r(\mathbf {z})} = addhyp \cdot gather_r$ and if $b>0$ and $z_b = x_l$ or $z_b = y_{l-k}$, then $match^{R_r(\mathbf {z})}_b$ is defined to be the term

  $$\begin{aligned}{}[mphypoth \cdot match^{R_r(\mathbf {z})}_{b-1} \cdot [tran \cdot [tran \cdot project^{\rho _1}_l \cdot match(z_b,b) ] \cdot replace^{a_r+1}_b ] ]. \end{aligned}$$

  We can see by induction on b that for every $0\le b \le a_r$,

  $$\begin{aligned} \begin{aligned}&Match,\ gather_r\! :_{1} \!( [p_{1}]^{v'_{1}}\wedge \cdots \wedge [p_{a_r}]^{v'_{a_r}} \wedge [R_r]^{v_{a_r +1}}) \vdash \\&\vdash match^{R_r({z}_1, \ldots , {z}_{a_r})}_b\! :_{1} \!\left( ( [x_1]^{v_1^{}}\wedge \cdots \wedge [x_k]^{v_k}\wedge [y_1]^{v_{k+1}}\wedge \cdots \wedge [y_{k'}]^{v_{k'+k}} ) \rightarrow \right. \\&\rightarrow \left. (ok_1 \wedge \cdots \wedge ok_b \wedge [p_{b+1}]^{v'_{b+1}}\wedge \cdots \wedge [p_{a_r}]^{v'_{a_r}} \wedge [R_r]^{v_{a_r +1}})\right) \end{aligned} \end{aligned}$$

  if and only if for every $j \in [a_r]$ and $j' \in [k+k']$, if $z_j = x_{j'}$ or $z_j = y_{j'-k}$, then $v'_j=v_{j'}$.

  Match and term $match_b^{R_r(\mathbf {z})}$ are used to confirm that given an assignment v for variables ${x}_1, \ldots , {x}_{k},{y}_1, \ldots , {y}_{k'}$, a tuple $\mathbf {z} \in Z^{a_r}$, and a tuple $({v'}_1, \ldots , {v'}_{a_{r+1}}) \in \{\top ,\bot \}^{a_{r+1}}$, that $(v(z_1),\ldots ,v(z_{a_r})) = ({v'}_1, \ldots , {v'}_{a_r})$, since this is a crucial condition to assert that $[R_r(\mathbf {z})]^{v_{a_{r+1}}}$ must be true (i.e. $R_r(\mathbf {z})$ is true iff $v_{a_{r+1}} = \top$).

• $T^!(match^{R_r(\mathbf {z})}_b)$ is defined in the following way:

  $T^!(match^{R_r(\mathbf {z})}_0) = c_\cdot \cdot !addhyph \cdot ! gather_r$ and for $b>0$ and $z_b = y_{l-k}$,

  $$\begin{aligned} \begin{aligned} T^!(match^{R_r(\mathbf {z})}_b) =\,&c_\cdot \cdot [c_\cdot \cdot ! mphypoth \cdot T^!(match^{R_r(\mathbf {z})}_{b-1})] \,\cdot \\&\cdot \, ! [ tran \cdot [tran \cdot project^{\rho _1}_l \cdot match(y_l,b) ] \cdot replace^{a_r+1}_b ]. \end{aligned} \end{aligned}$$

  We can see by induction on b that for every $0\le b \le a_r$,

  $$\begin{aligned} Match,\ !gather_r\! :_{2} \!gather_r\! :_{1} \!( [p_{1}]^{v'_{1}}\wedge \cdots \wedge [p_{a_r}]^{v'_{a_r}} \wedge [R_r]^{v_{a_r +1}}) \vdash \qquad \qquad \qquad \end{aligned}$$
  $$\begin{aligned} \vdash T^!(match^{R_r(\mathbf {z})}_b)\! :_{2} \!match^{R_r(\mathbf {z})}_b\! :_{1} \!\left( \bigwedge [x_i]^{v_i} \wedge \bigwedge [y_i]^{v_{k+i}} \rightarrow \right. \end{aligned}$$
  $$\begin{aligned} \qquad \qquad \rightarrow \left. (ok_1 \wedge \cdots \wedge ok_b \wedge [p_{b+1}]^{v'_{b+1}}\wedge \cdots \wedge [p_{a_r}]^{v'_{a_r}} \wedge [R_r]^{v_{a_r +1}})\right) \end{aligned}$$

  if and only if

  $$\begin{aligned} Match,\ gather_r\! :_{1} \!( [p_{1}]^{v'_{1}}\wedge \cdots \wedge [p_{a_r}]^{v'_{a_r}} \wedge [R_r]^{v_{a_r +1}}) \vdash \qquad \qquad \qquad \end{aligned}$$
  $$\begin{aligned} \vdash match^{R_r({z}_1, \ldots , {z}_{a_r})}_b\! :_{1} \!\left( \bigwedge [x_i]^{v_i} \wedge \bigwedge [y_i]^{v_{k+i}} \rightarrow \right. \end{aligned}$$
  $$\begin{aligned} \qquad \qquad \rightarrow \left. (ok_1 \wedge \cdots \wedge ok_b \wedge [p_{b+1}]^{v'_{b+1}}\wedge \cdots \wedge [p_{a_r}]^{v'_{a_r}} \wedge [R_r]^{v_{a_r +1}})\right) , \end{aligned}$$

  which in turn, as we have seen above, is true if and only if for every $j \in [a_r]$ and $j' \in [k+k']$, if $z_j = x_{j'}$ or $z_j = y_{j'-k}$, then $v'_j=v_{j'}$.

Using the terms (and formulas) we have defined above, we can construct terms $T^a$, where $0<a\le \rho _1$ and eventually $t^\phi$:

Let $\varPsi = \{{\psi }_1, \ldots , {\psi }_{l}\}$ be an ordering of all subformulas of $\psi$ and of variables ${x}_1, \ldots , {x}_{k},{y}_1, \ldots , {y}_{k'}$, which extends the ordering ${x}_1, \ldots , {x}_{k},{y}_1, \ldots , {y}_{k'}$, such that if $a < b$, then $|\psi _a| \le |\psi _b|.$ ⁸ Furthermore, $\rho _0 = |\{a\in [l] \mid \left| {\psi _a}\right| = 0\}|$ ($=k+k'$) and $\rho _1 = |\{a\in [l] \mid \left| {\psi _a}\right| = 1\}|$.

Let $T^1 = value_{z_1}$ and for every $1< a \le \rho _0$, $T^a = [append \cdot T^{a-1} \cdot value_{z_a} ]$. It is not hard to see that for ${v}_1, \ldots , {v}_{k} \in \{\top ,\bot \}$,

$$\begin{aligned} value_{z_1}\! :_{1} \![z_1]^{v_1}, \ldots , value_{z_k}\! :_{1} \![z_k]^{v_k} \vdash T^{\rho _0}\! :_{1} \!([z_1]^{v_1}\wedge \cdots \wedge [z_k]^{v_k}). \end{aligned}$$

(2)

For every $a \in [l]$,

• if $\psi _a = R_r(z_1^a,\ldots ,z^{a}_{a_r})$ , then

  $$\begin{aligned} Eval_a = truth_a\! :_{2} \!([match_{a_r}^{\psi _a} \cdot T^{\rho _0}]\! :_{1} \!({ok}_1 \wedge \cdots \wedge {ok}_{a_r} \wedge [R_r]^{\top })\rightarrow [\psi _a]^{\top }) \wedge \end{aligned}$$
  $$\begin{aligned} \wedge truth_a\! :_{2} \!([match_{a_r}^{\psi _a} \cdot T^{\rho _0}]\! :_{1} \!({ok}_1 \wedge \cdots \wedge {ok}_{a_r} \wedge [R_r]^{\bot })\rightarrow [\psi _a]^{\bot }); \end{aligned}$$

• if $\psi _a = \lnot \gamma$ , then

  $$\begin{aligned} Eval_a = truth_a\! :_{2} \!([\gamma ]^{\top }\rightarrow [\psi _a]^{\bot }) \wedge truth_a\! :_{2} \!([\gamma ]^{\bot }\rightarrow [\psi _a]^{\top }); \end{aligned}$$

• if $\psi _a = \gamma \vee \delta$ , then

  $$\begin{aligned} Eval_a = truth_a\! :_{2} \!([\gamma ]^{\top } \wedge [\delta ]^{\top }\rightarrow [\psi _a]^{\top }) \wedge truth_a\! :_{2} \!([\gamma ]^{\top } \wedge [\delta ]^{\bot }\rightarrow [\psi _a]^{\top }) \end{aligned}$$
  $$\begin{aligned} \wedge \ truth_a\! :_{2} \!([\gamma ]^{\bot } \wedge [\delta ]^{\top }\rightarrow [\psi _a]^{\top }) \wedge truth_a\! :_{2} \!([\gamma ]^{\bot } \wedge [\delta ]^{\bot }\rightarrow [\psi _a]^{\bot }); \end{aligned}$$

• if $\psi _a = \gamma \wedge \delta$ , then

  $$\begin{aligned} Eval_a = truth_a\! :_{2} \!([\gamma ]^{\top } \wedge [\delta ]^{\top }\rightarrow [\psi _a]^{\top }) \wedge truth_a\! :_{2} \!([\gamma ]^{\top } \wedge [\delta ]^{\bot }\rightarrow [\psi _a]^{\bot }) \end{aligned}$$
  $$\begin{aligned} \wedge \ truth_a\! :_{2} \!([\gamma ]^{\bot } \wedge [\delta ]^{\top }\rightarrow [\psi _a]^{\bot }) \wedge truth_a\! :_{2} \!([\gamma ]^{\bot } \wedge [\delta ]^{\bot }\rightarrow [\psi _a]^{\bot }); \end{aligned}$$

• if $\psi _a = \gamma \rightarrow \delta$ , then

  $$\begin{aligned} Eval_a = truth_a\! :_{2} \!([\gamma ]^{\top } \wedge [\delta ]^{\top }\rightarrow [\psi _a]^{\top }) \wedge truth_a\! :_{2} \!([\gamma ]^{\top } \wedge [\delta ]^{\bot }\rightarrow [\psi _a]^{\bot }) \end{aligned}$$
  $$\begin{aligned} \wedge \ truth_a\! :_{2} \!([\gamma ]^{\bot } \wedge [\delta ]^{\top }\rightarrow [\psi _a]^{\top }) \wedge truth_a\! :_{1} \!([\gamma ]^{\bot } \wedge [\delta ]^{\bot }\rightarrow [\psi _a]^{\top }). \end{aligned}$$

Let $Eval = \bigwedge _{a = \rho _0 +1}^l Eval_a$.

For $\rho _0 < a \le \rho _1$, we define $gathrel_a$ in the following way:

$$ gathrel_{\rho _0 +1} = c_\cdot \cdot T^!(match^{\psi _a}_{a_{r_a}}) $$

and for $\rho _0 +1 < a \le \rho _1$,

$$ gathrel_{\rho _0 +1} = appendconc \cdot gathrel_{a-1} \cdot [c_\cdot \cdot T^!(match^{\psi _a}_{a_{r_a}})]. $$

Then,

$$ T^{\rho _0 +1} = replace^{\rho _1 - \rho _0}_1 \cdot truth_{\rho _0 +1} \cdot [gathrel_{\rho _1} \cdot !T^{\rho _0}] $$

and for $\rho _0+1 < a \le \rho _1$,

$$ T^{a} = replace^{\rho _1 - \rho _0}_a \cdot truth_{\rho _0 +1} \cdot T^{a-1}. $$

if $\psi _a = \lnot \psi _{2}$, then

$$ T^a = hypappend \cdot [trans\cdot proj_j^{a - \rho _0 - 1} \cdot truth_a] \cdot T^{a-1} \text { and } $$

if $\psi _a = \psi _{b} \circ \psi _c$, then

$$ T^a = hypappend \cdot [trans\cdot [appendconc \cdot proj_b^{a - \rho _0 - 1} \cdot proj_c^{a-1}] \cdot truth_a] \cdot T^{a-1}. $$

We then define $t^\phi = [right \cdot T^l]$.

Lemma 5

For every $b \in [\rho _1]$, $j \in [a_{r_b}]$, let $\mathbf {l^b}=({l^b}_1, \ldots , {l^b}_{a_{r_b}}) \in \{p_j, \lnot p_j \}^{a_{r_b}}$ and $v^b \in \{\top ,\bot \}$. Assume that for every $b_1,b_2 \in [\rho _1]$, if $r_{b_1} = r_{b_2}$ and $\mathbf {l^{b_1}} = \mathbf {l^{b_2}}$, then it must also be the case that $v^{b_1} = v^{b_2}$. Then,⁹

$$\begin{aligned} \begin{aligned} \bigwedge _{b \in [\rho _1]}!gather_{r_b}\! :_{2} \!gather_{r_b}\! :_{1} \! \left( \mathbf {l^{b}} \wedge [R_{r_b}]^b\right) \wedge Match \wedge Eval \wedge \bigwedge _{z \in Z} val_z\! :_{1} \![z]^{v_z} \vdash \\ \vdash t^\phi \! :_{2} \! [\phi ]^{\top } \end{aligned} \end{aligned}$$

if and only if $\mathcal {M}\models \phi$ for every model $\mathcal {M}$ with universe $\{ \top , \bot \}$ and interpretation $\mathcal {I}$ such that

• for every $z \in Z$, $v_z = \mathcal {I}(z)$,

• for every $b \in [\rho _1]$, $\mathcal {M}\models R_{r_b}(f(l_1^b),\ldots ,f(l^b_{a_{r_b}}))$ iff $v^b = \top$,

where for all $j \in \alpha$, $f(p_j) = \top$ and $f(\lnot p_j) = \bot$.

Proof

The if direction is not hard to see by (induction on) the construction of the terms $T^a, t^\phi$. For the other direction, notice that a $*$-calculus derivation for

$$\begin{aligned} \bigwedge _{b \in [\rho _1]}!gather_{r_b}\! :_{2} \! gather_{r_b}\! :_{1} \! \left( \mathbf {l^{b}}\wedge [R_{r_b}]^{v^b}\right) , \qquad \qquad \end{aligned}$$

$$\begin{aligned} \qquad \qquad Match,\ Eval, \ \bigwedge _{z \in Z} val_z\! :_{1} \![z]^{v_z} \vdash t^\phi \! :_{2} \! [\phi ]^{\top } \end{aligned}$$

gives on the right hand side a derivation of

$$\begin{aligned} \bigwedge _{b \in [\rho _1]}gather_{r_b}\! :_{1} \! \left( \mathbf {l^{b}}\wedge [R_{r_b}]^{v^b}\right) , Match,\ Eval^{\#_2}, \ \bigwedge _{z \in Z} val_z\! :_{1} \![z]^{v_z} \vdash [\phi ]^{\top }. \end{aligned}$$

Some $\chi = [R_r(\mathbf {z}_r^a)]^{\triangle }$, where $R_r(\mathbf {z}_r^a) = \psi _a$, a subformula of $\phi$, can be derived from the assumptions above only if $[match^{\psi _a}_{a_{r_a}} \cdot T^{\rho _0}]\! :_{1} \!(\mathbf {ok}\wedge [R_{r_a}]^\triangle )$ can be derived as well – notice that the assumptions cannot be inconsistent and we can easily adjust a model that does not satisfy $[match^{\psi _a}_{a_{r_a}} \cdot T^{\rho _0}]\! :_{1} \!(\mathbf {ok}\wedge [R_{r_a}]^\triangle )$ so that it does not satisfy $\chi$ either, by simply changing the truth value of $\chi$.

The derivation of $match^{\psi _a}_{a_{r_a}}\! :_{1} \!(\mathbf {ok}\wedge [R_{r_a}]^\triangle )$ is not affected by $Eval^{\#_2}$: if there is a model that satisfies all assumptions except for $Eval^{\#_2}$ and not $match^{\psi _a}_{a_{r_a}}\! :_{1} \!(\mathbf {ok}\wedge [R_{r_a}]^\triangle )$, we can assume the strong evidence property and change the truth-values of every $[\psi _b]^{\triangle '}$ to true, so the new model satisfies all the assumptions and not $[match^{\psi _a}_{a_{r_a}} \cdot T^{\rho _0}]\! :_{1} \!(\mathbf {ok}\wedge [R_{r_a}]^\triangle )$.

Therefore we have a $*$-calculus derivation of $[match^{\psi _a}_{a_{r_a}} \cdot T^{\rho _0}]\! :_{1} \!(\mathbf {ok}\wedge [R_{r_a}]^\triangle )$ and since $gather_r$ only appears once in $match^{\psi _a}_{a_{r_a}}$, there is some $b \in [\rho _1]$ such that (see Lemma 2)

$$\begin{aligned} \begin{aligned} gather_{r_b}\! :_{1} \! \left( \mathbf {l^{b}}\wedge [R_{r_b}]^{v^b}\right) , Match,&\bigwedge _{z \in Z} val_z\! :_{1} \![z]^{v_z} \vdash \\&\vdash [match^{\psi _a}_{a_{r_a}}\cdot T^{\rho _0}]\! :_{1} \!(\mathbf {ok}\wedge [R_{r_a}]^\triangle ). \end{aligned} \end{aligned}$$

Similarly, we can remove the terms from this derivation, so

$$\begin{aligned} \mathbf {l^{b}}, [R_{r_b}]^{v^b}, Match^{\#_1},\ \bigwedge _{z \in Z} [z]^{v_z} \vdash \mathbf {ok}\wedge [R_{r_a}]^\triangle . \end{aligned}$$

From which it is not hard to see that for all $z \in Z$, $v^b = \triangle$, so every first-order model as described in the Lemma satisfies $\chi$. Then it is not hard to see by induction that all such models satisfy all $[\psi _a]^{\triangle }$ derivable from these same assumptions.   $\square$

Now to construct the actual formula the reduction gives. For this let $\rho$ be a fixed justification variable. We define the following formulas.

$$\begin{aligned} start = \lnot [active] \wedge \rho \! :_{3} \!\left( [active] \wedge \bigwedge _{a \in [\alpha ]}var_a\! :_{1} \!\lnot p_a \right) \end{aligned}$$

$$\begin{aligned} forward_A = \rho \! :_{4} \!\left( \bigvee _{a \in [\alpha ]} var_a\! :_{1} \!\lnot p_a \wedge [active] \rightarrow \rho \! :_{3} \![active] \right) \end{aligned}$$

$$\begin{aligned} forward_B = \rho \! :_{4} \! \bigwedge _{a \in [\alpha ]} \left( \bigwedge _{b \in [a-1]} var_b\! :_{1} \!p_b \wedge var_a\! :_{1} \! \lnot p_a \wedge [active] \right. \end{aligned}$$

$$\begin{aligned} \left. \qquad \qquad \rightarrow \rho \! :_{3} \!\left( \bigwedge _{b \in [a-1]} var_b\! :_{1} \! \lnot p_b \wedge var_a\! :_{1} \! p_a \right) \right) \end{aligned}$$

$$\begin{aligned} forward_C = \rho \! :_{4} \! \bigwedge _{a \in [\alpha ]} \left( \bigvee _{b \in [a-1]} var_b\! :_{1} \!\lnot p_{b} \wedge var_a\! :_{1} \! \lnot p_a \wedge [active] \right. \end{aligned}$$

$$\begin{aligned} \left. \qquad \qquad \rightarrow \rho \! :_{3} \! var_a\! :_{1} \! \lnot p_a \right) \end{aligned}$$

$$\begin{aligned} forward_D = \rho \! :_{4} \! \bigwedge _{a \in [\alpha ]} \left( \bigvee _{b \in [a-1]} var_b\! :_{1} \!\lnot p_{b} \wedge var_a\! :_{1} \! p_a \wedge [active] \right. \end{aligned}$$

$$\begin{aligned} \left. \qquad \qquad \rightarrow \rho \! :_{3} \! var_a\! :_{1} \! p_a \right) \end{aligned}$$

$$\begin{aligned} end = \rho \! :_{4} \! \left( \bigwedge _{a \in \alpha } var\! :_{1} \! p_a \wedge [active] \rightarrow \rho \! :_{4} \! \lnot [active]\right) \end{aligned}$$

$$\begin{aligned} choice_R = \rho \! :_{4} \!\left( [active] \rightarrow rel_r\! :_{1} \! [R_r]^\top \vee rel_r\! :_{1} \! [R_r]^\bot \right) \end{aligned}$$

$$\begin{aligned} choice_V = \rho \! :_{4} \!\left( \lnot [active] \rightarrow \bigwedge _{z \in X}\left( value_z\! :_{1} \! [z]^\top \vee value_z\! :_{1} \! [z]^\bot \right) \right. \end{aligned}$$

$$\begin{aligned} \left. \qquad \qquad \wedge \bigwedge _{z \in Y}\left( value_z\! :_{1} \! [z]^\top \wedge value_z\! :_{1} \! [z]^\bot \right) \right) \end{aligned}$$

$$\begin{aligned} test = \rho \! :_{4} \! \left( \lnot [active] \rightarrow Match \wedge Eval \wedge \lnot t^{\phi }\! :_{2} \! [\lnot \phi ]^T \right) \end{aligned}$$

Then, $\phi ^J_{FO}$, the formula constructed by the reduction is the conjunction of these formulas above:

$$\begin{aligned} start \wedge forward_A \wedge forward_B \wedge forward_C \wedge forward_D \wedge end \wedge \\ \wedge \, choice_R \wedge choice_V \wedge test. \end{aligned}$$

Theorem 3

$\phi ^J_{FO}$ is J-satisfiable if and only if $\phi$ is satisfiable by a two-element first-order model.

Proof

First, assume $\phi$ is satisfiable by two-element first-order model, say $\mathcal {M}$ with interpretation $\mathcal {I}$, and assume that for every $a \in [k]$, $\mathcal {I}(x_a)$ is such that $\mathcal {M}\models {\forall y}_1, \ldots , {\forall y}_{k'} \psi$. We construct a J-model for $\phi ^J_{FO}$:

$$\mathcal {M}_J = (W,R_1,R_2,R_3,R_4,{\mathcal {E}},\mathcal {V}) \text {, where: }$$

• $W = \{ \sigma \in \mathbb {N}\mid \sigma +2 \in [2^\alpha + 2] \}$ (i.e. $\sigma \in \{ -1, 0, 1, 2, \ldots 2^\alpha \}$);

• $R_1 = R_2 = \emptyset$, $R_3 = \{ (\sigma ,\sigma +1) \mid \sigma <2^\alpha \}\cup \{(2^\alpha ,2^\alpha ) \}$, and $R_4 = \{ (\sigma ,\sigma ') \mid \sigma < \sigma ' \} \cup \{(2^\alpha ,2^\alpha ) \}$;

• ${\mathcal {E}}$ is minimal such that

  • ${\mathcal {E}}_3(\rho ,\chi ) = {\mathcal {E}}_4(\rho ,\chi ) = W$ for any formula $\chi$,

  • ${\mathcal {E}}_1(var_a,p_a) = \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ] \text { and } bin_a(\sigma ) = 1 \}$,

  • ${\mathcal {E}}_1(var_a,\lnot p_a) = \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ] \text { and } bin_a(\sigma ) = 0 \}$,

  • ${\mathcal {E}}_1(rel_r,[R_r]^\top ) = \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ]$ and $\mathcal {M}\models R_r(bin_0(\sigma ),\ldots ,bin_{a_r}(\sigma )) \}$,

  • ${\mathcal {E}}_1(rel_r,[R_r]^\bot ) = \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ]$ and $\mathcal {M}\not \models R_r(bin_0(\sigma ),\ldots ,bin_{a_r}(\sigma )) \}$,

  • for every $a \in [k]$, ${\mathcal {E}}_1(value_{x_a},[x_a]^\top ) = \{ 2^\alpha \}$, if $\mathcal {I}(x_a) = \top$ and $\emptyset$ otherwise,

  • for every $a \in [k]$, ${\mathcal {E}}_1(value_{x_a},[x_a]^\bot ) = \{ 2^\alpha \}$, if $\mathcal {I}(x_a) = \bot$ and $\emptyset$ otherwise,

  • for every $a \in [k']$, ${\mathcal {E}}_1(value_{y_a},[y_a]^\top ) = {\mathcal {E}}_i(value_{y_a},[y_a]^\bot ) = \{ 2^\alpha \}$, and

  • $\mathcal {M}_J,2^\alpha \models Match, Eval$;

• $\mathcal {V}([active]) = \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ] \}$ and for any other propositional variable q, $V(q) = \emptyset$.

It is not hard to verify that $\mathcal {M}_J,-1 \models \phi _{FO}^J$, as long as we establish that , for which it is enough that $2^\alpha \notin {\mathcal {E}}_j(t^\phi ,[\lnot \phi ]^\top )$.

The definition of ${\mathcal {E}}$ is equivalent to $\sigma \in {\mathcal {E}}_g(s,\chi ) \Leftrightarrow S \vdash _* \sigma \ *_g(s,\chi )$, where $S =$

$$\begin{aligned} \{ w\ *_3(\rho ,F)\mid w \in W, F \text { a formula}\}\cup \{ w\ *_4(\rho ,F)\mid w \in W, F \text { a formula}\}\ \cup \end{aligned}$$

$$\begin{aligned} \{ w\ *_1(var_a,p_a)\mid w+1 \in [2^\alpha ] \text { and } bin_a(w) = 1\}\ \cup \end{aligned}$$

$$\begin{aligned} \{ w\ *_1(var_a,\lnot p_a)\mid w+1 \in [2^\alpha ] \text { and } bin_a(w) = 0\}\ \cup \end{aligned}$$

$$\begin{aligned} \{ w\ *_1(rel_r,[R_r]^\top )\mid w+1 \in [2^\alpha ] \text { and } \mathcal {M}\models R_r(bin_0(w),\ldots ,bin_{a_r}(w)) \}\ \cup \end{aligned}$$

$$\begin{aligned} \{ w\ *_1(rel_r,[R_r]^\bot )\mid w+1 \in [2^\alpha ] \text { and } \mathcal {M}\not \models R_r(bin_0(w),\ldots ,bin_{a_r}(w)) \}\ \cup \end{aligned}$$

$$\begin{aligned} \{2^\alpha \ *_1(value_{x_a},[x_a]^\top ) \mid a\in [k],\ \mathcal {I}(x_a) = \top \}\ \cup \end{aligned}$$

$$\begin{aligned} \{ 2^\alpha \ *_1(value_{x_a},[x_a]^\bot ) \mid a\in [k],\ \mathcal {I}(x_a) = \bot \} \ \cup \end{aligned}$$

$$\begin{aligned} \{ 2^\alpha \ *_1(value_{y_a},[y_a]^\top ) \mid a\in [k']\} \cup \{ 2^\alpha \ *_1(value_{y_a},[y_a]^\bot ) \mid a\in [k'] \} \ \cup \end{aligned}$$

$$\begin{aligned} \{2^\alpha \ e \mid e \in *Eval \cup *Match \} \end{aligned}$$

Then, $2^\alpha \in {\mathcal {E}}_2(t^\phi ,[\lnot \phi ]^\top )$ iff $S \vdash _* 2^\alpha *_2(t^\phi ,[\lnot \phi ]^\top )$. Notice the following: since $t^\phi$ does not have $\rho$ as a subterm, the $*$-expressions in

$$\begin{aligned} \{ w\ *_3(\rho ,F)\mid w \in W, F \text { a formula}\}\cup \{ w\ *_4(\rho ,F)\mid w \in W, F \text { a formula}\} \end{aligned}$$

cannot be a part of a derivation for $S \vdash _* 2^\alpha *_2(t^\phi ,[\lnot \phi ]^\top )$.

Since $1 \hookleftarrow 2 \hookleftarrow 3$ and 1, 2 do not interact with any agents in any other way, for any term s with no !, if for some a or r, $var_a$ or $rel_r$ are subterms os s, if $S \vdash _* w\ s\! :_{a} \!\chi$, then $a=1$, $0\le w < 2^\alpha$, and $\{ w\ e \in S \} \vdash _* w\ s\! :_{1} \!\chi$. $t^\phi$ includes exactly one $!gather_{r_b}$ for every b and one of $value_z$ for every $z \in Z$. Therefore, if $S \vdash _* 2^\alpha *_2(t^\phi ,[\lnot \phi ]^\top )$, then there are

$$\begin{aligned} \bigwedge _{b \in [\rho _1]}!gather_{r_b}\! :_{2} \!gather_{r_b}\! :_{1} \! \varPhi \wedge Match \wedge Eval \wedge \bigwedge _{z \in Z} val_z\! :_{1} \![z]^{v_z} \vdash t^\phi \! :_{2} \! [\lnot \phi ]^{\top } \end{aligned}$$

and by Lemma 5, $\mathcal {M}\models \lnot \phi$, a contradiction.

On the other hand, let there be some $\mathcal {M}'_J$ where $\phi ^J$ is satisfied. Then, we name $-1$ a state where $\mathcal {M}'_J,-1 \models \phi ^J$ and let $-1 R_3 0 R_3 1 R_3 \cdots R_3 2^\alpha$. Then,

• ${\mathcal {E}}_1(var_a,p_a) \subseteq \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ] \text { and } bin_a(\sigma ) = 1 \}$,

• ${\mathcal {E}}_1(var_a,\lnot p_a) \subseteq \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ] \text { and } bin_a(\sigma ) = 0 \}$,

• $\mathcal {M}_J,2^\alpha \models Match, Eval$ and for every $a \in [k'],$ $\mathcal {M}_J,2^\alpha \models value_{y_a}\! :_{1} \![y_a]^\top , value_{y_a}\! :_{1} \![y_a]^\bot$;

as we can see by induction on $\sigma$ - the conditions on $A_1(var_a,p_a),A_1(var_a,\lnot p_a)$ as imposed by $forward_B,\ forward_C,\ forward_D$ are positive. Notice here that if for some $0\le w<2^\alpha -1$, $w \in \bigcap _{a \in \alpha }{\mathcal {E}}_1(var_a,p_a)$, then we have a contradiction: $w+1 \models \lnot [active]$ and if w is minimal for this to happen, then $w \models [active]$, so since there is some a s.t. $w \in {\mathcal {E}}_1(var_a,\lnot p_a)$, $w+1 \models [active]$ (by $forward_A$).

Then, $\{w\mid w+1 \in [2^\alpha ] \} \subseteq {\mathcal {E}}_1(rel_r,[R_r]^\top ) \cup {\mathcal {E}}_1(rel_r,[R_r]^\bot )$ and then we can define a first-order model $\mathcal {M}$ such that:

• ${\mathcal {E}}_1(rel_r,[R_r]^\top ) \subseteq \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ] \text { and } \mathcal {M}\models R_r(bin_0(\sigma ),\ldots ,bin_{a_r}(\sigma )) \}$,

• ${\mathcal {E}}_1(rel_r,[R_r]^\bot ) \subseteq \{ \sigma \in W \mid \sigma +1 \in [2^\alpha ] \text { and } \mathcal {M}\not \models R_r(bin_0(\sigma ),\ldots ,bin_{a_r}(\sigma )) \}$,

• for every $a \in [k]$, ${\mathcal {E}}_1(value_{x_a},[x_a]^\top ) \subseteq \{ 2^\alpha \}$, if $\mathcal {I}(x_a) = \top$ and $\emptyset$ otherwise,

• for every $a \in [k]$, ${\mathcal {E}}_1(value_{x_a},[x_a]^\bot ) \subseteq \{ 2^\alpha \}$, if $\mathcal {I}(x_a) = \bot$ and $\emptyset$ otherwise.

Since it must be the case that , it cannot be the case that

$$\begin{aligned} \bigwedge _{b \in [\rho _1]}!gather_{r_b}\! :_{2} \!gather_{r_b}\! :_{1} \! \varPhi \wedge Match \wedge Eval \wedge \bigwedge _{z \in Z} val_z\! :_{1} \![z]^{v_z} \vdash t^\phi \! :_{2} \! [\lnot \phi ]^{\top } \end{aligned}$$

and since $\mathcal {M}$ satisfies the conditions from Lemma 5, .    $\square$