Rules with parameters in modal logic II

TL;DR

This paper classifies the computational complexity of admissibility and unifiability problems with parameters in transitive modal logics, providing precise complexity bounds for a broad class of such logics.

Contribution

It offers a complete complexity classification for unifiability and inadmissibility in cluster-extensible (clx) logics, including parameterized and parameter-free cases, with general lower bounds.

Findings

Complexity classified as $ ext{Sigma}^{ ext{exp}}_2$, NEXP, coNEXP, PSPACE, or $ ext{Pi}^p_2$.

Upper bounds specific to clx logics and related classes.

Lower bounds applicable to broad classes of transitive logics.

Abstract

We analyze the computational complexity of admissibility and unifiability with parameters in transitive modal logics. The class of cluster-extensible (clx) logics was introduced in the first part of this series of papers. We completely classify the complexity of unifiability or inadmissibility in any clx logic as being complete for one of $\Sigma^{\exp}_2$, NEXP, coNEXP, PSPACE, or $\Pi^p_2$. In addition to the main case where arbitrary parameters are allowed, we consider restricted problems with the number of parameters bounded by a constant, and the parameter-free case. Our upper bounds are specific to clx logics, but we also include similar results for logics of bounded depth and width. In contrast, our lower bounds are very general: they apply each to a class of all transitive logics whose frames allow occurrence of certain finite subframes. We also discuss the baseline problem of complexity of derivability: it is coNP-complete or PSPACE-complete for each clx logic. In particular, we prove PSPACE-hardness of derivability for a broad class of transitive logics that includes all logics with the disjunction property.

Tables

Table 1. Table 1: Complexity of nonderivability, unifiability, and inadmissibility problems for clx logics. Note: results in the parameter-free column only apply to inadmissibility, not unifiability.

logic		${⊬}_L$	unifiability, ${/\sim }_L$			examples
branching	cluster		parameters:
	size		no	$O\left(1\right)$	any
$0$					${\Pi }_2^p$	$\mathrm{𝐒𝟓}\oplus {\mathrm{𝐀𝐥𝐭}}_k$, $\mathrm{𝐕𝐞𝐫𝐮𝐦}$
	$\infty$	$\mathrm{NP}$			$\mathrm{coNEXP}$	$\mathrm{𝐒𝟓}$, $\mathrm{𝐊𝟒𝐁}$
$1$				$\mathrm{PSPACE}$		$\mathrm{𝐆𝐋}.3$, $\mathrm{𝐒𝟒𝐆𝐫𝐳}.3$
	$\infty$				$\mathrm{coNEXP}$	$\mathrm{𝐒𝟒}.3$, $\mathrm{𝐊𝟒}.3$
$\ge 2$		$\mathrm{PSPACE}$	$\mathrm{NEXP}$			$\mathrm{𝐆𝐋}$, $\mathrm{𝐊𝟒𝐆𝐫𝐳}$, $\mathrm{𝐒𝟒𝐆𝐫𝐳}$
	$\infty$				${\Sigma }_2^{\exp }$	$\mathrm{𝐊𝟒}$, $\mathrm{𝐒𝟒}$, ${\mathrm{𝐊𝟒𝐁𝐁}}_k$

Equations

$$[R]=\{\begin{array}{ll}1& \text{if R is true,}\\ 0& \text{otherwise.}\end{array}$$

$${\mathrm{DP}}_n$$

$$\beta_{u}=\begin{cases}\displaystyle\bigwedge_{v>u}\Diamond\beta_{v}\land\Box\bigvee_{v>u}\beta_{v},&\operatorname{refl}(u)={\bullet},\\[18.0pt] \displaystyle\Diamond\Bigl{(}\bigwedge_{v\gneq u}\Diamond\beta_{v}\Bigr{)}\land\Box\Bigl{(}\bigvee_{v\gneq u}\beta_{v}\lor\Diamond\bigwedge_{v\gneq u}\Diamond\beta_{v}\Bigr{)},&\operatorname{refl}(u)={\circ}.\end{cases}$$

$$u^{\prime }$$

$$u$$

$$\mathrm{P}$$

$$\mathrm{EXP}$$

$$\mathrm{PSPACE}=\mathrm{DSPACE}\bigl{(}\operatorname{poly}(n)\bigr{)}.$$

$$\mathrm{NP}$$

$$\mathrm{NEXP}$$

$${\Sigma }_k^p$$

$${\Sigma }_k^{\exp }$$

$$\mathrm{AP}=\mathrm{PSPACE}.$$

$${\Sigma }_k^p$$

$${\Sigma }_k^{\exp }$$

$$Q_0{x}_0{Q}_1{x}_1\dots Q_{n-1}{x}_{n-1}\phi (\vec{x}),$$

$$M_w\models P_a(i)\text{iff}{w}_i=a.$$

$$w\in L\text{iff}{M}_w\models \Phi .$$

$$\exists X_1\subseteq \mathcal{P}(n)\forall X_2\subseteq \mathcal{P}(n)\dots Q{X}_k\subseteq \mathcal{P}(n)\overline{Q}{t}_0,\dots ,t_{m-1}\subseteq n\phi$$

$$\exists {\vec{X}}_1\forall {\vec{X}}_2\dots \exists {\vec{X}}_k\Psi ({\vec{X}}_1,\dots ,{\vec{X}}_k),$$

$$\exists \xi Q_0{t}_0\dots Q_l{t}_l\psi$$

$$\displaystyle\Leftrightarrow\exists s\>Q_{0}t_{0}\,\dots\,Q_{l}t_{l}\>\bigl{(}s\neq\varnothing\land\forall\xi\,(s(\xi)\to\psi)\bigr{)},$$

$$\Phi =\exists {\vec{X}}_1\forall {\vec{X}}_2\dots \exists {\vec{X}}_k\forall t_0\exists s_1\forall t_1\dots \forall t_{l-1}\exists s_l\psi ({\vec{X}}_1,\dots ,{\vec{X}}_k,\vec{t},\vec{s}),$$

$$\exists\vec{X}_{1}\>\forall\vec{X}_{2}\,\dots\,\exists\vec{X}_{k}\>\exists Y_{1}\,\dots\exists Y_{l}\>\forall t_{0}\,\dots\,\forall t_{l-1}\\ \psi\bigl{(}\vec{X}_{1},\dots,\vec{X}_{k},\vec{t},\{\xi:Y_{1}(t_{0},\xi)\},\dots,\{\xi:Y_{l}(t_{0},\dots,t_{l-1},\xi)\}\bigr{)},$$

$$\exists\vec{X}_{1}\>\forall\vec{X}_{2}\,\dots\,\exists\vec{X}_{k}\>\exists Y_{1}\,\dots\exists Y_{l}\>\forall t_{0}\,\dots\,\forall t_{2l-1}\>\bigl{(}\gamma(\vec{Y},\vec{t})\to\psi(\vec{X}_{1},\dots,\vec{X}_{k},\vec{t})\bigr{)},$$

$$\bigwedge_{i<l}\forall\xi\,\bigl{(}t_{l+i}(\xi)\leftrightarrow Y_{i+1}(t_{0},\dots,t_{i},\xi)\bigr{)}.$$

$$\{⟨⟨\xi ,i⟩,⟨\xi ,j⟩⟩:\xi <n\text{ and }i,j<(l+1{)}^2\}$$

$$w\in L\text{iff}{M}_w\models \Phi \text{iff}{M}_w^{\ast }\models {\Phi }^{\ast }.$$

$$X^{*}=\bigcup_{i<l}\bigl{\{}t\times\{i\}:t\in X_{i}\bigr{\}}.$$

$$\bigcup_{i<l}\bigl{\{}t\times\{i\}:t\in X_{i}\bigr{\}}\\ \cup\bigcup_{i=1}^{l}\Bigl{\{}\bigcup_{j<i}\bigl{(}t_{j}\times\{i(l+1)+j\}\bigr{)}\cup\bigl{(}\{\xi\}\times\{i(l+1)+l\}\bigr{)}:\langle t_{0},\dots,t_{i-1},\xi\rangle\in Y_{i}\Bigr{\}}.$$

$$\exists X^{*}_{1}\>\forall X^{*}_{2}\,\dots\,\exists X^{*}_{k}\>\forall\vec{t}_{0}\,\dots\,\forall\vec{t}_{2l-1}\>\bigl{(}\gamma^{*}(X^{*}_{k},\vec{t}_{0},\dots,\vec{t}_{2l-1})\to\psi^{*}(X^{*}_{1},\dots,X^{*}_{k},\vec{t}_{0},\dots,\vec{t}_{2l-1})\bigr{)},$$

$$\bigwedge_{\begin{subarray}{c}i<2l\\ \hbox to0.0pt{\hss$\scriptstyle j,j^{\prime}<(l+1)^{2}$\hss}\end{subarray}}\forall\xi\,\bigl{(}t_{i,j^{\prime}}(\xi)\leftrightarrow C_{j^{\prime}}(\xi)\land\exists\eta\,\bigl{(}C_{j}(\eta)\land E(\xi,\eta)\land t_{i,j}(\eta)\bigr{)}\bigr{)},$$

$$\bigwedge_{i=1}^{l}\forall\xi\>\Bigl{(}t_{l+i-1,i(l+1)+l}(\xi)\leftrightarrow X^{*}_{k}\Bigl{(}\bigcup_{j<i}t_{j,i(l+1)+j}\cup\{\xi\}\Bigr{)}\Bigr{)}.$$

Full text

Our upper bounds are specific to clx logics, but we also include similar results for logics of bounded depth and width. In contrast, our lower bounds are very general: they apply each to a class of all transitive logics whose frames allow occurrence of certain finite subframes.

We also discuss the baseline problem of complexity of derivability: it is $\mathrm{coNP}$-complete or $\mathrm{PSPACE}$-complete for each clx logic. In particular, we prove $\mathrm{PSPACE}$-hardness of derivability for a broad class of transitive logics that includes all logics with the disjunction property.

Keywords: modal logic, computational complexity, admissible rule, equational unification

MSC (2020): 03B45, 68Q17

1 Introduction

In this paper, we continue the analysis of admissible rules with parameters (constants) in transitive modal logics satisfying certain extension properties started in Jeřábek [8]. We recall that the first part was devoted to structural results. We introduced the class of cluster-extensible (clx) logics, encompassing the most common transitive modal logics such as $\mathbf{K4}$, $\mathbf{S4}$, $\mathbf{GL}$, $\mathbf{S4Grz}$, $\mathbf{S4.3}$, and many others. We proved that in the setting of rules with parameters, all formulas have projective approximations in any clx logic $L$, whence $L$-admissibility is decidable, and we can compute finite complete sets of $L$-unifiers to any given formula. We provided semantic characterization of $L$-admissibility in terms of certain classes of frames (called $L$-extensible), and axiomatizations of $L$-admissible rules by explicit bases.

The topic of this second part is the computational complexity of admissibility with parameters, and of the closely related problem of unifiability, in clx and other transitive logics. We mention that the complexity of admissibility in transitive modal logics was previously studied in [5]: the main results were that admissibility in certain logics (called extensible) is either $\mathrm{coNP}$-complete or $\mathrm{coNEXP}$-complete depending on if the logic is linear (i.e., of width $1$) or not; the lower bound, stating that admissibility is $\mathrm{coNEXP}$-hard, was proved under a weak hypothesis applicable to a larger class of logics. The class of extensible logics of [5] is incomparable with the clx logics of [8]: on the one hand, the condition of extensibility only constraints frames with a one-element root cluster, hence in this sense it is less restrictive; on the other hand, the definition of extensibility in [5] did not accommodate nonlinear logics of bounded branching. However, the principal difference is that [5] only considered admissibility without parameters.

As we will see, the introduction of parameters leads to a richer and more complicated landscape: we will encounter several more complexity classes than just $\mathrm{coNP}$ and $\mathrm{coNEXP}$, and while linearity of the logic will remain an important dividing line, the complexity of the problem will also be influenced by other factors, the most important being if the logic allows clusters of unbounded size.

On the other hand, the usage of parameters makes our results on complexity more robust, and simpler to formulate. This is most clearly seen for lower bounds: first, they apply already to the special case of unifiability rather than to the full (in)admissibility problem, and second, they only require weak and easily checkable assumptions on the logics, such as being of width $\geq 2$, or having unbounded cluster size. (In contrast, the parameter-free $\mathrm{coNEXP}$ lower bound from [5] only applies to admissibility, and relies on a peculiar extensibility condition on the logic.) In general, our lower bounds will have the form that $L$-unifiability is $\mathcal{C}$-hard (for a particular complexity class $\mathcal{C}$) whenever certain finite frames may be embedded into $L$-frames, or more precisely, when there exist $L$-frames that subreduce or weakly subreduce to said finite frames; see below for definitions.

Wherever possible, we also include results on the complexity of restricted unifiability or admissibility problems in which only a constant number of parameters are allowed, though in this case the conditions on logics get more complicated, and do not seem optimal.

In contrast to lower bounds, decent upper bounds can be proved only for well-behaved logics, as random transitive modal logics may be quite wild, with already the set of tautologies being of high complexity or even undecidable. We are primarily interested in the case of clx logics, and one of the goals of this paper is to find a complete classification of the complexity of unifiability and admissibility in clx logics, both in the regime with arbitrary parameters, and with only constantly many parameters.

Additionally, we present upper bounds on the complexity of admissibility and unifiability in logics of bounded depth and width. To this end, we need first to prove a few structural results on admissibility in logics of bounded depth—in particular, semantical characterizations—since such logics are not covered by the framework from [8].

Similar to clx logics, logics of bounded depth and width are tame and well behaved, which allows us to prove interesting general results about their complexity. However, the class of these logics is structurally quite different from the class of clx logics. Clx logics are few and far between, they are particularly nice logics cherry-picked from the lattice $\operatorname{NExt}\mathbf{K4}$ of all transitive logics, both weak and strong. In contrast, logics of bounded depth and width form an ideal in $\operatorname{NExt}\mathbf{K4}$: in particular, all extensions of any logic from this class are also in the class. Thus, logics of bounded depth and width may be construed as a toy model that is representative of all well-behaved logics, whereas it may easily happen that there are classes of nice logics whose properties are quite different from clx logics. In fact, as we will see in the sequel, there are reasonable classes of nice non-clx logics, including logics with a single top cluster such as $\mathbf{S4.2}$, and some of these have different complexity of unifiability and admissibility from what we will encounter in this paper. These cases duly manifest already for logics of bounded depth and width, and for this reason we cannot give a complete classification of complexity of unifiability in these logics in the present paper.

We acknowledge that this guiding principle should not be taken too seriously: for example, we will also see that there is an interesting class of logics for which unifiability and admissibility are $\mathrm{PSPACE}$-complete, which cannot happen for logics of bounded depth and width, and likewise for all nontrivial results concerning the setting with constantly many parameters.

The main focus of the paper is on the complexity of admissibility and unifiability, but as a starting point, we also settle the complexity of derivability in clx logics. Generalizing results of Ladner [10], we show that nonlinear clx logics are $\mathrm{PSPACE}$-complete. For the lower bound, we prove $\mathrm{PSPACE}$-hardness for a broad class of transitive logics that includes all logics with the disjunction property, and many other logics such as $\mathbf{S4.2}$: similar to our lower bounds on unifiability, the result applies to all transitive logics $L$ such that, roughly speaking, all finite trees may be embedded into $L$-frames.

In the planned third part of this series of papers, we will adapt the set-up of clx logics to logics with a single top cluster such as $\mathbf{K4.2}$ and $\mathbf{S4.2}$, including both structural results as in [8], and computation complexity results as here. Among other things, this will allow us to complete the classification of the complexity of unifiability and admissibility for logics of bounded depth and width, and to obtain a complete classification of hereditary properties of transitive logics that guarantee hardness of unifiability for some complexity class. Both of these suggest that our results on complexity are in a certain sense optimal. We also plan to adapt our results to superintuitionistic logics.

1.1 Overview of results

The linear organization of the paper is as follows. Section 2 contains a few preliminary definitions and facts; its Subsection 2.1 reviews the needed background in complexity theory, including a proof of completeness of certain problems for levels of the exponential hierarchy.

Section 3 deals with the complexity of derivability.

Section 4 is devoted to upper bounds on the complexity of admissibility and unifiability in certain logics: nonlinear and linear clx logics in Subsections 4.1 and 4.2 (respectively), and logics of bounded depth (and, apart from structural results, bounded width) in Subsection 4.3.

Section 5 presents lower bounds on the complexity of unifiability and admissibility. Hardness results for levels of the exponential hierarchy ($\mathrm{NEXP}$, $\mathrm{coNEXP}$, $\Sigma^{\exp}_{2}$) appear in Subsection 5.1, except for results in the setting with a constant number of parameters, which are more complicated and are relegated to Subsection 5.2. Hardness results for $\mathrm{PSPACE}$ and levels of the polynomial hierarchy are in Subsection 5.3.

Section 6 concludes the paper.

A summary of results on the complexity of derivability, unifiability, and admissibility in consistent clx logics is given in Table 1. Each entry in the table should be understood so that the stated problem is complete for the complexity class indicated, for every clx logic that meets the description. Notice that for a given logic, unifiability and admissibility usually have dual complexity, because unifiability is a special case of inadmissibility; in order to avoid confusing switching between dual complexity classes, we adopt in this overview the convention to indicate the complexity of unifiability and inadmissibility rather than admissibility. In accordance with this, we also indicate the complexity of nonderivability (or equivalently: local satisfiability) rather than derivability. However, detailed statements of theorems later in the paper will often mention both.

The referee expressed surprise that some of these classes are existential and some universal. On the most basic level, unifiability and inadmissibility are existential properties as they amount to the existence of certain substitutions, but this is an unbounded existential quantifier, and even though our results also imply computable bounds, this usually makes a quite inefficient test. We rely instead on semantic criteria characterizing inadmissibility by the existence of certain finite models, and depending on properties of the logic, different quantifiers in this characterization become dominant.

Roughly speaking, in the $\Sigma^{\exp}_{2}$ case, the outer $\exists$ quantifies over a model, and the inner $\forall$ comes from verification of pseudoextensibility of the model, quantifying over valuations of parameters in a cluster. If cluster size or the number of parameters is bounded, the $\forall$ becomes polynomial-size and disappears, leading to $\mathrm{NEXP}$. If the logic is linear, the model is an upside-down tree of clusters, and rather than fixing it beforehand, we can explore it one branch at a time; this leads to $\mathrm{coNEXP}$ as the outer $\exists$ disappears. If both restrictions are met, we are left with only polynomial-size quantifiers: basically, alternating $\forall$ over parameter valuations with $\exists$ over variable valuations. This gives $\mathrm{PSPACE}$; furthermore, if the logic has bounded depth, the number of alternations is likewise bounded, leading to $\Pi^{p}_{2d}$.

Here is a cross-reference of our complexity results sorted according to complexity classes:

• •

$\Sigma^{\exp}_{2}$

• –

Upper bounds: inadmissibility in clx logics (Thm. 4.2) and in logics of bounded depth and width (Thm. 4.25).

• –

Lower bound: unifiability in logics with frames weakly subreducing to ({\circ}+{\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle n\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle n\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle n\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle n\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}})^{\circ} (Thm. 5.10).

• •

$\mathrm{NEXP}$

• –

Upper bounds: inadmissibility in clx logics with bounded cluster size or bounded number of parameters (Thm. 4.2), inadmissibility in tabular logics (Thm. 4.20).

• –

Lower bounds: unifiability in nonlinear logics (Thm. 5.3), unifiability with $O(1)$ parameters in certain logics (Thms. 5.15, 5.18, 5.20, Cor. 5.16), inadmissibility without parameters in certain logics (Thm. 5.23).

• •

$\mathrm{coNEXP}$

• –

Upper bounds: inadmissibility in linear clx logics (Thm. 4.3) and in linear logics of bounded depth (Thm. 4.21).

• –

Lower bound: unifiability in logics of unbounded cluster size (Thm. 5.6).

• •

$\mathrm{PSPACE}$

• –

Upper bounds: (non)derivability in clx logics (Thm. 3.3), (in)admissibility in linear clx logics with bounded cluster size or with $O(1)$ parameters (Thm. 4.3).

• –

Lower bounds: (non)derivability in logics subframe-universal for trees (Thm. 3.12, cf. Cor. 3.13), unifiability with $O(1)$ parameters in logics of unbounded depth (Thms. 5.25, 5.31).

• •

$\Pi^{p}_{2d}$

• –

Upper bound: inadmissibility in linear tabular logics (Thm. 4.21, cf. Cor. 4.22).

• –

Lower bound: unifiability in logics of depth $\geq d$ (Thm. 5.25).

• •

$\mathrm{NP}$

• –

Upper bounds: nonderivability in consistent linear clx logics (Thm. 3.2), unifiability with $O(1)$ parameters in logics of bounded depth (Thm. 4.6), inadmissibility with $O(1)$ parameters in logics of bounded depth and width (Thm. 4.19), inadmissibility without parameters in consistent linear clx logics [5, Thm. 2.6].

• –

Lower bound: unifiability without parameters in consistent logics (Thm. 5.2).

2 Preliminaries

This paper is a continuation of [8], and we assume the reader has access to that paper. We generally follow the same terminology and notational conventions as in [8], which we shall not repeat here, as it would considerably add to the length of the paper. In particular, we assume the reader is familiar with the content of [8, §2], which lays out our basic concepts and terminology. Moreover, we will rely on the definition of clx logics (Def. 4.1) and their main structural properties (§4.3); the definition of tight predecessors and extensible frames (Def. 5.1) along with the ensuing semantical characterization of admissibility in clx logics (Thm. 5.18); and the characterization of admissibility in terms of pseudoextensible models (Def. 5.21, Thm. 5.24).

We stress that unless stated otherwise, admissibility refers to admissibility with arbitrary parameters, and similarly for unification and other related notions.

All logics in this paper are normal modal logics extending $\mathbf{K4}$, which we will not always state explicitly.

As a piece of a more obscure notation, we recall from [8] that $\mathbf{2}=\{0,1\}$; if $P$ is a finite set of formulas (in this paper, typically $P\subseteq\mathrm{Par}$), then $\mathbf{2}^{P}$ is the set of all assignments $t\colon P\to\mathbf{2}$, and for any $t\in\mathbf{2}^{P}$, we put $P^{t}=\bigwedge_{\varphi\in P}\varphi^{t(\varphi)}$, where $\varphi^{1}=\varphi$, $\varphi^{0}=\neg\varphi$.

If $n\in\omega$ is a natural number (which we take to include [math]), we will sometimes denote the set $\{0,\dots,n-1\}=\{i:i<n\}$ as just $n$. (This in fact agrees with the common von Neumann definition of natural numbers.) Given an indexed sequence $P=\{\varphi_{i}:i<n\}$ and $t\in\mathbf{2}^{n}$, we extend the notation above so that $P^{t}=\bigwedge_{i<n}\varphi_{i}^{t(i)}$. Finally, we will use this notation also for subsets $t\subseteq n$, that are identified in this context with their characteristic functions: that is, $P^{t}=\bigwedge_{i<n}\varphi_{i}^{[i\in t]}$. Here, $[\dots]$ is the Iverson bracket: for any predicate $R$,

[TABLE]

The set of all subsets of $n$ is denoted $\mathcal{P}(n)$.

In accordance with [8, §5.1], we define a logic $L$ to have the disjunction property if it admits the rules

[TABLE]

for all $n\in\omega$, or equivalently, for $n=0,2$ (the admissibility of $\mathrm{DP}_{0}$ being equivalent to the consistency of $L$).

If $C$ is a cluster or a point in a model, a cluster type, or an extension condition, let $\operatorname{refl}(C)\in\{{\bullet},{\circ}\}$ denote its reflexivity: $\operatorname{refl}(C)={\bullet}$ if $C$ is irreflexive, and $\operatorname{refl}(C)={\circ}$ if it is reflexive.

Recall that a frame $\langle V,{\prec},B\rangle$ is a generated subframe of $\langle W,{<},A\rangle$ (written as $V\subseteq\mathrel{\cdot}\!W$) if $V\subseteq W$, ${\prec}={<}\cap(V\times W)$ (which implies $V\mathord{\uparrow}\subseteq V$), and $B=\{X\cap V:X\in A\}$. The disjoint sum of frames $\langle W_{i},<_{i},A_{i}\rangle$ ($i\in I$), denoted $\sum_{i\in I}W_{i}$, is the frame $\langle W,<,A\rangle$ whose underlying set $W$ is the disjoint union $\mathop{\dot{\bigcup}}_{i\in I}W_{i}$, ${<}=\bigcup_{i\in I}<_{i}$, and $A=\{X\subseteq W:\forall i\in I\,(X\cap W_{i}\in A_{i})\}$. A subreduction of $\langle W,{<},A\rangle$ to $\langle V,{\prec},B\rangle$ (see [3, §9.1]) is a partial map $f\colon W\to V$ such that

1. (i)

$Y\in B\implies f^{-1}[Y]\in A$, 2. (ii)

$w<w^{\prime}\implies f(w)\prec f(w^{\prime})$, and 3. (iii)

$f(w)\prec v\implies\exists w^{\prime}>w\,f(w^{\prime})=v$

for all $w,w^{\prime}\in W$, $v\in V$, and $Y\subseteq V$. If $V$ is a (Kripke) finite frame, condition (i) simplifies to

1. (i*′*)

$f^{-1}[v]\in A$ for all $v\in V$.

A subreduction is cofinal if \operatorname{dom}(f)\mathord{\uparrow}\subseteq\operatorname{dom}(f){\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}. A subreduction of $W$ onto $V$ is is a subreduction whose image is all of $V$. A frame $W$ (cofinally) subreduces onto $V$ if there exists a (cofinal, resp.) subreduction of $W$ onto $V$.

We will often encounter conditions concerning the occurrence of certain patterns as subframes that are oblivious to the reflexivity of individual points. In order to facilitate their formulation, we define a weak subreduction of $W$ to $V$ to be a partial map $f\colon W\to V$ that satisfies (i), (ii), and the modified condition

1. (iii*′*)

$f(w)\prec v\implies\exists w^{\prime}\geq w\,f(w^{\prime})=v$

for all $w\in W$ and $v\in V$. We define other derived notions such as weak subreductions onto $V$ and cofinal weak subreductions similarly as above.

The reflexivization of a frame $\langle W,{<},A\rangle$, denoted $W_{\circ}$, is the frame $\langle W,{\leq},A\rangle$. The following is an immediate consequence of the definitions:

Observation 2.1

Let $\langle W,{<},A\rangle$ and $\langle V,{\prec},B\rangle$ be frames, and $f$ a partial map from $W$ to $V$.

• •

If $f$ is a weak subreduction of $W$ to $V$, it is a subreduction of $W_{\circ}$ to $V_{\circ}$.

• •

*If $f$ is a subreduction of $W_{\circ}$ to $V$, it is a weak subreduction of $W$ to $V$.    *∎

If $L\supseteq\mathbf{K4}$ is a logic with the finite model property, and $P$ a finite set of parameters, let $U_{L}\mathopen{(}P\mathclose{)}$ denote the universal $L$-frame for parameters $P$: it is defined as the upper part of the universal $L$-frame of rank $\lvert P\rvert$ (denoted $\mathcal{F}_{L}^{<\infty}(\lvert P\rvert)$ in [3, §8.7]), endowed with the canonical valuation of parameters from $P$ to make it a parametric frame. The double dual of $U_{L}\mathopen{(}P\mathclose{)}$ is the canonical frame $C_{L}(P,\varnothing)$ ([3, Cor. 8.89]); in particular, if $\varphi\in\operatorname{Form}(P,\varnothing)$ is unprovable in $L$, then $u\nvDash\varphi$ for some $u\in U_{L}\mathopen{(}P\mathclose{)}$.

Explicitly, we may construct $U_{\mathbf{K4}}\mathopen{(}P\mathclose{)}$ as the union $\bigcup_{n\in\omega}W_{n}$ of the following inductively defined chain of finite parametric frames:

• •

We start with $W_{0}=\varnothing$.

• •

The frame $W_{n+1}$ includes $W_{n}$ as a generated subframe. Moreover, for every $X\subseteq\mathrel{\cdot}\!W_{n}$, ${*}\in\{{\bullet},{\circ}\}$, and $\varnothing\neq E\subseteq\mathbf{2}^{P}$, where $\lvert E\rvert=1$ if ${*}={\bullet}$: if $X$ has no tight $\langle{*},E\rangle$-predecessor in $W_{n}$, we include one in $W_{n+1}$.

Then $U_{L}\mathopen{(}P\mathclose{)}\subseteq\mathrel{\cdot}\!U_{\mathbf{K4}}\mathopen{(}P\mathclose{)}$ consists of all points $u\in U_{\mathbf{K4}}\mathopen{(}P\mathclose{)}$ such that u{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} is an $L$-frame. We stress that if $X\subseteq\mathrel{\cdot}\!W_{n}$ is a rooted subframe with a reflexive root cluster $C$ such that all assignments from $E$ are realized in $C$, then no tight $\langle{*},E\rangle$-predecessor of $X$ is added to $W_{n+1}$, as it already has one (viz., a subset of $C$).

If $L$ is a clx logic, we may also describe $U_{L}\mathopen{(}P\mathclose{)}$ in our terminology as the minimal locally finite $\operatorname{bas}(L)$-extensible parametric Kripke frame for the parameters $P$.

It is well known that every point of $U_{L}\mathopen{(}P\mathclose{)}$ is definable by a formula (see e.g. [3, Thm. 8.83]). We will need an explicit description of such formulas in the simplest case $P=\varnothing$. Notice that in this case, the universal frame has no proper clusters.

For each $u\in U_{\mathbf{K4}}\mathopen{(}\varnothing\mathclose{)}$, we define a formula $\beta_{u}$ by induction on the depth of $u$ as

[TABLE]

Lemma 2.2

Let $L\supseteq\mathbf{K4}$ have fmp, $u,u^{\prime}\in U_{L}\mathopen{(}\varnothing\mathclose{)}$, and $\varphi\in\operatorname{Form}(\varnothing,\varnothing)$.

[TABLE]

Proof:   We prove (2) by induction on the depth of $u$. The right-to-left implication amounts to $u\vDash\beta_{u}$, which is straightforward to check.

Assume that $u^{\prime}\vDash\beta_{u}$. If $u$ is irreflexive, the definition of $\beta_{u}$ and the induction hypothesis imply $u^{\prime}\mathord{\uparrow}=u\mathord{\uparrow}$. Notice that there is no $v\in u\mathord{\uparrow}$ such that $v\mathord{\uparrow}=u\mathord{\uparrow}$: this would make $u\mathord{\uparrow}$ rooted with a reflexive root $v$, hence no additional tight predecessor $u$ would be added to $U_{L}\mathopen{(}\varnothing\mathclose{)}$. Thus, $u^{\prime}\notin u\mathord{\uparrow}$, hence $u^{\prime}$ is irreflexive, i.e., it is the unique irreflexive tight predecessor of $u\mathord{\uparrow}$: $u^{\prime}=u$.

If $u$ is reflexive, we have $X:=u\mathord{\uparrow}\smallsetminus\{u\}\subseteq u^{\prime}\mathord{\uparrow}$, which implies $u^{\prime}\notin X$ as above. Assuming $u^{\prime}\neq u$ for contradiction, let $w\geq u^{\prime}$ be maximal such that $w\notin u\mathord{\uparrow}$. By maximality, $w\mathord{\uparrow}\smallsetminus\{w\}\subseteq u\mathord{\uparrow}$. Since $u^{\prime}\vDash\beta_{u}$, we have $w\vDash\Diamond\bigwedge_{v\in X}\Diamond\beta_{v}$, i.e., there is $w^{\prime}>w$ such that $X\subseteq w^{\prime}\mathord{\uparrow}$. This again implies $w^{\prime}\notin X$, hence $w^{\prime}=u$ or $w^{\prime}=w$ by maximality, i.e., $w<u$ or $w$ is reflexive. If $w<u$, then $w\mathord{\uparrow}\smallsetminus\{w\}=u\mathord{\uparrow}$, i.e., $w$ is a tight predecessor of $u\mathord{\uparrow}$ other than $u$ itself, but no such tight predecessor was added into $U_{L}\mathopen{(}\varnothing\mathclose{)}$. Otherwise $w\mathord{\uparrow}\smallsetminus\{w\}=X$ and $w$ is reflexive, i.e., $w$ is a reflexive tight predecessor of $X$ other than $u$, which is again impossible.

(3): The right-to-left implication follows from $u\vDash\beta_{u}$. Left-to-right: assume that $\nvdash_{L}\beta_{u}\to\varphi$. Since $(\beta_{u}\to\varphi)\in\operatorname{Form}(\varnothing,\varnothing)$, this implies $u^{\prime}\nvDash\beta_{u}\to\varphi$ for some $u^{\prime}\in U_{L}\mathopen{(}\varnothing\mathclose{)}$ by universality. We must have $u^{\prime}=u$ by (2), thus $u\nvDash\varphi$.     ∎

2.1 Complexity classes

Since the topic of this paper is computational complexity, we will assume some degree of familiarity with basic computation models and complexity classes. We refer the reader to e.g. Arora and Barak [1] for general background on complexity theory, but for convenience, we review the definitions of classes that appear in this paper.

For any function $t\colon\omega\to\omega$, let $\mathrm{DTIME}(t)$ (or \mathrm{DTIME}\bigl{(}t(n)\bigr{)} for emphasis) denote the class of all languages $L\subseteq\Sigma^{*}$ (where $\Sigma$ is a finite alphabet) computable by a deterministic (multitape) Turing machine (DTM) in time at most $t(n)$, where $n$ is the length of input. If $F$ is a family of such functions, such as the family of all polynomially bounded functions $\operatorname{poly}(n)=n^{O(1)}$, we put $\mathrm{DTIME}(F)=\bigcup_{t\in F}\mathrm{DTIME}(t)$. The polynomial time and exponential time classes are then defined as

[TABLE]

(This is exponential time with polynomial exponent; exponential classes with linear exponent, such as \mathrm{E}=\mathrm{DTIME}\bigl{(}2^{O(n)}\bigr{)}, will not be used in this paper.) Likewise, \mathrm{DSPACE}\bigl{(}s(n)\bigr{)} is the class of languages computable by a DTM using $s(n)$ cells of memory, and

[TABLE]

For polynomial-space languages it does not matter, but recall that in general, space usage is defined so that it only accounts for the content of work tapes, excluding the input tape (which is assumed read-only), and—if we are computing a function rather than language membership—excluding the output tape (which is write-only).

In particular, our basic notion of reduction will be many-one logarithmic-space (logspace) reductions. If $X$ is a complexity class, a language $L_{0}$ is $X$-hard if every language $L\in X$ is logspace-reducible to $L_{0}$, and $L_{0}$ is $X$-complete if additionally $L_{0}\in X$.

Nondeterministic Turing machines (NTM) may have a choice between multiple possible transitions in any configuration; the machine is declared to accept a given input if there exists a run of the machine that ends in an accepting state. The class of languages accepted by a NTM in time $t(n)$ is denoted $\mathrm{NTIME}(t)$, and we put

[TABLE]

An equivalent definition of $\mathrm{NP}$ is that it consists of languages $L$ such that membership in $L$ can be witnessed by a polynomial-size certificate whose validity can be checked in $\mathrm{P}$.

We could also define nondeterministic space classes, but the only example we are interested in is $\mathrm{NPSPACE}$, which equals $\mathrm{PSPACE}$ by Savitch’s theorem.

For any class $X$ of languages $L\subseteq\Sigma^{*}$, $\mathrm{co}X$ denotes the dual class $\{\Sigma^{*}\smallsetminus L:L\in X\}$.

The deterministic and nondeterministic time classes above can be relativized: for any language $A$, a Turing machine with oracle $A$ may query membership of words in $A$ (by writing them on a dedicated oracle query tape) at unit time cost. Then for any class $X$, $\mathrm{NP}^{X}$ denotes the set of languages computable in polynomial-time by a NTM with oracle $A\in X$, and similarly for other classes. The polynomial and exponential hierarchies are defined by $\Sigma^{p}_{0}=\Delta^{p}_{0}=\Pi^{p}_{0}=\mathrm{P}$, and for $k>0$,

[TABLE]

(Notice that an $\mathrm{(N)EXP}$ machine may supply exponentially long queries to the oracle, hence the $\Sigma^{p}_{k-1}$ oracle in the definition of $\Sigma^{\exp}_{k}$ should be thought of actually having the power of $\Sigma^{\exp}_{k-1}$.) In particular, $\Sigma^{p}_{1}=\mathrm{NP}$, and $\Sigma^{\exp}_{1}=\mathrm{NEXP}$.

Many of the classes above can be equivalently defined using alternating Turing machines (ATM), which is a view we will favour especially when proving upper bounds (Sections 3–4). An ATM is similar to a NTM in that multiple possible transitions may be defined for any given state. However, the definition of acceptance is different. Each non-final state of an ATM is labelled as either existential or universal, and we define inductively the set of accepting configurations of the machine as the smallest set satisfying the following conditions:

• •

A configuration in an accepting final state111In fact, we could dispense with final states altogether: an accepting (rejecting) final state is equivalent to a universal (existential, resp.) state with no possible transitions out. is accepting.

• •

A configuration in an existential state is accepting if there exists a transition to an accepting configuration.

• •

A configuration in a universal state is accepting if all transitions lead to accepting configurations.

(States with exactly one possible transition can be thought of as deterministic; it makes no difference whether they are labelled as existential or universal.)

If $\mathrm{AP}$ denotes the class of languages computable by an ATM in polynomial time, we have

[TABLE]

(On a related note, $\mathrm{APSPACE}=\mathrm{EXP}$, but we will not need this.)

We are especially interested in classes with bounded alternation. Here, an ATM is said to make an alternation when it transitions from an existential state to a universal state, or vice versa. For any $k>0$ and $t\colon\omega\to\omega$, $\Sigma_{k}\text{-}\mathrm{TIME}(t)$ denotes the class of languages computable in time $t(n)$ by an ATM that starts in an existential state, and then makes at most $k-1$ alternations. The class $\Pi_{k}\text{-}\mathrm{TIME}(t)$ is defined similarly, but starting from a universal state. In particular, $\Sigma_{1}\text{-}\mathrm{TIME}(t)=\mathrm{NTIME}(t)$, and $\Pi_{1}\text{-}\mathrm{TIME}(t)=\mathrm{coNTIME}(t)$. We have the following characterization for any $k>0$:

[TABLE]

We will also need convenient complete languages for our classes. The set TAUT of tautologies of $\mathbf{CPC}$ is the canonical $\mathrm{coNP}$-complete language, and the dual language SAT of satisfiable classical propositional formulas is $\mathrm{NP}$-complete. The standard $\mathrm{PSPACE}$-complete language222It is more transparent to think of it as an $\mathrm{AP}$-complete language: the existential and universal quantifiers almost directly correspond to existential and universal states of an ATM. The usual textbook proof of $\mathrm{PSPACE}$-completeness of QSAT is for the most part actually a proof of the equality (4). is QSAT: the language of all true quantified Boolean sentences

[TABLE]

where $\varphi$ is a propositional formula, and each $Q_{i}\in\{\exists,\forall\}$ quantifies over a truth value $x_{i}\in\mathbf{2}$.

Let $k>0$. A quantified Boolean sentence (5) is in $\Sigma^{q}_{k}$ if the quantifier prefix $Q_{0}\dots Q_{n-1}$ may be written as at most $k$ alternating blocks, the first block consisting of existential quantifiers, the second of universal quantifiers, and so on; $\Pi^{q}_{k}$ is defined dually (i.e., starting with a universal block). Then the language $\Sigma^{q}_{k}\text{-}{\textsc{SAT}}$ consisting of all true $\Sigma^{q}_{k}$ sentences is $\Sigma^{p}_{k}$-complete, and the dual language $\Pi^{q}_{k}\text{-}{\textsc{SAT}}$ is $\Pi^{p}_{k}$-complete. Notice that $\Sigma^{q}_{1}\text{-}{\textsc{SAT}}$ is just a notational variant of SAT: a propositional formula is satisfiable iff the corresponding existentially quantified sentence is true.

Finally, we need complete languages for $\Sigma^{\exp}_{k}$ (in particular, for $k=2$). Recall that in descriptive complexity, we encode words $w=w_{0}\dots w_{n-1}\in\Sigma^{*}$ by models $M_{w}$ with domain $n=\{0,\dots,n-1\}$ endowed with the order relation $<$ (and possibly other arithmetical predicates, which we will not need here), and unary predicates $P_{a}$ for each symbol $a\in\Sigma$, such that

[TABLE]

By Fagin’s theorem, a language $L$ is in $\mathrm{NP}$ iff there is a $\Sigma^{1}_{1}$ (i.e., existential second-order) sentence $\Phi$ such that

[TABLE]

More generally, $\Sigma^{p}_{k}$ languages are exactly those that are $\Sigma^{1}_{k}$-definable. This correspondence can be generalized to the exponential hierarchy, using third-order sentences: a language is in $\Sigma^{\exp}_{k}$ iff it is $\Sigma^{2}_{k}$-definable. (See Kołodziejczyk [9, Prop. 2.6], which also includes a brief historical discussion. A similar statement in Hella and Turull-Torres [4, Thm. 7] suffers from an off-by-one error.)

Since we only need complete problems rather than exact descriptions of the languages, we may simplify the $\Sigma^{2}_{k}$ sentences to a convenient form. This was already done in [5, L. 3.1] for the special case $k=1$ (i.e., $\mathrm{NEXP}$); here we generalize it to higher levels of the exponential hierarchy (with a more detailed proof).

Theorem 2.3

Let $k\geq 1$. Put $Q=\exists$ for $k$ odd, and $Q=\forall$ for $k$ even, and let $\overline{Q}$ be its dual. Then the set of true $\Sigma^{2}_{k}$ sentences of the form

[TABLE]

is a $\Sigma^{\exp}_{k}$-complete language, where $n$ is given in unary, and $\varphi$ is a Boolean combination of atomic formulas of the form $i\in t_{\alpha}$ or $t_{\alpha}\in X_{j}$ for $\alpha<m$, $i<n$, and $j=1,\dots,k$.

Proof:   For ease of notation, we will assume that $k$ is odd, so that $Q=\exists$. The case of $k$ even is dual. We will denote third-order variables by capital letters $X,Y,\dots$ (with indices etc.), second-order variables by lower-case letters $t,s,\dots$, and first-order variables with Greek letters $\xi,\eta,\dots$.

First, any $\Sigma^{\exp}_{k}$ language reduces to a language $L\in\Sigma_{k}\text{-}\mathrm{TIME}(2^{n})$ by a simple padding argument: if $L_{0}\in\Sigma_{k}\text{-}\mathrm{TIME}(2^{n^{c}})$, then $L=\{0^{n^{c}}1w:w\in L_{0},\lvert w\rvert=n\}$ is computable in $\Sigma_{k}\text{-}\mathrm{TIME}(2^{n})$, and $w\mapsto 0^{n^{c}}1w$ is a logspace reduction of $L_{0}$ to $L$. Thus, let us fix a $\Sigma^{\exp}_{k}$-complete language $L\in\Sigma_{k}\text{-}\mathrm{TIME}(2^{n})$.

By Kołodziejczyk [9] (Thm. 5.6 and a comment below Def. 5.9), there is a $s[\Sigma^{2}_{k}]^{\leq 1}$ sentence $\Phi$ that defines $L$ as in (6): that is, $\Phi$ has the form

[TABLE]

where $\Psi$ is a second-order formula, and all the second-order and third-order variables are unary: i.e., for a model with domain $n$, the second-order variables range over $\mathcal{P}(n)$, and third-order variables over $\mathcal{P}(\mathcal{P}(n))$. (Second-order variables will remain unary for the rest of the proof, but we will introduce third-order variables of higher arity during subsequent manipulations.) We may assume $\Psi$ only uses $=$ for first-order objects.

We may write $\Psi$ in prenex normal form, and moreover, we may assume that all second-order quantifiers precede all first-order quantifiers: this is easily accomplished by exploiting the equivalences

[TABLE]

where $s\neq\varnothing$ stands for $\exists\xi\,s(\xi)$; similarly for universal quantifiers. Thus, we may write

[TABLE]

where $\psi$ is first-order. Next, we get rid of existential second-order quantifiers by introducing Skolem functions: $\Phi$ is equivalent to

[TABLE]

where each $Y_{i}$ is a third-order relation variable with $i$ second-order and one first-order argument (i.e., it ranges over $\mathcal{P}(\mathcal{P}(n)^{i}\times n)$.) Eliminating the comprehension symbols, $\Phi$ is equivalent to

[TABLE]

where $\gamma$ denotes the first-order formula

[TABLE]

By increasing $l$ or adding dummy quantifiers if necessary, we may assume that all the tuples $\vec{X}_{j}$ also have length $l$.

In order to simplify each third-order quantifier block to a single unary variable, we pass from $M_{w}$ to a larger model $M^{*}_{w}$, defined as follows. The domain of $M^{*}_{w}$ is $n^{*}=n\times(l+1)^{2}$ (i.e., $(l+1)^{2}$ disjoint copies of the domain of $M_{w}$). For each $i<(l+1)^{2}$, $M^{*}_{w}$ includes a unary predicate $C_{i}$ that selects the $i$th copy of $M_{w}$ (i.e., $C_{i}$ is satisfied by elements of $n\times\{i\}$), and a binary predicate $E$ that defines the equivalence relation

[TABLE]

(i.e., the kernel of the projection $M^{*}_{w}\to M_{w}$). The original relations of $M_{w}$ are included on the [math]th copy $n\times\{0\}$. Clearly, the mapping $w\mapsto M^{*}_{w}$ is still logspace computable. We will translate $\Phi$ to a formula $\Phi^{*}$ such that

[TABLE]

We may represent elements $\xi\in M_{w}$ by elements of $M^{*}_{w}$ that satisfy $C_{0}$, and subsets $t\subseteq M_{w}$ by subsets of $C_{0}$; however, we will actually need to quantify over the copies of $t$ in each $C_{i}$ as well. We represent an $l$-tuple $\vec{X}=\langle X_{i}:i<l\rangle$ of third-order objects $X_{i}\subseteq\mathcal{P}(n)$ by a single third-order object $X^{*}\subseteq\mathcal{P}(n^{*})$ defined as

[TABLE]

Moreover, if we are in addition to $\vec{X}$ given a tuple $Y_{1},\dots,Y_{l}$, where $Y_{i}\subseteq\mathcal{P}(n)^{i}\times n$, we represent $\vec{X},\vec{Y}$ together by

[TABLE]

With this representation in mind, $\Phi^{*}$ will have the form

[TABLE]

where each $\vec{t}_{i}$ is an $(l+1)^{2}$-tuple $\langle t_{i,j}:j<(l+1)^{2}\rangle$, the formula $\gamma^{*}$ is a conjunction of (10) and (11) below, and $\psi^{*}$ is constructed from $\psi$ as follows. We replace first-order quantifiers $\exists\xi\,\dots$ and $\forall\xi\,\dots$ by $\exists\xi\,(C_{0}(\xi)\land\dots)$ and $\forall\xi\,(C_{0}(\xi)\to\dots)$, respectively. Atomic subformulas of $\psi$ that only mention first-order objects are left intact, atomic formulas $t_{i}(\xi)$ are replaced with $t_{i,0}(\xi)$, and atomic formulas $X_{j,p}(t_{i})$ are replaced with $X_{j}^{*}(t_{i,p})$.

The first conjunct of $\gamma^{*}$,

[TABLE]

ensures that the sets $\vec{t}_{i}$ are correctly formed: i.e., $t_{i,j}\subseteq C_{j}$, and for fixed $i$, all the $t_{i,j}$ are copies of the same set $t_{i}\subseteq n$. The second conjunct is a translation of (8), which can be written as

[TABLE]

Expanding the definition of $\cup$, we arrive at

[TABLE]

By construction, (9) holds. Notice that $\gamma^{*}$, specifically (11), contains a second-order quantifier. When we bring $\Phi^{*}$ to prenex normal form, we obtain a sentence of the form (dropping the ∗ decoration from variables)

[TABLE]

where $\varphi$ is first-order. (This is still a single, constant-size sentence that only depends on $L$, not on $w$.)

As a final step, we transform $\Phi^{*}$ for any given word $w$ to a sentence $\Phi_{w}$ that embeds the structure of $M^{*}_{w}$ as follows. Using constants for elements $i\in M^{*}_{w}$ (i.e., $i<n^{*}$), we expand each first-order quantifier $\exists\xi\,\dots$ to a disjunction $\bigvee_{i<n^{*}}\dots$, and $\forall\xi\,\dots$ to $\bigwedge_{i<n^{*}}\dots$. Then we evaluate each atomic formula that does not involve higher-order variables, and replace it with $\top$ or $\bot$ according to its truth-value.

The resulting formula has size polynomial in $n$ (the exponent being roughly the nesting depth of first-order quantifiers in $\Phi^{*}$), and it is easy to see that it is logspace computable. It has the form (7), and we have

[TABLE]

by construction.     ∎

3 Derivability

Before we embark on our main quest for the complexity of admissibility and unifiability in clx logics, let us first settle a more basic question: what is the complexity of tautologicity or derivability in these logics.

Remark 3.1

Notice that (single-conclusion) derivability has the same complexity as tautologicity for any transitive logic $L$, as

[TABLE]

gives a logspace reduction.

Recall that any clx logic $L$ is $\forall\exists$-definable on finite frames [8, Thm. 4.29], and as a consequence, finite $L$-frames are recognizable in polynomial time (in fact, in $\mathrm{\Pi_{2}\text{-}TIME}(O(\log n))$, a subclass of uniform $\mathrm{AC}^{0}$).

Theorem 3.2

For any consistent linear clx logic $L$, derivability in $L$ is $\mathrm{coNP}$-complete.

Proof:   Since $L$ is a conservative extension of classical propositional logic, $\vdash_{L}$ is $\mathrm{coNP}$-hard.

On the other hand, if $\varphi$ is a formula of size $n=\lvert\varphi\rvert$ such that $\nvdash_{L}$, then there exists an $L$-model $F\nvDash\varphi$ of depth and cluster size at most $n$, hence size at most $n^{2}$, by [8, Thm. 4.38]. (In fact, it is easy to show that size $n$ is enough.) Since finite $L$-frames are polynomial-time recognizable by Remark 3.1, this shows that $\nvdash_{L}$ is in $\mathrm{NP}$.     ∎

The complexity of nonlinear clx logics is a bit more difficult to establish (although it is just a variant of standard $\mathrm{PSPACE}$-completeness results for modal logics starting with Ladner [10]). For this reason, we state the upper and lower bounds separately. We begin with the former.

Recall from [8, Def. 4.20] that $\operatorname{bas}(L)$ is a finite set of extension conditions that determines the shape of $L$-frames.

Theorem 3.3

For any clx logic $L$, $L$-derivability is in $\mathrm{PSPACE}$.

Proof:   Recall from [8, Thm. 4.38] that if $\nvdash_{L}\varphi$, then $\varphi$ is falsified in a rooted $L$-model which is a tree of depth $\leq n$ of clusters of size $\leq n$. Similarly to the standard case of $\mathbf{K4}$ and other common logics, we may search for such a tree in polynomial space—or as we prefer to think about it, in alternating polynomial time—by exploring one branch at a time.

In more detail, let $\varphi$ be a formula whose provability in $L$ we want to determine. Since variables and parameters work the same way with respect to derivability, we may assume $\varphi$ contains no parameters. Put $\Sigma=\operatorname{Sub}(\Box\varphi)$, $B=\{\psi:\Box\psi\in\Sigma\}$, $V=\Sigma\cap\mathrm{Var}$, and $n=\lvert\Sigma\rvert$. For any $v\in\mathbf{2}^{V}$ and $X\subseteq B$, let $A(v,X)$ denote the Boolean assignment to modal formulas that agrees with $v$ on variables, and that makes $\Box\psi$ true for $\psi\in X$, and false for $\psi\in B\smallsetminus X$. If $W$ is an $L$-model, let $B^{+}(W)=\{\psi\in B:W\vDash\psi\}$.

We intend to construct an algorithm to compute the predicate

[TABLE]

for $X\subseteq B$. (I.e., $S$ determines what assignments to the set $\{{\boxdot}\psi:\psi\in B\}$ are consistent with $L$; recall that $\operatorname{Mod}_{L}$ denotes the class of rooted finite $L$-models.) We may then express (un)provability of $\varphi$ as

[TABLE]

We will present a recursive description of $S(X)$ expressing how to build a model witnessing $S(X)$ by attaching a new root cluster to a disjoint sum of rooted models witnessing $S(Z)$ for some sets $Z\supsetneq X$.

To this end, we consider auxiliary predicates $H_{C}(X,Y)$ and $U_{m}(X,Y)$ for $X\subseteq Y\subseteq B$, where $\langle C,m\rangle\in\mathit{EC}^{\infty}$. Their intended meaning is that $H_{C}(X,Y)$ holds if, given a (not necessarily rooted) model $W^{\prime}$ such that $B^{+}(W^{\prime})=Y$, we can construct a model $W$ such that $B^{+}(W)=X$ by attaching to $W^{\prime}$ a root cluster of type $C$ with a suitable valuation; $U_{m}(X,Y)$ holds if there are rooted models $\{W_{i}:i<m\}$ such that B^{+}\bigl{(}\sum_{i<m}W_{i}\bigr{)}=Y and $B^{+}(W_{i})\supsetneq X$ for each $i$. We interpret this for infinite extension conditions such that if C={\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle\infty\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle\infty\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle\infty\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle\infty\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}}, the root cluster can be reflexive of arbitrary size, and if $m=\infty$, any positive number of $W_{i}$ is allowed.

Formally, we define $H_{C}$ and $U_{m}$ as follows:

[TABLE]

for $1\leq k<\omega$ and $m<\omega$.

Claim 3.3.1

For any $X\subseteq B$,

[TABLE]

Proof:   Left-to-right: Fix a finite rooted $L$-model $W$ such that $B^{+}(W)=X$, and such that B^{+}(w{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}})\supsetneq X for all $w\in W\smallsetminus\operatorname{rcl}(W)$. Assume that $W$ is of type $t$, and fix $\langle C,m\rangle\in\operatorname{bas}(L)$ such that $t\preceq\langle C,m\rangle$. Put Y=B^{+}\bigl{(}W\smallsetminus\operatorname{rcl}(W)\bigr{)}.

We claim that $H_{C}(X,Y)$: if $C={\bullet}$, let $v\in\mathbf{2}^{V}$ be the assignment of variables in the (unique) root $r$, i.e., $v=\operatorname{Sat}_{V}(r)$. Since $Y=\{\psi\in B:r\vDash\Box\psi\}$, we have $\operatorname{Sat}_{\Sigma}(r)=A(v,Y)$, and it is readily seen that

[TABLE]

thus $v$ witnesses that $H_{\bullet}(X,Y)$ holds. If $C$ is reflexive, then $X=\{\psi\in B:r\vDash\Box\psi\}$, thus for any $w\in\operatorname{rcl}(W)$, $\operatorname{Sat}_{\Sigma}(w)=A(v,X)$, where $v=\operatorname{Sat}_{V}(w)$. If C={\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle k\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle k\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle k\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle k\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}}, fix a (not necessarily injective) enumeration $\operatorname{rcl}(W)=\{w_{i}:i<k\}$; then H_{{\mathchoice{\vbox{\hbox to8.55556pt{\hss\scriptstyle k\hss}}\kern-8.55556pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to8.55556pt{\hss\scriptstyle k\hss}}\kern-8.55556pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to6.45555pt{\hss\scriptscriptstyle k\hss}}\kern-6.45555pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to5.05554pt{\hss\scriptscriptstyle k\hss}}\kern-5.05554pt\hbox{\scriptscriptstyle\bigcirc}}}}(X,Y) is witnessed by $v_{i}=\operatorname{Sat}_{V}(w_{i})$. Likewise, if C={\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle\infty\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle\infty\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle\infty\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle\infty\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}}, we may take $v=\operatorname{Sat}_{V}(w)$ for any $w\in\operatorname{rcl}(W)$ such that $w\vDash\neg\chi$.

We also claim that $U_{m}(X,Y)$. If $m<\infty$, let $\{C_{j}:j<m\}$ be a (not necessarily injective) enumeration of immediate successor clusters of $\operatorname{rcl}(W)$, and put Z_{j}=B^{+}(C_{j}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}). Then $S(Z_{j})$ by definition, and $Y=\bigcap_{j<m}Z_{j}$, which implies that $Y\subseteq Z_{j}\subseteq B$, and for each $\chi\in B\smallsetminus Y$, $\chi\notin Z_{j}$ for some $j$. Moreover, our assumptions on $W$ ensure that $X\subsetneq Z_{j}$. Thus, $\{Z_{j}:j<m\}$ witness that $U_{m}(X,Y)$ holds. If $m=\infty$, then for any $\chi\in B\smallsetminus Y$, there exists a point $x\in W\smallsetminus\operatorname{rcl}(W)$ such that $x\nvDash{\boxdot}\chi$; then Z=B^{+}(x{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}) has the required properties. If $Y=B$, we just do the same for an arbitrary $x\in W\smallsetminus\operatorname{rcl}(W)$.

Right-to-left: Fix $\langle C,m\rangle\in\operatorname{bas}(L)$ and $X\subseteq Y\subseteq B$ such that $H_{C}(X,Y)$ and $U_{m}(X,Y)$. We will construct a finite $L$-model $W$ whose root witnesses $S(X)$. First, we build the root cluster. If $C={\bullet}$, $\operatorname{rcl}(W)$ will be an irreflexive point with valuation of variables $v$ chosen as a witness for $H_{\bullet}(X,Y)$. Likewise, if C={\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle k\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle k\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle k\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle k\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}}, let $\{v_{i}:i<k\}$ be witnesses for H_{{\mathchoice{\vbox{\hbox to8.55556pt{\hss\scriptstyle k\hss}}\kern-8.55556pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to8.55556pt{\hss\scriptstyle k\hss}}\kern-8.55556pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to6.45555pt{\hss\scriptscriptstyle k\hss}}\kern-6.45555pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to5.05554pt{\hss\scriptscriptstyle k\hss}}\kern-5.05554pt\hbox{\scriptscriptstyle\bigcirc}}}}(X,Y); then $\operatorname{rcl}(W)$ is a $k$-element reflexive cluster $\{w_{i}:i<k\}$ with $\operatorname{Sat}_{V}(w_{i})=v_{i}$. If C={\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle\infty\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle\infty\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle\infty\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle\infty\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}}, then for each $\chi\in Y\smallsetminus X$, fix $v_{\chi}\in\mathbf{2}^{V}$ such that $A(v_{\chi},X)\vDash\bigwedge_{X}\psi\land\neg\chi$; then $\operatorname{rcl}(W)$ is a reflexive cluster consisting of points $\{w_{\chi}:\chi\in Y\smallsetminus X\}$ such that $\operatorname{Sat}_{V}(w_{\chi})=v_{\chi}$. This does not work if $X=Y$; in this case, we let $\operatorname{rcl}(W)$ be a reflexive singleton satisfying $v$ where $A(v,X)\vDash\bigwedge_{\psi\in X}\psi$.

Next, we construct the rest of the model. If $m<\infty$, let $\{Z_{j}:j<m\}$ be witnesses for $U_{m}(X,Y)$. Since $S(Z_{j})$ for each $j<m$, we may fix a finite rooted $L$-model $W_{j}$ such that $B^{+}(W_{j})=Z_{j}$. We let $W\smallsetminus\operatorname{rcl}(W)=\sum_{j<m}W_{j}$. Similarly, if $m=\infty$, then for each $\chi\in B\smallsetminus Y$, we fix $Z_{\chi}$ satisfying the condition from the definition of U_{{\mathchoice{\vbox{\hbox to8.55556pt{\hss\scriptstyle\infty\hss}}\kern-8.55556pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to8.55556pt{\hss\scriptstyle\infty\hss}}\kern-8.55556pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to6.45555pt{\hss\scriptscriptstyle\infty\hss}}\kern-6.45555pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to5.05554pt{\hss\scriptscriptstyle\infty\hss}}\kern-5.05554pt\hbox{\scriptscriptstyle\bigcirc}}}}, and we find a rooted $L$-model $W_{\chi}$ such that $B^{+}(W_{\chi})=Z_{\chi}$. We define $W\smallsetminus\operatorname{rcl}(W)$ as the disjoint union of $W_{\chi}$ for all $\chi\in B\smallsetminus Y$, as long as $Y\subsetneq B$. If $Y=B$, let $W\smallsetminus\operatorname{rcl}(W)$ be a rooted $L$-model satisfying $\bigwedge_{\psi\in B}{\boxdot}\psi$.

Since $Y=\bigcap_{j<m}Z_{j}$ or $Y=\bigcap_{\chi\in B\smallsetminus Y}Z_{\chi}$ (respectively), we see that

[TABLE]

and

[TABLE]

Then it is easy to check that $\operatorname{rcl}(W)$ witnesses $S(X)$.     $\Box\hbox{ (Claim 3.3.1)}$

Notice that if we expand the occurrences of $H_{C}$ and $U_{m}$ in (13) using their definitions, we obtain a recursive expression for $S(X)$ in terms of $S(Z)$ or $S(Z_{j})$, where $X\subsetneq Z,Z_{j}$. We may read it as a recipe for an algorithm computing $S(X)$ (and $\vdash_{L}\varphi$, in view of (12)) on an alternating Turing machine, where we interpret the existential and universal quantifiers (and disjunctions and conjunctions) in the expression as nondeterministic choices in existential or universal states (respectively). As just noted, the argument strictly increases on each recursive call to $S(X)$, hence the recursion depth is at most $n$. Moreover, each quantifier takes $O(n)$ bits, and the conditions in-between (e.g., the truth of some formulas from $\Sigma$ under $A(v,X)$) can be checked deterministically in polynomial time. Thus, the algorithm works in alternating polynomial time, i.e., in $\mathrm{PSPACE}$ by (4).     ∎

Remark 3.4

The bounds in Theorems 3.2 and 3.3 apply not just to derivability of single-conclusion rules as in Remark 3.1, but also to derivability of multiple-conclusion rules: its definition in terms of single-conclusion derivability

[TABLE]

shows that $\vdash_{L}^{m}$ is in $\mathrm{coNP}$ or $\mathrm{PSPACE}$ whenever $\vdash_{L}^{1}$ is. (In general, the definition gives a logspace disjunctive truth-table (dtt) reduction of $\vdash_{L}^{m}$ to $\vdash_{L}^{1}$; both $\mathrm{PSPACE}$ and $\mathrm{coNP}$ are closed under dtt-reductions.)

We now turn to the lower bound. There is more than one way to approach it. One possibility is to extend Ladner’s proof to show that all normal modal logics with the disjunction property are $\mathrm{PSPACE}$-hard. (Even though this is straightforward to carry out, and seems to be a fundamental result, the author is not aware of any published reference. The corresponding result for si logics was proved by Chagrov [2], cf. [3, Thm. 18.30].) We will use another method, namely by reduction from intuitionistic logic ($\mathbf{IPC}$) using a series of translations. This route is more useful for our purposes, because the resulting statement is relatively more general in the context of transitive modal logics (it applies to all transitive logics with the disjunction property, and it also applies to various extensions of $\mathbf{K4.2}$, which will be relevant in the sequel).

Definition 3.5

Let $\mathsf{T}$ denote the Gödel–McKinsey–Tarski translation of $\mathbf{IPC}$ (formulated using connectives $\{{\to},{\land},{\lor},{\bot}\}$) in $\mathbf{S4}$: $\mathsf{T}(\varphi)=\Box\varphi$ if $\varphi$ is an atom, $\mathsf{T}$ commutes with $\land$, $\lor$, and $\bot$, and

[TABLE]

The relativization translation $\mathsf{R}$ of $\mathbf{K4}$ in itself is defined as follows. Given a formula $\varphi$, we fix an atom $r$ (a parameter, in contexts where the distinction between variables and parameters becomes relevant) that does not occur in $\varphi$. We define an auxiliary translation $\psi^{r}$ such that it preserves atoms, commutes with Boolean connectives, and

[TABLE]

Then we define $\mathsf{R}(\varphi)$ as $r\to\varphi^{r}$.

Let $\mathsf{B}$ denote the boxdot translation of $\mathbf{S4}$ in $\mathbf{K4}$, which preserves atoms, commutes with Boolean connectives, and satisfies

[TABLE]

Notice that when expanded out, this formula contains two occurrences of $\mathsf{B}(\varphi)$, and as a consequence, the boxdot translation may exponentially enlarge formulas with deeply nested boxes. For this reason, we define the efficient boxdot translation $\mathsf{B}^{\prime}(\varphi)$ as follows. We introduce a new variable $z_{\psi}$ for each formula $\psi$ such that $\Box\psi\subseteq\varphi$. For any $\chi\subseteq\varphi$, let $\chi^{\prime}$ denote the formula resulting from $\chi$ by replacing all topmost occurrences of boxed subformulas $\Box\psi$ with the corresponding $z_{\psi}$. Then

[TABLE]

Lemma 3.6

For any formula $\varphi$, the formulas $\mathsf{B}(\varphi)$ and $\mathsf{B}^{\prime}(\varphi)$ are equiderivable. Specifically, we have

[TABLE]

where $\sigma$ is the substitution such that $\sigma(z_{\psi})=\mathsf{B}(\Box\psi)$.

Proof:

(14): We can prove

[TABLE]

for each $\chi\subseteq\varphi$ by induction on the complexity of $\chi$.

(15): Since $\mathsf{B}$ and $\sigma$ both commute with Boolean connectives, we have $\sigma(\chi^{\prime})=\mathsf{B}(\chi)$ for each $\chi\subseteq\varphi$, thus $\sigma(\mathsf{B}^{\prime}(\varphi))$ is

[TABLE]

which is equivalent to just $\mathsf{B}(\varphi)$.     ∎

Recall that for any frame $W$, $W_{\circ}$ denotes its reflexivization. Following [3], if $W$ is reflexive, let $\varrho W$ denote the skeleton of $W$, i.e., the quotient of $W$ by the cluster equivalence relation $\sim$, considered as an intuitionistic frame. The following is standard (see e.g. [3, L. 8.28]):

Lemma 3.7

For any reflexive frame $W$, and an intuitionistic formula $\varphi$, we have

[TABLE]

Lem

We leave the straightforward proof of the corresponding property of the boxdot translation to the reader:

Lemma 3.8

For any frame $W$, and a formula $\varphi$, we have

[TABLE]

Lem

The $\mathsf{R}(\varphi)$ translation is equivalent to $\varphi^{sf}$ from Chagrov and Zakharyaschev [3, Exer. 9.7].

Lemma 3.9

Let $\varphi$ be a formula, $r$ an atom, $W$ a frame, $W_{0}$ its subframe, and $\vDash$ a valuation in $W$ such that

[TABLE]

Then

[TABLE]

for all $w\in W_{0}$.

Proof:   By induction on the complexity of $\varphi$.     ∎

Corollary 3.10

A frame $W$ validates $\mathsf{R}(\varphi)$ iff $\varphi$ holds in all subframes of $W$ (and thus in all frames that $W$ subreduces onto).

Consequently, if $L$ is a subframe logic and $\vdash_{L}\varphi$, then $\vdash_{L}\mathsf{R}(\varphi)$.     ∎

Definition 3.11

A logic $L\supseteq\mathbf{K4}$ is (cofinally) subframe-universal for trees if for each finite tree $T$, considered as a reflexive frame, there exists an $L$-frame $W$ that (cofinally, resp.) weakly subreduces onto $T$.

Notice that in order to verify subframe universality for trees, it is enough to check binary trees; on the other hand, if a logic is subframe-universal for trees, it is also subframe-universal for all finite reflexive rooted frames without proper clusters. This follows from the fact that every such frame is a p-morphic image of a binary tree. The same considerations apply, mutatis mutandis, to cofinal subframe universality.

Theorem 3.12

Let a logic $L\supseteq\mathbf{K4}$ be subframe-universal for trees. Then $L$-derivability is $\mathrm{PSPACE}$-hard.

Proof:   Derivability in $\mathbf{IPC}$ is $\mathrm{PSPACE}$-complete by Statman [11], hence it suffices to provide a reduction of $\mathbf{IPC}$ to $L$. Now, the translations $\mathsf{T}$, $\mathsf{R}$, and $\mathsf{B}^{\prime}$ increase the size of the formula only linearly, and are readily seen to be logspace-computable, thus we only need to prove

[TABLE]

By Lemma 3.6, this is equivalent to

[TABLE]

For the left-to-right implication, it is well known that $\mathsf{T}$ is an interpretation of $\mathbf{IPC}$ in $\mathbf{S4}$, and $\mathsf{B}$ is an interpretation of $\mathbf{S4}$ in $\mathbf{K4}$. By Corollary 3.10, $\mathsf{R}$ is a self-interpretation of $\mathbf{S4}$.

For the right-to-left implication, assume that $\nvdash_{\mathbf{IPC}}\varphi$, whence there exists a finite tree $T$ such that $\varphi$ is not valid in $\varrho T$ (the intuitionistic version of $T$). By assumption, there exists a weak subreduction from an $L$-frame $W$ onto $T$, hence a subreduction from the reflexivization $W_{\circ}$ to $T$ by Observation 2.1. Then

[TABLE]

by Lemma 3.7, Corollary 3.10, and Lemma 3.8.     ∎

The previous theorem applies in particular to all logics with the disjunction property, as they are subframe universal for trees. We will even prove that logics with the disjunction property are cofinally subframe-universal for trees, which fact we will need later. We note that the special case for logics $L\supseteq\mathbf{S4}$ follows from [3, Prop. 15.13]; indeed, we could alternatively prove the general result by reducing it to the reflexive case, but the proof below is more elementary (it avoids the machinery of canonical formulas).

Theorem 3.13

Every logic $L\supseteq\mathbf{K4}$ satisfying the disjunction property is cofinally subframe-universal for trees. Consequently, $L$-derivability is $\mathrm{PSPACE}$-hard.

Proof:   We will show by induction on the depth of $T$ that for every finite tree $T$, there exists a descriptive $L$-frame $W$ cofinally weakly subreducing to $T$. For the base case, any nonempty $L$-frame (which exists as $L$ is consistent) weakly subreduces to the one-element tree.

For the induction step, let $r$ be the root of $T$, let $r_{i}$, $i<n$, be the immediate successors of $r$, and for each $i<n$, let $T_{i}$ be the subtree of $T$ rooted at $r_{i}$. We may assume $n\geq 2$ by duplicating $T_{0}$ if necessary. By the induction hypothesis, we may fix a descriptive $L$-frame $W_{i}$, and a cofinal weak subreduction $f_{i}$ from $W_{i}$ onto $T_{i}$ for each $i<n$. We may assume that $W_{i}$ is rooted, and its root $w_{i}$ is mapped to $r_{i}$ by $f_{i}$.

By [3, Thm. 15.1], there exists a rooted descriptive $L$-frame $\langle W,{<},A\rangle$ such that the disjoint sum $\sum_{i<n}W_{i}$ is a generated subframe of $W$. Notice that $f_{i}$ is not necessarily a weak subreduction from $W$ to $T_{i}$, as $W_{i}$ may not be an admissible subset of $W$: it is in general only an intersection of admissible subsets. Nevertheless, assume for now that $\bigcup_{i<n}f_{i}$ extends to a cofinal weak subreduction $g$ from $W$ to $\bigcup_{i<n}T_{i}\subseteq T$. We may further extend it to a subreduction $h\supseteq g$ from $W$ onto $T$ by putting

[TABLE]

(In particular, the root of $W$ is mapped to $r$.) The subreduction $h$ is not necessarily cofinal. However, if $v\in W$ sees no point of $\operatorname{dom}(h)$ (i.e., violates cofinality), then points below $v$ cannot be mapped by $h$ to anything else than $r$, as $g$ is cofinal. Thus, if we fix an arbitrary leaf node $t\in T$, the partial mapping $f\colon W\to T$ that extends $h$ by putting

[TABLE]

is still a weak subreduction from $W$ onto $T$, and it is clearly cofinal.

Now, it remains to construct $g$. Let us first fix $i<n$ and $u\in W_{i}$. Since $W$ is refined, we may find for each $j<n$, $j\neq i$, a set $X_{u,j}\in A$ such that $w_{j}\in{\boxdot}X_{u,j}$, and $u\notin X_{u,j}$. Putting $X_{u}=W\smallsetminus\bigcup_{j\neq i}X_{u,j}$, we have $u\in X_{u}\in A$, while X_{u}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}\cap\bigcup_{j\neq i}W_{j}=\varnothing. The sets $X_{u}\cap W_{i}$ are admissible in $W_{i}$; using the compactness of $W_{i}$, there exists a finite set $\{u_{k}:k<m\}\subseteq W_{i}$ such that $W_{i}$ is covered by $Y_{i}=\bigcup_{k<m}X_{u_{k}}\in A$.

Let $\vDash$ be an admissible valuation on $W$ such that

[TABLE]

for each $i<n$ and $v\in W$, and

[TABLE]

for each $i<n$, $t\in T_{i}$, and $v\in W_{i}$ (the valuation of $x_{t}$ may be arbitrary outside $W_{i}$, which allows $\vDash$ to be admissible in $W$). We define a partial function $g\colon W\to T$ such that for any $i<n$, $t\in T_{i}$, and $v\in W$,

[TABLE]

The ${\boxdot}y_{i}$ conjunct ensures that the purported preimages of distinct points are disjoint, hence $g$ is indeed a well-defined partial mapping. It is then easy to check that $g\supseteq f_{i}$ for each $i<n$, and that $g$ is a cofinal weak subreduction from $W$ onto $\bigcup_{i<n}T_{i}$.     ∎

4 Upper bounds

4.1 Nonlinear cluster-extensible logics

In order to prove our basic estimate of the complexity of admissibility in clx logics, we will use the description of admissibility in terms of pseudoextensible models from [8, Thm. 5.24], thus we need to know what it takes to check pseudoextensibility.

Lemma 4.1

Let us fix an extension condition $\langle C,m\rangle\in\mathit{EC}^{\infty}$.

Given a finite set of formulas $\Sigma$ which is closed under subformulas, and a finite model $F$, we can check if $F$ is $\langle C,m\rangle$-pseudoextensible wrt $\Sigma$ in \mathrm{coNTIME}\bigl{(}(N+2^{n^{2}})^{O(1)}\bigr{)}, where $n=\lvert\Sigma\rvert$, and $N=\lvert F\rvert$.

If moreover $C$ is finite, we can even check it in \mathrm{DTIME}\bigl{(}(N+2^{n})^{O(1)}\bigr{)}.

Proof:   First, observe that we can compute the valuation of all formulas from $\Sigma$ in $F$ in about $O(nN^{2})$ steps.

Let $P=\mathrm{Par}\cap\Sigma$, $B=\{\varphi:\Box\varphi\in\Sigma\}$, and ${*}=\operatorname{refl}(C)$. (Recall that ${*}\in\{{\bullet},{\circ}\}$ denotes the reflexivity of $C$.)

Given $X\subseteq F$, $\varnothing\neq E\subseteq\mathbf{2}^{P}$ (with $\lvert E\rvert=1$ if ${*}={\bullet}$), and $u=\{u_{e}:e\in E\}\subseteq F$, we can test in \mathrm{DTIME}\bigl{(}(N+2^{n})^{O(1)}\bigr{)} if $u$ is a tight $\langle{*},E\rangle$-pseudopredecessor of $X$ wrt $\Sigma$ just using the definition: this amounts to checking $u_{e}\vDash P^{e}$ for all $e\in E$, and for each $\varphi\in B$, to look at the valuation of $\varphi$ and $\Box\varphi$ in every $u_{e}$ and $w\in X$.

Better yet, given $E$ and $X$, we can check the existence of a $\langle{*},E\rangle$-tpp of $X$ wrt $\Sigma$ in \mathrm{DTIME}\bigl{(}(N+2^{n^{2}})^{O(1)}\bigr{)}: we compute $B^{+}=\bigcap_{w\in X}\{\varphi\in B:w\vDash{\boxdot}\varphi\}$, and $B^{-}=B\smallsetminus B^{+}$. If ${*}={\bullet}$, we try every $u\in F$ to see if

[TABLE]

If ${*}={\circ}$, we try every $D\subseteq B^{+}$ and $f\colon D\to E$ to see if any satisfy the condition

[TABLE]

(cf. [8, Def. 5.21 and L. 5.22]). This condition in turn can be checked by trying all possible $e$ and $u$. Notice that there are at most $2^{n}$ choices for $D$, and at most $\lvert E\rvert^{n}\leq 2^{n^{2}}$ choices for $f$; if $\lvert E\rvert$ is bounded by a constant, the latter bound is $2^{O(n)}$.

If $m$ is finite, then $F$ is $\langle C,m\rangle$-pseudoextensible wrt $\Sigma$ iff for all $E\subseteq\mathbf{2}^{P}$ of size $\lvert E\rvert\leq_{0}\lvert C\rvert$, and for all $X=\{w_{i}:i<m\}\subseteq F$, there exists a $\langle{*},E\rangle$-tpp of $X$ wrt $\Sigma$. We check this by co-nondeterministically choosing $E$, and then deterministically trying all $N^{m}$ possibilities for $X$, resulting in a \mathrm{coNTIME}\bigl{(}(N+2^{n^{2}})^{O(1)}\bigr{)} algorithm. If moreover $C$ is finite with $\lvert C\rvert=k$, we only need to check $E\subseteq\mathbf{2}^{P}$ of size $\lvert E\rvert\leq k$; we may do this deterministically by trying all $2^{kn}$ possibilities, resulting in a \mathrm{DTIME}\bigl{(}(N+2^{n})^{O(1)}\bigr{)} algorithm.

If $m=\infty$, we could choose $X\subseteq F$ co-nondeterministically as well. However, in order to get a deterministic algorithm for $C$ finite, we cannot afford to try all $2^{N}$ possibilities for $X$. We observe that the existence of a $\langle{*},E\rangle$-tpp of $X$ wrt $\Sigma$ does not depend on $X$ as such, but only on the set $B^{+}\subseteq B$ as defined above. Thus, instead of checking all $X\subseteq F$, we only check all (at most $2^{n}$) possibilities for $B^{+}\subseteq B$. Given $B^{+}$, we can test if there exists a corresponding $\langle{*},E\rangle$-tpp by the same method as above; moreover, we can test if there exists a set $X\subseteq F$ such that $B^{+}=\bigcap_{w\in X}\{\varphi\in B:w\vDash{\boxdot}\varphi\}$ as this is equivalent to the condition

[TABLE]

easily verifiable by going through all $\varphi$ and $w$.     ∎

Theorem 4.2

For any clx logic $L$, $L$-admissibility is computable in $\Pi^{\exp}_{2}$, and $L$-unifiability is computable in $\Sigma^{\exp}_{2}$.

If $L$ has bounded cluster size, or if the number of parameters is bounded by a constant, $L$-admissibility is computable in $\mathrm{coNEXP}$, and $L$-unifiability in $\mathrm{NEXP}$.

Proof:   Using [8, Thm. 5.24], a rule $\Gamma\mathrel{/}\Delta$ is not $L$-admissible if and only if it fails in some $L$-model $F$ of size at most $4^{n}$ that is $\operatorname{bas}(L)$-pseudoextensible wrt $\Sigma$, where $\Sigma=\operatorname{Sub}(\Gamma\cup\Delta)$, and $n=\lvert\Sigma\rvert$.

We can check this by nondeterministically choosing such a model $F$ of size $N\leq 4^{n}$ equipped with an assignment ${\vDash}\colon\Sigma\to\mathbf{2}$, and verifying it is indeed a counterexample for admissibility of $\Gamma\mathrel{/}\Delta$. Given $F$, we can check in time $N^{O(1)}=2^{O(n)}$ whether $F$ is an $L$-frame (using [8, Thm. 4.29]), whether $\vDash$ is an honest valuation respecting the connectives, and whether $\Gamma\mathrel{/}\Delta$ is satisfied in the model $\langle F,{\vDash}\rangle$. By Lemma 4.1, we can check that $F$ is $\langle C,m\rangle$-pseudoextensible wrt $\Sigma$ for each $\langle C,m\rangle\in\operatorname{bas}(L)$ by a $\mathrm{coNTIME}(2^{O(n^{2})})$ algorithm. Overall, this gives a $\Sigma^{\exp}_{2}$ algorithm for checking inadmissibility.

If $L$ has bounded cluster size, all conditions $\langle C,m\rangle\in\operatorname{bas}(L)$ have $C$ finite, thus we can check $\operatorname{bas}(L)$-pseudoextensibility of $F$ in $\mathrm{DTIME}(2^{O(n)})$, and inadmissibility in $\mathrm{NEXP}$ (in fact, in $\mathrm{NE}$). The same bound also holds for arbitrary $L$ in case the number of parameters is bounded by a constant $k$, as we may reduce the size of each $C$ to at most $2^{k}$.     ∎

4.2 Linear cluster-extensible logics

Observe that linear clx logics are cofinal-subframe logics.

Theorem 4.3

Let $L$ be a linear clx logic. Then $L$-admissibility is computable in $\mathrm{NEXP}$, and $L$-unifiability in $\mathrm{coNEXP}$.

If $L$ has bounded cluster size, or if the number of parameters is bounded by a constant, then $L$-admissibility and $L$-unifiability are in $\mathrm{PSPACE}$.

Proof:   Put $\operatorname{bas}^{i}(L)=\{\langle C,m\rangle\in\operatorname{bas}(L):m=i\}$ and $\operatorname{bas}_{i}(L)=\{C:\langle C,i\rangle\in\operatorname{bas}(L)\}$ for $i=0,1$. Let us fix a rule $\Gamma\mathrel{/}\Delta$, and put $\Sigma=\operatorname{Sub}(\Gamma\cup\Delta)$, $P=\Sigma\cap\mathrm{Par}$, $B=\{\varphi:\Box\varphi\in\Sigma\}$, and $n=\lvert\Sigma\rvert$.

If $W$ is a finite rooted $L$-model, we put $B^{+}(W)=\{\varphi\in B:W\vDash\varphi\}$, and we define predicates $G_{i}(W)$ for $i\geq\lvert B^{+}(W)\rvert$ inductively by

[TABLE]

Notice that the constraint $B^{+}(W^{\prime})\subsetneq B^{+}(W)$ ensures that the condition $i\geq\lvert B^{+}(W)\rvert$ is preserved; in particular, $G_{0}(W)$ never refers to the nonexistent $G_{-1}$, and it is well defined. Finally, we define $G(W)$ for arbitrary finite $L$-models $W$ by

[TABLE]

Claim 4.3.1

If $W_{0}$ and $W_{1}$ are rooted $L$-models of $\Gamma$ such that $B^{+}(W_{0})=B^{+}(W_{1})$, and $i\geq\lvert B^{+}(W_{0})\rvert$, then $G_{i}(W_{0})$ iff $G_{i}(W_{1})$.

Proof:   By induction on $i$. Fix $C$ and $E$ as in (16), and let $W^{\prime}_{0}$ be a witness for $G_{i}(W_{0})$, so that $U=W^{\prime}_{0}\smallsetminus W_{0}$ is a $\langle\operatorname{refl}(C),E\rangle$-tp of $W_{0}$. Put $W^{\prime}_{1}=W_{1}\cup U$ (with $U<W_{1}$ so that $W_{1}\subseteq\mathrel{\cdot}\!W^{\prime}_{1}$). Then $W^{\prime}_{1}$ is an $L$-model, and $W^{\prime}_{1}\smallsetminus W_{1}$ is a $\langle\operatorname{refl}(C),E\rangle$-tp of $W_{1}$ in $W^{\prime}_{1}$. We have $W^{\prime}_{1}\vDash\Gamma$: $\Gamma$ holds in $W_{1}\subseteq\mathrel{\cdot}\!W^{\prime}_{1}$ by assumption; it holds in $U$ since it holds in $W^{\prime}_{0}$, and satisfaction of formulas from $\Sigma$ in $U$ only depends (apart from valuation of atoms in $U$, which did not change) on $B^{+}(W_{1})$, equal to $B^{+}(W_{0})$ by assumption. For the same reason, we obtain $B^{+}(W^{\prime}_{1})=B^{+}(W^{\prime}_{0})$, therefore, in case $B^{+}(W^{\prime}_{1})\subsetneq B^{+}(W_{1})$, we have $G_{i-1}(W^{\prime}_{1})$ by the induction hypothesis.     $\Box\hbox{ (Claim 4.3.1)}$

Claim 4.3.2

$G(W)$* holds if and only if $W$ is a generated submodel of an $L$-model $F\vDash\Gamma$ such that $F$ is $\operatorname{bas}^{1}(L)$-pseudoextensible wrt $\Sigma$.*

Proof:

Left-to-right: Start with $W$, and by unwinding (17) and (16), attach all the tight predecessors that are asserted to exist. Call the resulting model $F$. It is clear that $F$ is a finite $L$-model, $W\subseteq\mathrel{\cdot}\!F$, and $F\vDash\Gamma$. In order to see that $F$ is $\operatorname{bas}^{1}(L)$-pseudoextensible wrt $\Sigma$, let $C\in\operatorname{bas}_{1}(L)$, and $E\subseteq\mathbf{2}^{P}$ with $\lvert E\rvert\leq_{0}\lvert C\rvert$. By construction, all rooted submodels $W^{\prime}\subseteq\mathrel{\cdot}\!F$ satisfy $G_{i}(W^{\prime})$ for an appropriate $i$, which guarantees the existence of a $\langle\operatorname{refl}(C),E\rangle$-tp (and a fortiori $\langle\operatorname{refl}(C),E\rangle$-tpp wrt $\Sigma$), with the following exception: no tp’s of $W^{\prime}$ were added when $W^{\prime}$ resulted by attaching the cluster $\operatorname{rcl}(W^{\prime})$ below the model $W^{\prime\prime}=W^{\prime}\smallsetminus\operatorname{rcl}(W^{\prime})$ which satisfied $G_{i}(W^{\prime\prime})$ for some $i$, and such that $B^{+}(W^{\prime})=B^{+}(W^{\prime\prime})$. But then $F$ includes a $\langle\operatorname{refl}(C),E\rangle$-tp of $W^{\prime\prime}$, and since $B^{+}(W^{\prime})=B^{+}(W^{\prime\prime})$, this is also a $\langle\operatorname{refl}(C),E\rangle$-tpp of $W^{\prime}$ wrt $\Sigma$.

Right-to-left: It suffices to show that $G_{i}(W)$ if furthermore $W$ is rooted, and $i\geq\lvert B^{+}(W)\rvert$. Let us proceed by induction on $i$ as in the definition of $G_{i}(W)$. For any $C\in\operatorname{bas}_{1}(L)$ and $E\subseteq\mathbf{2}^{P}$ such that $\lvert E\rvert\leq_{0}\lvert C\rvert$, we may fix a $\langle\operatorname{refl}(C),E\rangle$-tpp $\{u_{e}:e\in E\}\subseteq F$ of $W$ wrt $\Sigma$. We construct $W^{\prime}$ by attaching to $W$ a new cluster $\{v_{e}:e\in E\}$, reflexive or not according to $\operatorname{refl}(C)$, such that $v_{e}\vDash P^{e}$ satisfies the same variables as $u_{e}$. Clearly, $W\subseteq\mathrel{\cdot}\!W^{\prime}$, $W^{\prime}$ is an $L$-model, and $W^{\prime}\smallsetminus W$ is a $\langle\operatorname{refl}(C),E\rangle$-tp of $W$. Using the fact that $\{u_{e}:e\in E\}$ is a $\langle\operatorname{refl}(C),E\rangle$-tpp wrt $\Sigma$, we can prove $u_{e}\vDash\psi\Leftrightarrow v_{e}\vDash\psi$ for all $\psi\in\Sigma$ and $e\in E$ by induction on the complexity of $\psi$. This implies $W^{\prime}\vDash\Gamma$, and $B^{+}(W^{\prime})=B^{+}(F_{u_{e}})$ for any $e\in E$. Thus, either $B^{+}(W^{\prime})=B^{+}(W)$, or $i>0$ and $G_{i-1}(F_{u_{e}})$ by the induction hypothesis, which implies $G_{i-1}(W^{\prime})$ by Claim 4.3.1.     $\Box\hbox{ (Claim 4.3.2)}$

Claim 4.3.3

\Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta* if and only if*

[TABLE]

Proof:

Right-to-left: For each $C\in\operatorname{bas}_{0}(L)$ and $E\subseteq\mathbf{2}^{P}$ such that $\lvert E\rvert\leq_{0}\lvert C\rvert$, there exists an $L$-model $F_{C,E}\vDash\Gamma$ which is $\operatorname{bas}^{1}(L)$-pseudoextensible wrt $\Sigma$ by Claim 4.3.2. Likewise, for each $\varphi\in\Delta$, there exists a $\operatorname{bas}^{1}(L)$-pseudoextensible wrt $\Sigma$ $L$-model $F_{\varphi}\vDash\Gamma$ such that $F_{\varphi}\nvDash\varphi$. Let $F$ be the disjoint union of all the $F_{C,E}$’s and $F_{\varphi}$’s. Then $F$ is an $L$-model refuting $\Gamma\mathrel{/}\Delta$ that is $\operatorname{bas}(L)$-pseudoextensible wrt $\Sigma$, hence \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta by [8, Thm. 5.24].

Left-to-right: Using [8, Thm. 5.24] again, there exists a locally finite $\operatorname{bas}(L)$-extensible $L$-model $F$ such that $F\vDash\Gamma$, and $F\nvDash\varphi$ for each $\varphi\in\Delta$. For any $C$ and $E$ as in (18), let $W$ be a $\langle\operatorname{refl}(C),E\rangle$-tp of $\varnothing$ inside $F$; then $G(W)$ by Claim 4.3.2, as $F$ is in particular $\operatorname{bas}^{1}(L)$-pseudoextensible wrt $\Sigma$.

A similar argument shows that for any $\varphi\in\Delta$, there is a finite rooted submodel $W\subseteq\mathrel{\cdot}\!F$ such that $G(W)$, and $W\nvDash\varphi$. Let $W_{0}\subseteq W$ be a subset of size at most $n+1$ that contains a point in a final cluster of $W$, and for each $\psi\in(B\smallsetminus B^{+}(W))\cup\{\varphi\}$, a point $u_{\psi}\nvDash\psi$ such that $\psi$ holds in all clusters strictly above $\operatorname{cl}(u_{\psi})$. Then $W_{0}$ is an $L$-model, and since $W$ is a chain of clusters, it is easy to see that $W_{0}$ agrees with $W$ on the truth of all formulas from $\Sigma$; in particular, $W_{0}\vDash\Gamma$, and $W_{0},u_{\varphi}\nvDash\varphi$. Moreover, we have $G(W_{0})$ using Claim 4.3.1: for any $u\in W_{0}$, $B^{+}((W_{0})_{u})=B^{+}(W_{u})$.     $\Box\hbox{ (Claim 4.3.3)}$

We will now use Claim 4.3.3 and the definition of $G(W)$ to estimate the complexity of \mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}. Assume first that $L$ has cluster size bounded by $k$, or that the number of parameters is bounded, in which case we put $k=2^{\lvert P\rvert}$. Then all the sets $E$ referred to in (16) and (18) have size at most $k$. We may directly “execute” (18), (17), and (16) by an alternating Turing machine, with existential and universal quantifiers implemented by nondeterministic choices in existential or universal states (respectively).

Since $\lvert B^{+}(W)\rvert<n$, there are $O(n)$ alternations. For the universal quantifiers, we need $O(1)$ bits to specify $C$, $O(kn)$ bits to specify $E$, and $O(\log n)$ bits to specify $\varphi\in\Delta$. For the existential quantifiers, we need $n^{O(1)}$ bits to specify the model $W$ of size $\leq n+1$ on the second line of (18); the remaining existential quantifiers quantify over a single cluster of size $\leq k$ each, hence they can be specified with $O(kn)$ bits. The other conditions in the definition (e.g., truth of $\Gamma$) may be tested deterministically in polynomial time from the data. Thus, we obtain an alternating polynomial-time algorithm for checking \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta, showing that it is in $\mathrm{AP}=\mathrm{PSPACE}$.

In the general case where both the cluster size and the number of parameters are unbounded, we need $O(2^{n})$ bits to specify the universally quantified $E$ and the existentially quantified $W^{\prime}$. The former is expected as we are shooting for $\mathrm{coNEXP}$, but the latter is a problem. Similarly to the proof of Lemma 4.1, we solve it by existentially quantifying only over the sets $B^{+}(W^{\prime})\subseteq B$ instead of $W^{\prime}$ proper, which makes sense because of Claim 4.3.1.

In more detail, let $G^{\prime}_{i}(B^{+})$ (with $B^{+}\subseteq B$ and $i\geq\lvert B^{+}\rvert$) stand for $G_{i}(W)$ with input $B^{+}(W)$ in place of $W$. Put $V=\Sigma\cap\mathrm{Var}$. For any $v\in\mathbf{2}^{V}$, $e\in\mathbf{2}^{P}$, and $B^{+}\subseteq B$, let $A(v,e,B^{+})$ denote the Boolean assignment that agrees with $v$ and $e$ on variables and parameters (respectively), and that makes $\Box\varphi$ true for $\varphi\in B^{+}$, and false for $\varphi\in B\smallsetminus B^{+}$. Then we can express $G^{\prime}_{i}(B^{+})$ as the conjunction of

[TABLE]

if {\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle\infty\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle\infty\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle\infty\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle\infty\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}}\in\operatorname{bas}_{1}(L), a similar conjunct restricted to $\lvert E\rvert\leq k$ if {\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle k\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle k\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle k\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle k\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}}\in\operatorname{bas}_{1}(L), and the conjunct

[TABLE]

if ${\bullet}\in\operatorname{bas}_{1}(L)$. We may rewrite the first conjunct in (18) analogously.

In this way, we get an alternating algorithm for \mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L} using time $2^{n^{O(1)}}$, out of which time $t_{\exists}(n)=n^{O(1)}$ is spent in existential states. We can simulate the existential states by deterministically trying all possible choices; this will multiply the overall running time by a factor of $2^{t_{\exists}(n)}$, which is still $2^{n^{O(1)}}$, hence we obtain a $\mathrm{coNEXP}$ algorithm.     ∎

Remark 4.4

Admissibility in linear clx logics with no parameters at all is even easier than $\mathrm{PSPACE}$, viz. $\mathrm{coNP}$, by [5, Thm. 2.6].

4.3 Logics of bounded depth

Our basic goal is to completely determine the complexity of admissibility and unification for clx logics. As we will see later, the only cases remaining where we can improve upon the upper bounds proved so far is for clx logics of branching [math] (i.e., depth $1$) when, moreover, the cluster size or the number of parameters is bounded. This is a tiny class of problems, most of which are not really interesting. For this reason, we broaden the scope of this section beyond clx logics, and we will look at larger classes of logics of bounded depth. We are primarily interested in cases where we can get the complexity inside the polynomial hierarchy, but we will also include for completeness some results of higher complexity, analogous to clx logics.

The added generality comes at a cost: the analysis of admissible rules from [8] does not apply to non-clx logics, hence we need to come up with a relevant theory of admissible rules for logics of bounded depth. Fortunately, this is fairly easy to do. The key factor is that logics of bounded depth are locally tabular:

Theorem 4.5** **([3, Thm. 12.21])

Every logic $L$ of finite depth is locally tabular, i.e., there are only finitely many nonequivalent formulas over any finite set of atoms, or equivalently, the canonical frames $C_{L}(P,V)$ are finite for any finite $P\subseteq\mathrm{Par}$ and $V\subseteq\mathrm{Var}$ (and more generally, all finitely generated refined $L$-frames are finite).

Consequently, all logics $L$ of finite depth, as well as atomic multi-conclusion consequence relations that extend them (such as \mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{$\scriptstyle\sim\mathstrut$}}}}_{L}), have the finite model property.     ∎

The finite model property with respect to admissibility avoids most of the trouble we had to go through in [8].

Let us start with a simple result on unifiability in all logics of bounded depth as a teaser.

Theorem 4.6

If $L$ is a logic of bounded depth, then $L$-unifiability with a constant number of parameters is in $\mathrm{NP}$.

In particular, this holds if $L$ is a clx logic of branching [math].

Proof:   A formula $\varphi$ with parameters from a fixed finite set $P$ is $L$-unifiable iff it has a variable-free unifier iff there is a (definable) valuation in the canonical frame $C_{L}(P,\varnothing)$ that makes $\varphi$ true in all points of the model. By Theorem 4.5, $C_{L}(P,\varnothing)$ is a fixed finite frame, which makes the condition above checkable in $\mathrm{NP}$.     ∎

Subsequent complexity results will only apply under further restrictions, not to all logics of bounded depth. When the number of parameters is unlimited, we will see in the next section that $L$-unifiability is $\mathrm{NEXP}$-hard or $\mathrm{coNEXP}$-hard whenever $L$ has width $\geq 2$ or unbounded cluster size (Theorems 5.3 and 5.6). Thus, we may hope to get better complexity only for linear logics of bounded cluster size, which in view of bounded depth means that $L$ is tabular.

Contrary to Theorem 4.6, we need some restrictions even if the number of parameters is finite when we discuss admissibility rather than unifiability: we know from [5] that logics such as $\mathbf{S4BD_{3}}$ have a $\mathrm{coNEXP}$-hard admissibility problem already with no parameters at all. Even if we just wanted results analogous to the previous sections, placing admissibility on a low level of the exponential hierarchy, this does not seem possible for general logics of bounded depth: cf. the construction of logics of depth $d$ in [3, §18.4] such that some nonderivable formulas require countermodels whose size is a tower of exponentials of height $d-2$. With these examples in mind, it seems we can only expect reasonably general results if we restrict attention to logics of bounded width (which is equivalent to bounded branching for logics of bounded depth).

But first, we need a rudimentary theory of admissibility in logics of bounded depth.

Definition 4.7

Let $L$ be a logic of bounded depth, and assume that $\mathrm{Par}$ is finite. A finite parametric $L$-frame $F$ has a loosely separated root if it is rooted, and points of $\operatorname{rcl}(F)$ have pairwise distinct valuations of parameters. The frame $F$ has a separated root if, moreover, it is not the case that $F\smallsetminus\operatorname{rcl}(F)$ is a rooted frame with reflexive root cluster $C$, and for each $w\in\operatorname{rcl}(F)$ there is $x\in C$ such that $w\equiv_{\mathrm{Par}}x$.

A finite parametric $L$-frame $W$ is $L$-extensible (or strongly $L$-extensible) if for every parametric $L$-frame $F$ with a separated root (a loosely separated root, resp.) such that $F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!W$, $\mathrm{id}_{F\smallsetminus\operatorname{rcl}(F)}$ extends to an isomorphism of $F$ onto a generated subframe of $W$.

While the concept of strong $L$-extensibility looks simpler, and it is easier to work with, $L$-extensibility is a structurally more fundamental property due to the following characterization: $L$-extensible frames are exactly the finitely generated injective $L$-frames, or duals of finitely generated projective $L$-algebras.

Lemma 4.8

Let $L$ be a logic of bounded depth, and assume that $\mathrm{Par}$ is finite. The following are equivalent for any finite parametric $L$-frame $W$.

1. (i)

$W$* is $L$-extensible.* 2. (ii)

For every pair of finite parametric $L$-frames $F_{0}\subseteq\mathrel{\cdot}\!F$, and a p-morphism $f_{0}\colon F_{0}\to W$, there exists a p-morphism $f\colon F\to W$ such that $f\supseteq f_{0}$.

Proof:

(i)${}\to{}$(ii): We may extend the p-morphism to one cluster after another in a top-down fashion, hence we may assume that $F$ is rooted, and $F_{0}=F\smallsetminus\operatorname{rcl}(F)$. Let $F^{\prime}$ be $f_{0}[F_{0}]\subseteq\mathrel{\cdot}\!W$ extended with a copy of $\operatorname{rcl}(F)$ as a new root cluster: then $f_{0}$ extends to a p-morphism of $F$ onto $F^{\prime}$, hence replacing $F$ with $F^{\prime}$, we may assume without loss of generality that $F_{0}\subseteq\mathrel{\cdot}\!W$, and $f_{0}=\mathrm{id}_{F_{0}}$. We may shrink the root cluster of $F$ by a p-morphism identifying all points that satisfy the same parameters, hence we may assume that points of $\operatorname{rcl}(F)$ have pairwise distinct valuations of parameters. If $F_{0}$ has a reflexive root cluster, and for each $w\in\operatorname{rcl}(F)$ there exists $x_{w}\in\operatorname{rcl}(F_{0})$ such that $w\equiv_{\mathrm{Par}}x_{w}$, then $\mathrm{id}_{F_{0}}$ extended with the mapping $w\mapsto x_{w}$ is a p-morphism $F\to F_{0}$. Otherwise $F$ has a separated root, hence $f_{0}=\mathrm{id}_{F_{0}}$ extends to a p-morphism $F\to W$ using (i).

(ii)${}\to{}$(i): Assume that $F$ has a separated root, and $F_{0}=F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!W$. Using (ii), $\mathrm{id}_{F_{0}}$ extends to a p-morphism $f\colon F\to W$. Since $F$ has a separated root, $f$ cannot identify distinct points of $\operatorname{rcl}(F)$, and it cannot map any point of $\operatorname{rcl}(F)$ to $F_{0}$, thus it is an isomorphic embedding in $W$.     ∎

Lemma 4.9

Let $L$ be a logic of bounded depth, and assume that $\mathrm{Par}$ is finite.

1. (i)

For any finite $V\subseteq\mathrm{Var}$, the canonical parametric frame $C_{L}(\mathrm{Par},V)$ is $L$-extensible. 2. (ii)

If $W$ is an $L$-extensible finite parametric $L$-frame, there exists a finite $V\subseteq\mathrm{Var}$ such that $W$ is a p-morphic image of $C_{L}(\mathrm{Par},V)$.

Proof:

(i): The frame $C_{L}(\mathrm{Par},V)$ is finite by Theorem 4.5. If $F$ is a finite $L$-frame with a separated root such that $F_{0}=F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!C_{L}(\mathrm{Par},V)$, let $\vDash$ be a valuation in $F$ that agrees in $F_{0}$ with the canonical valuation of $C_{L}(\mathrm{Par},V)$, and is arbitrary in $\operatorname{rcl}(F)$. Define a mapping $f\colon F\to C_{L}(\mathrm{Par},V)$ by $f(x)=\operatorname{Sat}_{\operatorname{Form}(\mathrm{Par},V)}(F,x)$. Then $f$ is a p-morphism of $F$ to $C_{L}(\mathrm{Par},V)$ extending $\mathrm{id}_{F_{0}}$. As in Lemma 4.8, $f$ is an isomorphic embedding because $F$ has separated root.

(ii): By [8, Lem. 2.3], $W$ is isomorphic to a generated subframe $W^{\prime}\subseteq\mathrel{\cdot}\!C_{L}(\mathrm{Par},V)$ for sufficiently large finite $V\subseteq\mathrm{Var}$. The isomorphism $W^{\prime}\to W$ extends to a p-morphism $C_{L}(\mathrm{Par},V)\to W$ by Lemma 4.8.     ∎

Remark 4.10

In fact, $L$-extensible frames are exactly the retracts of the finitely generated canonical frames $C_{L}(\mathrm{Par},V)$.

It is not generally true that p-morphic images of $C_{L}(\mathrm{Par},V)$ are $L$-extensible. For example, let $F_{0}$ be the disjoint union of the two-element cluster and the two-element reflexive chain, and let $L$ be the logic of $F_{0}$. If $V\neq\varnothing$, then one of the connected components of $C_{L}(\mathrm{Par},V)$ is a two-element cluster where both elements satisfy the same parameters. We may contract this cluster to a single point by a p-morphism, but then the resulting frame is not $L$-extensible (if $\mathrm{Par}\neq\varnothing$). For much the same reason, there exist inadmissible rules \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta with $\Gamma\cup\Delta\subseteq\operatorname{Form}(\mathrm{Par},V)$ such that there is no projective formula $\theta\in\operatorname{Form}(\mathrm{Par},V)$ such that $\theta\vdash_{L}\bigwedge\Gamma$, and $\theta\nvdash_{L}\varphi$ for each $\varphi\in\Delta$. An explicit example is the rule $p\lor\Diamond x\to\Box x\mathrel{/}x$ for $\mathrm{Par}=\{p\}$ and $V=\{x\}$.

It is easy to show (e.g. using the frame rules from [6]) that p-morphic images of finitely generated canonical frames are exactly the finite $L$-frames that validate all $L$-admissible rules.

The canonical frames $C_{L}(\mathrm{Par},V)$ are in general not strongly $L$-extensible. For example, let $L=\mathbf{S4.3}\oplus\mathbf{BD_{2}}$. Then $C_{L}(\mathrm{Par},V)$ contains a cluster $C$ such that every possible valuation of $\mathrm{Par}\cup V$ is realized by a point of $C$. There cannot be any cluster below $C$, as any such could be p-morphically contracted into $C$ while preserving the canonical valuation. Thus, $C_{L}(\mathrm{Par},V)$ is not strongly $L$-extensible.

Lemma 4.11

Let $L$ be a logic of bounded depth, and assume that $\mathrm{Par}$ is finite. Then any finite parametric $L$-frame is a generated subframe of a strongly $L$-extensible finite parametric $L$-frame.

Proof:   Let $W_{0}$ be the given frame, and $d$ be the depth of $L$. We define a sequence of parametric $L$-frames $W_{0}\subseteq\mathrel{\cdot}\!W_{1}\subseteq\mathrel{\cdot}\!\dots\subseteq\mathrel{\cdot}\!W_{d}$ by induction as follows: for every parametric $L$-frame $F$ with a loosely separated root such that $F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!W_{i}$, but $\mathrm{id}_{F\smallsetminus\operatorname{rcl}(F)}$ does not extend to an isomorphism of $F$ to a generated subframe of $W_{i}$, we add a copy of $\operatorname{rcl}(F)$ to $W_{i+1}$. (We do not distinguish among isomorphic frames $F$: they all get a single common copy of $\operatorname{rcl}(F)$.)

Since all the clusters being added have size at most $2^{\lvert\mathrm{Par}\rvert}$, there are only finitely many choices for $F$ up to isomorphism, hence all the frames $W_{i}$ are finite. Moreover, we see by induction on $i$ that all frames $F$ as above with $F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!W_{i}$ such that the depth of $F$ is less than $i$ already have a copy in $W_{i}$, i.e., only clusters of depth $\geq i+1$ are added to $W_{i+1}$. It follows that $W_{d}$ is strongly $L$-extensible.     ∎

Each of the classes of finitely generated canonical frames, p-morphic images of canonical frames, $L$-extensible frames, or strongly $L$-extensible frames, provides an adequate semantics for admissible rules. We will mostly work with strongly $L$-extensible frames, as the other possibilities are not suitable for our purposes for various reasons: canonical frames are astronomically large, and are not flexible enough so that they could be constructed from small pieces as needed; p-morphic images of canonical frames are difficult to algorithmically recognize. There is not much difference between $L$-extensible and strongly $L$-extensible frames, however strongly $L$-extensible frames have a somewhat simpler definition, and are easier to manipulate.

Theorem 4.12

Let $L$ be a logic of bounded depth, and assume that $\mathrm{Par}$ is finite. The following are equivalent for any rule $\Gamma\mathrel{/}\Delta$:

1. (i)

\Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{$\scriptstyle\sim\mathstrut$}}}}_{L}\Delta. 2. (ii)

$\Gamma\mathrel{/}\Delta$* holds in all $L$-extensible finite parametric $L$-frames.* 3. (iii)

$\Gamma\mathrel{/}\Delta$* holds in all strongly $L$-extensible finite parametric $L$-frames.*

Proof:

(i)${}\leftrightarrow{}$(ii): By [8, Lem. 2.2], $\Gamma\mathrel{/}\Delta$ is $L$-admissible iff it holds in $C_{L}(\mathrm{Par},V)$ for all finite sets of variables $V$. Thus, on the one hand, if \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{$\scriptstyle\sim\mathstrut$}}}}_{L}\Delta, then $\Gamma\mathrel{/}\Delta$ holds in all $L$-extensible frames by Lemma 4.9, as the validity of rules is preserved by p-morphic images. On the other hand, if $\Gamma\mathrel{/}\Delta$ holds in $L$-extensible frames, it holds in particular in every $C_{L}(\mathrm{Par},V)$ by Lemma 4.9, hence \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{$\scriptstyle\sim\mathstrut$}}}}_{L}\Delta.

(ii)${}\to{}$(iii) is trivial. (iii)${}\to{}$(ii): Assume that $\Gamma\mathrel{/}\Delta$ holds in all strongly $L$-extensible frames, and let $W$ be an $L$-extensible frame. By Lemma 4.11, there exists a strongly $L$-extensible frame $W^{\prime}$ such that $W\subseteq\mathrel{\cdot}\!W^{\prime}$. By Lemma 4.8, there exists a p-morphism $f\colon W^{\prime}\to W$ extending $\mathrm{id}_{W}$. Thus, $W^{\prime}\vDash\Gamma\mathrel{/}\Delta$ implies $W\vDash\Gamma\mathrel{/}\Delta$.     ∎

Remark 4.13

We can, and will, apply the characterization from Theorem 4.12 even if $\mathrm{Par}$ is infinite, by considering frames with valuation of a finite set of parameters $P\subseteq\mathrm{Par}$, which will be formally accomplished by shrinking $\mathrm{Par}$ to a finite subset for the duration of an argument. We formulated the criteria the way we did for notational convenience.

Lemma 4.14

Any logic $L$ of finite depth $d$ is axiomatizable over $\mathbf{K4BD}_{d}$ by a set of frame formulas $\{\alpha^{\sharp}(F_{i},\bot):i\in I\}$.

Proof:   Let $\{F_{i}:i\in I\}$ be an enumeration of finite rooted frames of depth $d$ such that $F_{i}\nvDash L$, and put $L^{\prime}=\mathbf{K4BD}_{d}\oplus\{\alpha^{\sharp}(F_{i},\bot):i\in I\}$. On the one hand, $F_{i}\nvDash L$ implies $\vdash_{L}\alpha^{\sharp}(F_{i},\bot)$, hence $L^{\prime}\subseteq L$. Assume for contradiction that $\vdash_{L}\varphi$, but $\nvdash_{L^{\prime}}\varphi$. Being a logic of bounded depth, $L^{\prime}$ has the finite model property, hence there exists a finite rooted $L^{\prime}$-frame $F\nvDash\varphi$ of depth $d$. Since $\vdash_{L}\varphi$, $F$ is not an $L$-frame. But then $\alpha^{\sharp}(F,\bot)$ is an axiom of $L^{\prime}$, which implies that $F$ is not an $L^{\prime}$-frame after all, a contradiction.     ∎

We now focus on logics of bounded depth and width. All such logics are finitely axiomatizable (see [7, Thm. 5.16]), and therefore their finite frames are $\mathrm{coNP}$-recognizable. In fact, we can improve this to $\mathrm{P}$:

Lemma 4.15

Let $L$ be a logic of bounded depth and width. Then finite $L$-frames are recognizable in polynomial time.

Proof:   By [7, Thm. 5.16] and Lemma 4.14, $L$ is axiomatizable by $\mathbf{K4BD}_{k}\mathbf{BW}_{k}$ for some constant $k$, plus finitely many frame formulas $\alpha^{\sharp}(F_{i},\bot)$. We can compute the depth and width of a finite frame in polynomial time. Moreover, given a rooted frame $W$ of width and depth at most $k$, we can recognize in polynomial time if $W$ reduces to $F_{i}$: if $F_{i}$ has no proper clusters, then for any p-morphism $f\colon W\twoheadrightarrow F_{i}$, preimages of all points are unions of clusters of $W$. Thus, there are only $O(1)$ choices for $f$, which are easy to check. In the general case, let $F^{\prime}_{i}$ be $F_{i}$ with all clusters reduced to size $1$. Then a p-morphism $W\to F_{i}$ induces a p-morphism $W\to F^{\prime}_{i}$; conversely, a p-morphism $W\to F^{\prime}_{i}$ is induced by a p-morphism $W\to F_{i}$ if and only if the maximal clusters in the preimage of each point of $F^{\prime}_{i}$ have size at least the size of the corresponding cluster of $F_{i}$. This is again easy to check in polynomial time.     ∎

Corollary 4.16

For any logic $L$ of bounded depth and width, there exists a constant $c$ with the following property: whenever $W$ is a Kripke $L$-frame, and $C$ is a cluster of $W$ of size $\lvert C\rvert\geq c$, then the frames obtained from $W$ by enlarging $C$ to arbitrary cardinality are also $L$-frames.

Proof:   Let $c$ be the maximum of cluster sizes of the frames $F_{i}$ in the proof of Lemma 4.15.     ∎

Incidentally, since logics of bounded depth and width have the polynomial-size model property (see e.g. [7, L. 5.13]), Lemma 4.15 implies that all such logics are in $\mathrm{coNP}$. (This will also follow from Theorem 4.19.)

Corollary 4.17

If $L$ is a logic of bounded depth and width, then $L$-derivability is in $\mathrm{coNP}$.     ∎

Lemma 4.18

Let $L$ be a logic of bounded depth and width, and assume that $\mathrm{Par}$ is finite. There is a polynomial $p(x)$ such that whenever $\Gamma\mathrel{/}\Delta$ is a rule of length $n$, and \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta, then $\Gamma\mathrel{/}\Delta$ is falsified in a strongly $L$-extensible parametric $L$-frame of size at most $p(n)$.

Proof:   Put $\Sigma=\operatorname{Sub}(\Gamma\cup\Delta)$, $B=\{\varphi:\Box\varphi\in\Sigma\}$, and $n=\lvert\Sigma\rvert$. Let $\vDash$ be a valuation falsifying $\Gamma\mathrel{/}\Delta$ in a strongly $L$-extensible parametric finite $L$-frame $W$, using Theorem 4.12. For each $\varphi\in\Delta$, fix $x_{\varphi}\in W$ such that $x_{\varphi}\nvDash\varphi$, and put W_{0}=\bigcup_{\varphi\in\Delta}x_{\varphi}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}.

Starting with $W_{0}$, we define a sequence $W_{0}\subseteq W_{1}\subseteq\cdots\subseteq W_{d}$ of generated subframes of $W$ as follows: $W_{i+1}\supseteq W_{i}$, and whenever $F\subseteq\mathrel{\cdot}\!W$ has a loosely separated root, $F\smallsetminus\operatorname{rcl}(F)\subseteq W_{i}$, but $\mathrm{id}_{F\smallsetminus\operatorname{rcl}(F)}$ does not extend to a p-morphic embedding $F\to W_{i}$, we add a copy of $\operatorname{rcl}(F)$ to $W_{i+1}$ using strong $L$-extensibility of $W$. As in Lemma 4.11, we do not distinguish among isomorphic $F$.

By the same argument as in Lemma 4.11, the frame $W_{d}$ is strongly $L$-extensible. Let $s_{i}$ be the number of clusters in $W_{i}$. Since $L$ has bounded depth and width, any rooted $L$-frame has only $O(1)$ clusters, thus $s_{0}=O(\lvert\Delta\rvert)=O(n)$. When constructing $W_{i+1}$ from $W_{i}$, each $F\smallsetminus\operatorname{rcl}(F)$ is generated by an antichain in $W_{i}$; since $L$ has bounded width $w$, there are at most $s_{i}^{w+1}$ choices for $F\smallsetminus\operatorname{rcl}(F)$. For each of them, there are at most $2^{2^{\lvert\mathrm{Par}\rvert}}+2^{\lvert\mathrm{Par}\rvert}=O(1)$ choices for $\operatorname{rcl}(F)$ up to isomorphism. Thus, $s_{i+1}=s_{i}^{O(1)}$. Since a constant number of iterations of a polynomial is still polynomial, $s_{d}=n^{O(1)}$.

We construct a submodel $W^{\prime}\subseteq W_{d}$ as follows:

• •

The points $x_{\varphi}$, $\varphi\in\Delta$, are included in $W^{\prime}$.

• •

For each cluster $C$ of $W_{d}$, and each assignment $e\in\mathbf{2}^{\mathrm{Par}}$ that is realized in $C$, we include in $W^{\prime}$ at least one point from $C$ satisfying $e$.

• •

For each cluster $C$ of $W_{d}$, and each formula $\varphi\in B$ that is falsified in some point of $C$, we include at least one such point in $W^{\prime}$.

• •

All clusters of $W_{d}$ of size $\leq c$ are fully included in $W^{\prime}$, where $c$ is the constant from Corollary 4.16.

• •

For each cluster $C$ of $W_{d}$ of size $\geq c$, we make sure $W^{\prime}$ includes at least $c$ points of $C$.

We may choose $W^{\prime}$ satisfying these requirements so that it has cluster size at most $\lvert B\rvert+2^{\lvert\mathrm{Par}\rvert}+\lvert\Delta\rvert+c=O(n)$, thus the overall size of $W^{\prime}$ is polynomial in $n$. Notice that $W^{\prime}$ has the same skeleton as $W_{d}$: we merely shrunk large clusters to control their size.

The choice of $W^{\prime}$ ensures that it is an $L$-model, and that it agrees with $W$ on the satisfaction of formulas from $\Sigma$; in particular, $\Gamma\mathrel{/}\Delta$ fails in $W^{\prime}$. We claim that $W^{\prime}$ is strongly $L$-extensible. Let $F^{\prime}$ be a parametric $L$-frame with a loosely separated root such that $F^{\prime}\smallsetminus\operatorname{rcl}(F^{\prime})\subseteq\mathrel{\cdot}\!W^{\prime}$. Let $F$ denote (F^{\prime}\smallsetminus\operatorname{rcl}(F^{\prime})){\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\subseteq\mathrel{\cdot}\!W_{d} with $\operatorname{rcl}(F^{\prime})$ attached below (i.e., we expand the clusters of $W^{\prime}$ included in $F^{\prime}\smallsetminus\operatorname{rcl}(F^{\prime})$ back to what they were in $W_{d}$). By Corollary 4.16 and the choice of $W^{\prime}$, $F$ is still an $L$-frame with a loosely separated root. Since $W_{d}$ is strongly $L$-extensible, $\mathrm{id}_{F\smallsetminus\operatorname{rcl}(F)}$ extends to a p-morphic embedding $f\colon F\to W_{d}$. Since all points of $\operatorname{rcl}(F)=\operatorname{rcl}(F^{\prime})$ are distinguished by valuation of parameters, all of $\operatorname{rcl}(F)$ is included in $W^{\prime}$, thus $f\colon F^{\prime}\to W^{\prime}$.     ∎

Theorem 4.19

Let $L$ be a logic of bounded depth and width. Then $L$-admissibility with a constant number of parameters is in $\mathrm{coNP}$.

In particular, this holds if $L$ is a clx logic of branching [math].

Proof:   By Lemma 4.18, we have \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta iff $\Gamma\mathrel{/}\Delta$ is falsified in a strongly $L$-extensible $L$-model $W$ of polynomial size. Clearly, we can check in polynomial time that $W\nvDash\Gamma\mathrel{/}\Delta$, and by Lemma 4.15, we can check that $W$ is an $L$-model.

We can also check in polynomial time that $W$ is strongly $L$-extensible: by the same argument as in the proof of Lemma 4.18, there are only polynomially many choices for a parametric $L$-frame $F$ with a loosely separated root such that $F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!W$. We can generate each such frame in polynomial time, check that it is indeed an $L$-frame with a loosely separated root, and check if we can find a suitable copy of $\operatorname{rcl}(F)$ inside $W$.     ∎

The situation for admissibility with unrestricted number of parameters is more complicated. As we already mentioned, cluster size and linearity will come into play. Notice that logics of bounded depth, width, and cluster size are tabular.

Theorem 4.20

Let $L$ be a tabular logic. Then $L$-admissibility is decidable in $\mathrm{coNEXP}$, and $L$-unifiability in $\mathrm{NEXP}$.

Proof:   Let us fix a rule $\Gamma\mathrel{/}\Delta$, and put $\Sigma=\operatorname{Sub}(\Gamma\cup\Delta)$ and $n=\lvert\Sigma\rvert$. In order to apply the criterion from Theorem 4.12, we will proceed as if $\mathrm{Par}$ were finite, consisting of only the parameters from $\Sigma$ (cf. Remark 4.13). However, we bear in mind that $\lvert\mathrm{Par}\rvert$ is bounded by $n$, not by a constant, for complexity estimates.

We claim that if \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta, there exists a strongly $L$-extensible $L$-model $W$ falsifying $\Gamma\mathrel{/}\Delta$ of size $2^{O(n)}$. This can be shown by constructing a sequence of models $W_{0}\subseteq\mathrel{\cdot}\!W_{1}\subseteq\mathrel{\cdot}\!\dots\subseteq\mathrel{\cdot}\!W_{d}$ as in the proof of Lemma 4.18. Since $L$ has bounded cluster size, there are only $2^{O(n)}$ possible root clusters in frames with loosely separated roots; with this in mind, it is easy to compute that each $W_{i}$ has size $2^{O(n)}$. (We do not need to select $W^{\prime}\subseteq W_{d}$, as $W_{d}$ already has bounded cluster size.)

Given a model $W$ of size $2^{O(n)}$, it is easy to check in deterministic exponential time that $W$ is an $L$-frame, and that $W\nvDash\Gamma\mathrel{/}\Delta$. We may also check in exponential time if $W$ is strongly $L$-extensible: by the same counting argument as above, there are $2^{O(n)}$ possible frames $F$ that we need to test, and we can generate and check them in exponential time.     ∎

Theorem 4.21

Let $L$ be a linear logic of depth $d$. Then $L$-admissibility is decidable in $\mathrm{NEXP}$, and $L$-unifiability in $\mathrm{coNEXP}$.

If $L$ has bounded cluster size (i.e., it is tabular), then $L$-admissibility is in $\Sigma^{p}_{2d}$, and $L$-unifiability in $\Pi^{p}_{2d}$.

Proof:   We use a variant of the algorithm presented in Theorem 4.3. We fix $\Gamma\mathrel{/}\Delta$, and put $\Sigma=\operatorname{Sub}(\Gamma\cup\Delta)$, $B=\{\varphi:\Box\varphi\in\Sigma\}$, and $n=\lvert\Sigma\rvert$. We will again proceed as if $\mathrm{Par}$ were finite of size $\leq n$.

Given a finite parametric $L$-frame $F$, let $\operatorname{Ext}_{L}(F)$ denote the set of single-cluster parametric frames $C$ such that $F^{C}$ is an $L$-frame with a loosely separated root, where $F^{C}$ denotes $F$ with $C$ added as a new root cluster. Using Lemma 4.15, it is polynomial-time decidable if $C\in\operatorname{Ext}_{L}(F)$. If $W$ is an $L$-model, let $\mathrm{Fr}(W)$ denote its underlying parametric frame. By abuse of notation, we will write $\operatorname{Ext}_{L}(W)$ instead of $\operatorname{Ext}_{L}(\mathrm{Fr}(W))$.

Similarly to the proof of Theorem 4.3, but avoiding the complicated set-up using $B^{+}(W)$ to guard the search, we define predicates $G_{i}(W)$ for $W$ a finite rooted $L$-model, and $i<d$, such that $G_{0}(W)$ is always true, and

[TABLE]

We define $G(W)$ by

[TABLE]

Claim 4.21.1

\Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta* if and only if*

[TABLE]

Moreover, we may restrict the size of $W$ on the second line of (21) to $n+O(1)$.

Proof:

Left-to-right: Let $U$ be a finite strongly $L$-extensible $L$-model falsifying $\Gamma\mathrel{/}\Delta$, using Theorem 4.12. First, we show by induction on $i$ that if $u\in U$ is of depth at least $d-i$, then $G_{i}(U_{u})$ holds. This is trivial for $i=0$. For the induction step, if $i>0$, and $C\in\operatorname{Ext}_{L}(U_{u})$, then by strong $L$-extensibility of $U$, we can find a copy of $C$ in $U$ so that the model W=C{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} satisfies $U_{u}\subseteq\mathrel{\cdot}\!W$ and $\mathrm{Fr}(W)=\mathrm{Fr}(U_{u})^{C}$. Since $W\subseteq\mathrel{\cdot}\!U$, $W\vDash\Gamma$. We have $G_{i-1}(W)$ by the induction hypothesis as $\operatorname{rcl}(W)$ has depth at least $d-i+1$.

By taking $i=1$, it follows that $G(U_{u})$ for all $u\in U$. Then the first line of (21) holds by $L$-extensibility of $U$, and the second one as each $\varphi\in\Delta$ is falsified in $U$.

Concerning the bound on $\lvert W\rvert$, let $W=U_{u}$ for some $u\nvDash\varphi$. If $L$ is tabular, $\lvert W\rvert=O(1)$ and we are done. In general, $W$ is a chain of $j\leq d$ clusters $C_{j}<C_{j-1}<\dots<C_{1}$. We first modify the model $U$ to a model $U^{\prime}$ so that for each $1\leq i<j$, we put a new copy of the submodel C_{i+1}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}} below $C_{i}$, and likewise, we include a copy of C_{1}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}} as a new connected component of $U^{\prime}$. Then we shrink each original cluster $C_{i}$ to a subcluster $C^{\prime}_{i}\subseteq C_{i}$ such that:

• •

$\lvert C^{\prime}_{i}\rvert\geq c$, where $c$ is the constant from Corollary 4.16.

• •

$u\in C^{\prime}_{j}$.

• •

For each formula $\psi\in B$ such that $W\nvDash\psi$, let $i$ be minimal such that C_{i}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\nvDash\psi. Then $C^{\prime}_{i}$ includes a point falsifying $\psi$.

Let $W^{\prime\prime}=\bigcup_{i}C^{\prime}_{i}\subseteq W$, and $U^{\prime\prime}=(U^{\prime}\smallsetminus W)\cup W^{\prime\prime}\subseteq U^{\prime}$. Clearly, $U^{\prime\prime}$ is an $L$-frame, $W^{\prime\prime}\subseteq\mathrel{\cdot}\!U^{\prime\prime}$, and the construction ensures that $\operatorname{Sat}_{\Sigma}(U^{\prime},x)=\operatorname{Sat}_{\Sigma}(U^{\prime\prime},x)$ for each $x\in U^{\prime\prime}$; in particular, $U^{\prime\prime}\vDash\Gamma$, and $W^{\prime\prime}\nvDash\varphi$. We have $\lvert W^{\prime\prime}\rvert\leq cd+n$.

We claim that $U^{\prime\prime}$ is strongly $L$-extensible, which implies $G(U^{\prime\prime}_{x})$ for all $x\in U^{\prime\prime}$ by the first part of the proof, and, in particular, $G(W^{\prime\prime})$. So, let $F^{\prime}_{0}\subseteq\mathrel{\cdot}\!U^{\prime\prime}$, and $C\in\operatorname{Ext}_{L}(F^{\prime}_{0})$. Let $F_{0}\supseteq F^{\prime}_{0}$ be the frame obtained by replacing each $C^{\prime}_{i}$ with $C_{i}$ (if it is included in $F^{\prime}_{0}$). By Corollary 4.16, $C\in\operatorname{Ext}_{L}(F_{0})$. If $F_{0}\subseteq U$, strong $L$-extensibility of $U$ ensures there is an isomorphism $f$ of $F_{0}^{C}$ to a generated subframe of $U$ extending $F_{0}$. If $f[C]=C_{i}$ for some $i$, we may modify $f$ so that $f[C]$ is instead the new copy of $C_{i}$ included in $U^{\prime}$. Thus, we may assume that $f[C]$ is disjoint from $W$, hence $f[C]\subseteq U^{\prime\prime}$. But then $f$ maps $F_{0}^{\prime C}$ to a generated subframe of $U^{\prime\prime}$ extending $F^{\prime}_{0}$.

If $F_{0}\nsubseteq U$, it is a rooted frame whose root cluster is inside one of the new copies of C_{i}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}} in $U^{\prime}$. Then strong $L$-extensibility of $U$, applied in the original copy of C_{i}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}} and transferred back, ensures that $\mathrm{id}_{F_{0}}$ extends to an isomorphism $f$ of $F_{0}^{C}$ to a generated subframe of $U^{\prime}$. Since $f[C]$ is also in the new copy of C_{i}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}, it is included in $U^{\prime\prime}$, hence $f$ restricts to an isomorphism of $F_{0}^{\prime C}$ to a generated subframe of $U^{\prime\prime}$.

Right-to-left: For each $C\in\operatorname{Ext}_{L}(\varnothing)$, we fix a model $W_{C}$ based on $C$ such that $G(W_{C})$, and for each $\varphi\in\Delta$, we fix a model $W_{\varphi}\nvDash\varphi$ such that $G(W_{\varphi})$. For each $W_{C}$ and $W_{\varphi}$, we unwind the definition of $G$ to extend the models downwards with all the “tight predecessors” to an upside-down tree of clusters. We let $U$ be the disjoint sum of the models we obtain. Clearly, $U$ is a finite $L$-model such that $U\vDash\Gamma$, and $U\nvDash\varphi$ for each $\varphi\in\Delta$. By induction on $i$, we see that any point $u\in U$ of depth $i$ satisfies $G_{j}(U_{u})$ for some $j\geq d-i$, which was unwinded in the course of the construction of $U$. It follows that $U$ is strongly $L$-extensible: let $F_{0}\subseteq\mathrel{\cdot}\!U$, and $C\in\operatorname{Ext}_{L}(F_{0})$. If $F_{0}=\varnothing$, then a copy of $C$ was added to $U$ as $W_{C}$. Otherwise $F_{0}$ is a rooted $L$-model of depth at most $d-1$, hence $G_{j}(F_{0})$ for some $j\geq 1$, hence $F_{0}$ was extended with a copy of $C$ while unwinding it.     $\Box\hbox{ (Claim 4.21.1)}$

As in the proof of Theorem 4.3, (19)–(21) give an algorithm deciding \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta on an alternating Turing machine. If $L$ is tabular, the clusters $C$ and models $W$ or $W^{\prime}$ appearing in (19)–(21) have bounded size, hence they can be specified using $O(n)$ bits (encoding the relevant valuations of parameters or variables). Thus, the algorithm works in alternating polynomial time. Since it consists of $d$ pairs of universal quantifiers followed by existential quantifiers, it is a $\Pi^{p}_{2d}$ algorithm.

If $L$ has unbounded cluster size, the quantifiers over $C$, $W$, and $W^{\prime}$ in (19)–(21) have exponential size, hence as such, we only get a $\Pi^{\exp}_{2d}$ algorithm. We keep the $\forall C$ quantifiers, but we will need something more efficient for the existential quantifiers. We can do it in the same way as in Lemma 4.1 or Theorem 4.3: instead of specifying the full models $W$ or $W^{\prime}$, we only specify the set of formulas ${\boxdot}\psi$, $\psi\in B$, that they satisfy, while checking separately that this choice of the subset of $B$ is satisfiable in the frame, and validates $\Gamma$. Of course, we also need to know the underlying frame of the model, but in (19) and on the first line of (21), this is already fully specified by $C$. The models $W$ on the second line of (21) may be written down explicitly, as they have polynomial size.

In this way, the existential quantifiers in the algorithm become polynomial-size, hence they can be simulated in deterministic exponential time by trying all possibilities. The universal quantifiers remain, hence we obtain a $\mathrm{coNEXP}$ algorithm for \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta.     ∎

Corollary 4.22

If $L$ is a clx logic of branching [math] and bounded cluster size, then $L$-admissibility is in $\Sigma^{p}_{2}$, and $L$-unifiability in $\Pi^{p}_{2}$.     ∎

For completeness, we will also include an algorithm for admissibility with unlimited parameters in general logics of bounded depth and width with no bound on cluster size. The argument in Lemma 4.18 and Theorem 4.20 only shows that an inadmissible rule is refuted in a strongly extensible model of size $2^{O(2^{n})}$, and this bound cannot be improved. This shows that $L$-admissibility is decidable in \mathrm{coNTIME}\bigl{(}2^{O(2^{n})}\bigr{)}, i.e., in $\mathrm{coNEE}$. We need a little more elaborate argument to obtain complexity that matches lower bounds from the next section (Theorem 5.10).

Definition 4.23

Assume that $\mathrm{Par}$ is finite. Let $L$ be a logic of finite width and depth, and $\Sigma$ a finite set of formulas closed under subformulas.

A finite $L$-model $W$ is a $\Sigma$-pruned $L$-extensible model if for every parametric $L$-frame $F$ with a loosely separated root such that $F\smallsetminus\operatorname{rcl}(F)$ is a generated subframe of (the underlying parametric frame of) $W$, there exists a subframe $F\smallsetminus\operatorname{rcl}(F)\subsetneq F_{1}\subseteq F$ such that $\mathrm{id}_{F\smallsetminus\operatorname{rcl}(F)}$ extends to an isomorphism $f$ of $F_{1}$ to a generated parametric subframe of $W$, and the valuation on $F_{1}$ lifted from $W$ via $f$ extends to a valuation on $F$ such that

[TABLE]

for all $\varphi\in\Sigma$.

Lemma 4.24

Assume that $\mathrm{Par}$ is finite. Let $L$ be a logic of finite width and depth, $\Sigma$ a finite set of formulas closed under subformulas of size $n=\lvert\Sigma\rvert$, and $\Gamma\cup\Delta\subseteq\Sigma$.

1. (i)

If \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta, then $\Gamma\mathrel{/}\Delta$ fails in some $\Sigma$-pruned $L$-extensible model of size $2^{O(n^{2})}$. 2. (ii)

If \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{$\scriptstyle\sim\mathstrut$}}}}_{L}\Delta, then $\Gamma\mathrel{/}\Delta$ holds in all $\Sigma$-pruned $L$-extensible models.

Proof:

(i): Let $c$ be the constant from Corollary 4.16. We may assume $n\geq c$. Since $\Gamma\mathrel{/}\Delta$ is not admissible, we may fix a strongly $L$-extensible model $W$ where it fails.

We first construct a submodel $W^{\prime}\subseteq W$ by reducing each cluster $C\subseteq W$ as follows:

• •

If $\lvert C\rvert\leq c$, then $C\subseteq W^{\prime}$. If $\lvert C\rvert\geq c$, we make sure $\lvert C\cap W^{\prime}\rvert\geq c$.

• •

For each formula $\varphi\in\Sigma$ falsified in some point of $C$, we include at least one such point in $W^{\prime}$.

Clearly $W^{\prime}$ is an $L$-model, and it has cluster size at most $n$. The satisfaction of all formulas from $\Sigma$ is preserved in all points of $W^{\prime}$; in particular, $W^{\prime}$ refutes $\Gamma\mathrel{/}\Delta$. We claim that $W^{\prime}$ is a $\Sigma$-pruned $L$-extensible model, by a similar argument as in the proof of Lemma 4.18: if $F^{\prime}$ is a parametric $L$-frame with a loosely separated root such that $F^{\prime}\smallsetminus\operatorname{rcl}(F^{\prime})\subseteq\mathrel{\cdot}\!W^{\prime}$, let $F$ be $\operatorname{rcl}(F^{\prime})$ attached below (F^{\prime}\smallsetminus\operatorname{rcl}(F^{\prime})){\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\subseteq\mathrel{\cdot}\!W. By Corollary 4.16, $F$ is still an $L$-frame, hence $\mathrm{id}_{F\smallsetminus\operatorname{rcl}(F)}$ extends to an isomorphism $f$ of $F$ to a generated subframe of $W$. Then $F_{1}=f^{-1}[f[F]\cap W^{\prime}]$ has the property required by Definition 4.23.

Next, if $C$ and $C^{\prime}$ are two clusters of $W^{\prime}$ such that G:=C{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\smallsetminus C=C^{\prime}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\smallsetminus C^{\prime}, and $\mathrm{id}_{G}$ extends to an isomorphism of C{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} to C^{\prime}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} (including valuation), let $W^{\prime\prime}$ be the model obtained from $W^{\prime}$ by deleting $C^{\prime}$ and everything below it. Then $W^{\prime\prime}$ is an $L$-model refuting $\Gamma\mathrel{/}\Delta$, and it is still a $\Sigma$-pruned $L$-extensible model: for any $F$ as in the definition with $F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!W^{\prime\prime}$, let us find $F_{1}\subseteq F$ and $f\colon F_{1}\to W^{\prime}$ using $\Sigma$-pruned $L$-extensibility of $W^{\prime}$ so that the conclusion of the definition holds. If $\operatorname{rcl}(f[F_{1}])=C^{\prime}$, we modify it so that $\operatorname{rcl}(f[F_{1}])=C$. Then $f\colon F_{1}\to W^{\prime\prime}$, and it still has the required property.

By continuing in this fashion, we obtain a $\Sigma$-pruned $L$-extensible model $U$ of cluster size $\leq n$ such that no two clusters have the same successors and valuations of parameters and variables. We claim that this implies $\lvert U\rvert=2^{O(n^{2})}$. For $i\leq d$, let $U_{i}$ denote the set of points of depth at most $i$ in $U$. We will prove by induction that $\lvert U_{i}\rvert=2^{O(n^{2})}$. We have $U_{0}=\varnothing$. For the induction step, each cluster $C$ of $U_{i+1}\smallsetminus U_{i}$ has C{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\smallsetminus C generated by an antichain in $U_{i}$, for which there are $\lvert U_{i}\rvert^{O(1)}=2^{O(n^{2})}$ choices. Apart from this, $C$ is uniquely determined by its reflexivity, and its multiset of $\leq n$ valuations to $\mathrm{Par}\cup V$, of which there are \leq\bigl{(}2^{\lvert\mathrm{Par}\cup V\rvert}\bigr{)}^{n+1}=2^{O(n^{2})} choices. Thus, $\lvert U_{i+1}\rvert=2^{O(n^{2})}$.

(ii): Assume that $W_{0}$ is a $\Sigma$-pruned $L$-extensible model refuting $\Gamma\mathrel{/}\Delta$. Put $f_{0}=\mathrm{id}_{W_{0}}$. We will construct a sequence of models $W_{0}\subseteq\mathrel{\cdot}\!W_{1}\subseteq\mathrel{\cdot}\!\dots\subseteq\mathrel{\cdot}\!W_{d}$, and maps $f_{i}\colon W_{i}\to W_{0}$ such that $f_{0}\subseteq f_{1}\subseteq\dots\subseteq f_{d}$, by induction on $i$. Each $f_{i}$ will be a depth-preserving p-morphism of the underlying (non-parametric) frames. It will not preserve the valuation as such, but it will preserve the satisfaction of formulas of the form ${\boxdot}\varphi$ for $\varphi\in\Sigma$.

Assume that $W_{i}$ has been constructed. For each parametric $L$-frame $F$ with a loosely separated root such that $F_{0}=F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!W_{i}$, let $F^{\prime}$ denote the subframe $f_{i}[F_{0}]\subseteq\mathrel{\cdot}\!W_{0}$ with $\operatorname{rcl}(F)$ attached below. Since $f_{i}$ is a frame p-morphism, $F^{\prime}$ is still an $L$-frame with a loosely separated root, and we may apply Definition 4.23 to find $F^{\prime}_{1}\subseteq F^{\prime}$ with $f_{i}[F_{0}]\subsetneq F^{\prime}_{1}$, and a parametric isomorphism $f\supseteq\mathrm{id}_{f_{i}[F_{0}]}$ of $F^{\prime}_{1}$ to a generated subframe $f[F^{\prime}_{1}]\subseteq\mathrel{\cdot}\!W_{0}$. Moreover, we can fix a valuation in $\operatorname{rcl}(F^{\prime})$ so that the same formulas from $\Sigma$ hold in $F^{\prime}$ as in $f[F^{\prime}_{1}]$. The same formulas from $\Sigma$ also hold in $F$ under the valuation obtained using $\operatorname{rcl}(F)=\operatorname{rcl}(F^{\prime})$, as $f_{i}$ preserves the truth of formulas ${\boxdot}\varphi$, $\varphi\in\Sigma$, between $F_{0}$ and $f_{i}[F_{0}]$. We include $\operatorname{rcl}(F)$ with this valuation in $W_{i+1}$, and extend $f_{i}$ to $f_{i+1}$ so that $\operatorname{rcl}(F)$ is mapped onto $\operatorname{rcl}(f[F^{\prime}_{1}])$. We carry out this construction for all frames $F$ simultaneously, so that $W_{i+1}$ is $W_{i}$ together with all the new clusters $\operatorname{rcl}(F)$.

The construction ensures that $W_{d}$ is a model based on a strongly $L$-extensible parametric frame. Since $f_{d}$ preserves the truth of ${\boxdot}\varphi$ for $\varphi\in\Gamma$, we have $W_{d}\vDash\Gamma$, while $W_{d}\nvDash\varphi$ for any $\varphi\in\Delta$, as $W_{0}\subseteq\mathrel{\cdot}\!W_{d}$. Thus, \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta by Theorem 4.12.     ∎

Theorem 4.25

Let $L$ be a logic of bounded depth and width. Then $L$-admissibility is decidable in $\Pi^{\exp}_{2}$, and $L$-unifiability in $\Sigma^{\exp}_{2}$.

Proof:   Let us fix a rule $\Gamma\mathrel{/}\Delta$, and put $\Sigma=\operatorname{Sub}(\Gamma\cup\Delta)$. As in Theorem 4.20, we will proceed as if $\mathrm{Par}$ were finite of size $\leq n$.

By Lemma 4.24, we have \Gamma\mathrel{\vrule width=0.0pt,height=6.94444pt,depth=0.0pt\mkern-1.0mu\lower 0.0pt\hbox{\vbox{\hbox{\hbox to8.22217pt{\hss$\scriptstyle/$\hss}\kern-8.22217pt\hbox{$\scriptstyle\sim\mathstrut$}}}}}_{L}\Delta iff there exists a $\Sigma$-pruned $L$-extensible model $W\nvDash\Gamma\mathrel{/}\Delta$ of size $\lvert W\rvert=2^{O(n^{2})}$. This will give a $\Sigma^{\exp}_{2}$ algorithm for inadmissibility if we show how to check that $W$ is a $\Sigma$-pruned $L$-extensible model in $\mathrm{coNTIME}(2^{O(n^{2})})$. We do this by co-nondeterministically choosing $F$ as in Definition 4.23, and then deterministically testing it satisfies the required condition.

We specify $F$ by selecting one of the $\lvert W\rvert^{O(1)}$ choices for $F\smallsetminus\operatorname{rcl}(F)\subseteq\mathrel{\cdot}\!W$, and by indicating the reflexivity of $\operatorname{rcl}(F)$ as well as the set of assignments $E\subseteq\mathbf{2}^{\mathrm{Par}}$ that are realized in $\operatorname{rcl}(F)$. This can be done with $O(2^{n})$ bits, and we can make sure the choice is sound (i.e., that $F$ is an $L$-frame, and that $\lvert E\rvert=1$ if $\operatorname{rcl}(F)$ is irreflexive).

In order to test a given $F$, we go through the clusters $C$ of $W$ such that C{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\smallsetminus C=F\smallsetminus\operatorname{rcl}(F), $\operatorname{refl}(C)=\operatorname{refl}(\operatorname{rcl}(F))$, $C$ is loosely separated, and the set $E_{1}$ of assignment to parameters realized in $C$ is a subset of $E$. Notice that $E_{1}\subsetneq E$ may only happen in the reflexive case. Then the condition on extension of valuation amounts to

[TABLE]

where $V=\Sigma\cap\mathrm{Var}$, $X=\{\varphi\in\Sigma:C\vDash{\boxdot}\varphi\}$, and $A(v,e,X)$ is as in the proof of Theorem 4.3.     ∎

5 Lower bounds

Our lower bounds generally have the form that unifiability in all logics from a certain class (usually determined by the presence of particular frames as subframes) is hard for some complexity class $\mathcal{C}$, and we will in fact prove more: the reduction showing $\mathcal{C}$-hardness, and even the unifiers of positive instances, will be independent of the logic. We introduce terminology so that we can state this more concisely.

Definition 5.1

Let $\mathcal{L}$ be a class of logics, and $\mathcal{C}$ a complexity class. We say that unifiability in $\mathcal{L}$ is uniformly $\mathcal{C}$-hard, if for every $A\in\mathcal{C}$, there exists a logspace-computable function $w\mapsto\xi_{w}$ such that:

1. (i)

If $w\in A$, there is a substitution $\sigma$ such that $\vdash_{L}\sigma(\xi_{w})$ for every $L\in\mathcal{L}$. 2. (ii)

If $w\notin A$, then $\xi_{w}$ is not $L$-unifiable for any $L\in\mathcal{L}$.

Let us illustrate the concept on a simple example:

Theorem 5.2

Parameter-free unifiability in all consistent logics $L$ is uniformly $\mathrm{NP}$-hard.

Proof:   A propositional formula $\varphi$ with no modal operators or parameters is classically satisfiable if and only if it is $L$-unifiable: on the one hand, a satisfying assignment provides a $\{\bot,\top\}$-substitution that makes the formula a classical tautology; on the other hand, if $\vdash_{L}\sigma(\varphi)$, then the evaluation of $\sigma$ in any fixed element of a fixed $L$-model gives a satisfying assignment for $\varphi$.     ∎

5.1 Exponential hierarchy

In this section, we prove hardness of unifiability for several levels of the exponential hierarchy ($\mathrm{NEXP}$, $\mathrm{coNEXP}$, $\Sigma_{2}^{\exp}$) for logics admitting suitable patterns as subframes, complementing the matching upper bounds from Section 4. In all three cases, we proceed by reducing the truth of third-order formulas from Theorem 2.3 to unifiability. Generally speaking, we use variables to encode existential quantifiers, and parameters to encode universal quantifiers; while second-order objects $t\subseteq n$ may be encoded by $n$ atoms in a straightforward way, third-order objects $X\subseteq\mathcal{P}(n)$ require more complex machinery to ensure they are specified consistently, and it is at this point that the frame patterns are needed.

Theorem 5.3

Unifiability in nonlinear logics is uniformly $\mathrm{NEXP}$-hard.

Proof:   By Theorem 2.3, it is enough to exhibit a logspace reduction from the problem of determining the truth of sentences of the form

[TABLE]

where $n$ is given in unary and $\varphi$ is a Boolean formula. Given $\Phi$, we define a formula $\xi_{\Phi}$ in variables $x,x_{\alpha}$, and parameters $p_{i},p_{\alpha,i},q,r$ for $i<n$ and $\alpha<m$, as the conjunction of the formulas

[TABLE]

for $\alpha<m$, and

[TABLE]

Clearly, $\lvert\xi_{\Phi}\rvert=\operatorname{poly}(n,\lvert\Phi\rvert)$, and the mapping $\Phi\mapsto\xi_{\Phi}$ is logspace-computable.

Claim 5.3.1

If $\Phi$ is true, then $\xi_{\Phi}$ is $\mathbf{K4}$-unifiable.

Proof:   Let W=U_{\mathbf{K4}}\mathopen{\big{missing}}(\{p_{i},p_{\alpha,i},q,r:i<n,\alpha<m\}\mathclose{\big{missing}}), and let us fix a witness $X$ for the existential quantifier in (22). By [8, Thm. 5.18], it suffices to construct a valuation of the variables in $W$ that makes $\xi_{\Phi}$ true in $W$. For any point $u\in W$, we define $t_{\alpha}^{u},t^{u}\subseteq n$ for $\alpha<m$ by

[TABLE]

Then we define the valuation of variables in $u$ by

[TABLE]

The choice of $X$ ensures that $\varphi(\dots,t_{\alpha}^{u}(i),\dots,t_{\alpha}^{u}\in X,\dots)$ is true for any $u\in W$, hence (24) is true in $u$ by the definition of $t_{\alpha}^{u}$ and of the valuation of $x_{\alpha}$.

Concerning (23), let $\alpha<m$, and assume that

[TABLE]

for all $i<n$. This means there exists $t\subseteq n$ such that $t_{\alpha}^{v}=t$ for all $v\geq u$ satisfying $q$, and $t^{v}=t$ for all $v\geq u$ satisfying $r$. It follows that

[TABLE]

if $t\in X$, and

[TABLE]

if $t\notin X$.     $\Box\hbox{ (Claim 5.3.1)}$

Claim 5.3.2

If $L$ is a nonlinear logic, and $\xi_{\Phi}$ is $L$-unifiable, then $\Phi$ is true.

Proof:   Let $\sigma$ be an $L$-unifier of $\xi_{\Phi}$. We may assume that the target formulas of $\sigma$ include no parameters except those occurring in $\xi_{\Phi}$, and no variables. By assumption, there is an $L$-frame $W$ that weakly subreduces onto a two-prong fork; that is, we may assume that $W$ is rooted, and we may fix disjoint nonempty admissible subsets $A,B\subseteq W$ such that A\cap B{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}=B\cap A{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}=\varnothing. Put $P=\{p_{i}:i<n\}$, and $P_{\alpha}=\{p_{\alpha,i}:i<n\}$ for $\alpha<m$.

For any $t\subseteq n$, let $W_{t}$ denote the parametric frame based on $W$ where we make $r\land P^{t}$ true in $A$, and all parameters false elsewhere. In the root of $W_{t}$, the premise of (23) (for arbitrary $\alpha<m$) is true, hence $W_{t}\vDash\sigma(\xi_{\Phi})$ implies

[TABLE]

We define a set $X\subseteq\mathcal{P}(n)$ by

[TABLE]

We claim that $X$ is a witness for the truth of $\Phi$. Let $t_{0},\dots,t_{m-1}\subseteq n$; we need to show that

[TABLE]

is true.

Define a new parametric frame $W^{t_{0},\dots,t_{m-1}}$ based on $W$, where $q\land\bigwedge_{\alpha<m}P_{\alpha}^{t_{\alpha}}$ holds in $B$, and all parameters are false elsewhere. Since $W^{\vec{t}}\vDash\sigma(\xi_{\Phi})$, we have

[TABLE]

and fixing $u\in B$,

[TABLE]

by the definition of $W^{\vec{t}}$, hence (25) will follow if we establish

[TABLE]

for each $\alpha<m$.

Consider the mixed parametric frame $W^{\vec{t}}_{t_{\alpha}}$: that is, make $r\land P^{t_{\alpha}}$ true in $A$, $q\land\bigwedge_{\beta<m}P_{\beta}^{t_{\beta}}$ true in $B$, and all parameters false elsewhere. On the one hand, $W^{\vec{t}}_{t_{\alpha}}$ coincides with $W^{\vec{t}}$ everywhere except in $A$, and B{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\cap A=\varnothing, hence

[TABLE]

On the other hand, $W^{\vec{t}}_{t_{\alpha}}$ coincides with $W_{t_{\alpha}}$ everywhere except in $B$, and A{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\cap B=\varnothing, hence

[TABLE]

for any $v\in A$. To connect these, the premise of (23) for $\alpha$ holds in the root of $W^{\vec{t}}_{t_{\alpha}}$, hence

[TABLE]

which implies

[TABLE]

This shows (26).     $\Box\hbox{ (Claim 5.3.2)}$

The result now follows from Claims 5.3.1 and 5.3.2.     ∎

Corollary 5.4

Let $L$ be a nonlinear clx logic of bounded cluster size, or a nonlinear tabular logic. Then $L$-unifiability is $\mathrm{NEXP}$-complete, and $L$-admissibility is $\mathrm{coNEXP}$-complete.

Proof:   By Theorems 4.2, 4.20, and 5.3.     ∎

Example 5.5

The previous corollary applies to the logics $\mathbf{GL}$, $\mathbf{S4Grz}$, and $\mathbf{K4Grz}$, as well as to their extensions by the $\mathbf{BB}_{k}$ axioms for $k\geq 2$.

Theorem 5.6

Unifiability in logics of unbounded cluster size is uniformly $\mathrm{coNEXP}$-hard.

Proof:   Using Theorem 2.3 again, we will present a logspace reduction from the truth of sentences of the form

[TABLE]

where $n$ is given in unary and $\varphi$ is a Boolean formula. Given $\Phi$, we define a formula $\xi_{\Phi}$ in parameters $p_{i},q$, and variables $z_{\alpha,i}$ for $i<n$ and $\alpha<m$, as the conjunction of the formulas

[TABLE]

where

[TABLE]

The result follows from the next two claims.

Claim 5.6.1

If $\Phi$ is true, then $\xi_{\Phi}$ is $\mathbf{K4}$-unifiable.

Proof:   Putting $W=U_{\mathbf{K4}}\mathopen{(}\vec{p},q\mathclose{)}$, we will construct a valuation in $W$ that makes $\xi_{\Phi}$ true. Since $\Phi$ holds, we may fix for every $Y\subseteq\mathcal{P}(n)$ some sets $t_{0}^{Y},\dots,t_{m-1}^{Y}\subseteq n$ that make $\varphi$ true. Write $P=\{p_{i}:i<n\}$. For each point $u\in W$, we put

[TABLE]

and define

[TABLE]

In order to show that (28) holds, assume $u\vDash\Diamond q$. We can find $u<v\vDash q$ which is $\lnsim$-maximal, i.e., $\neg q$ holds in all points strictly above $\operatorname{cl}(v)$. We claim that this makes $v\vDash\gamma$: indeed, the only points $v^{\prime}\geq v$ that satisfy {\mathchoice{\lower 0.0pt\hbox to6.66669pt{\hss\displaystyle\mathop{\cdot}\hss}\hbox{\displaystyle\Diamond}}{\lower 0.0pt\hbox to6.66669pt{\hss\textstyle\mathop{\cdot}\hss}\hbox{\textstyle\Diamond}}{\lower 0.0pt\hbox to4.66667pt{\hss\scriptstyle\mathop{\cdot}\hss}\hbox{\scriptstyle\Diamond}}{\lower 0.0pt\hbox to3.33334pt{\hss\scriptscriptstyle\mathop{\cdot}\hss}\hbox{\scriptscriptstyle\Diamond}}}q are $v^{\prime}\sim v$, and these have $Y(v^{\prime})=Y(v)$, hence they agree on the satisfaction of all the variables $z_{\alpha,i}$.

As for (29), assume that $u\vDash q\land\gamma$. This means that for each $\alpha<m$, there is $t_{\alpha}\subseteq n$ such that

[TABLE]

for all $i<n$. Since $u\vDash q$, we must have $t_{\alpha}=t_{\alpha}^{Y(u)}$, thus

[TABLE]

is true. This will imply

[TABLE]

if we show

[TABLE]

But (30) ensures that

[TABLE]

which is the definition of $t_{\alpha}\in Y(u)$.     $\Box\hbox{ (Claim 5.6.1)}$

Claim 5.6.2

If $\xi_{\Phi}$ is unifiable in a logic $L$ of cluster size at least $2^{n}+1$, then $\Phi$ is true.

Proof:   Let $\sigma$ be an $L$-unifier of $\xi_{\Phi}$ such that the target formulas of $\sigma$ include no parameters except those occurring in $\xi_{\Phi}$, and no variables. Fix $Y\subseteq\mathcal{P}(n)$: we need to find $t_{0},\dots,t_{m-1}\subseteq n$ satisfying (27).

Let $\{s_{j}:j<l\}$ be an enumeration of $Y$ with $l=\lvert Y\rvert\leq 2^{n}$. By assumption, there exists an $L$-frame $W$ that subreduces onto the $(l+1)$-element cluster: i.e., we may fix disjoint nonempty admissible subsets $A_{j}\subseteq W$, $j\leq l$, such that $A_{j}\subseteq A_{j^{\prime}}\mathord{\downarrow}$ for all $j,j^{\prime}\leq l$. We may assume w.l.o.g. that

[TABLE]

by adding $A_{l}\mathord{\downarrow}\smallsetminus\bigcup_{j\leq l}A_{j}$ to $A_{l}$ if necessary. (Notice that $A_{j}\mathord{\downarrow}=A_{l}\mathord{\downarrow}$ for all $j\leq l$.) With this condition, $\{A_{j}:j\leq l\}$ is in fact a partition of $A_{l}\mathord{\downarrow}$.

We consider the parametric frame based on $W$ such that $A_{j}$ satisfies $P^{s_{j}}$ for $j<l$, $A_{l}$ satisfies $q$, and no parameters hold elsewhere. Since $\vdash_{L}\sigma(\xi_{\Phi})$, there exists $u\in A_{l}$ such that $u\vDash\sigma(\gamma)$ by (28), thus there are $t_{0},\dots,t_{m-1}\subseteq n$ such that

[TABLE]

for each $\alpha<m$ and $i<n$. As in the previous claim, this implies

[TABLE]

Now,

[TABLE]

on the one hand, for each $j<l$, $u$ sees a point $v\in A_{j}$, and we have $v\vDash\neg q\land\Diamond q\land P^{s_{j}}$; on the other hand, all points satisfying $\neg q\land\Diamond q$ are of this form.

Thus,

[TABLE]

follows from $u\vDash\sigma(\ref{eq:30})$.     $\Box\hbox{ (Claim 5.6.2)}$

∎

Corollary 5.7

Let $L$ be a linear clx logic of unbounded cluster size, or a linear logic of bounded depth and unbounded cluster size. Then $L$-unifiability is $\mathrm{coNEXP}$-complete, and $L$-admissibility is $\mathrm{NEXP}$-complete.

Proof:   By Theorems 4.3, 4.21, and 5.6.     ∎

Example 5.8

The previous corollary applies to $\mathbf{S5}$ and to the related logics $\mathbf{K45}$, $\mathbf{D45}$, and $\mathbf{K4B}$. It also applies to the logics $\mathbf{S4.3}$, $\mathbf{K4.3}$, and $\mathbf{D4.3}$, and their extensions by the $\mathbf{BD}_{k}$ axioms for $k\geq 1$.

For our most complex logics, we will prove a $\Sigma_{2}^{\exp}$ lower bound. The argument will combine ideas from both Theorems 5.3 and 5.6. First, let us fix a notation for frames that appear in our $\Sigma_{2}^{\exp}$-hardness criterion.

Definition 5.9

Let $n\geq 1$. The symbol ({\circ}+{\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle n\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle n\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle n\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle n\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}})^{\circ} denotes a finite reflexive Kripke frame consisting of a root and two successor clusters, one of which is an $n$-cluster, and the other one a single point.

Theorem 5.10

Unifiability is uniformly $\Sigma_{2}^{\exp}$-hard in the class of logics $L\supseteq\mathbf{K4}$ such that for every $n\geq 1$, there exists an $L$-frame weakly subreducing onto ({\circ}+{\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle n\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle n\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle n\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle n\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}})^{\circ}.

Proof:   We use Theorem 2.3 once again. Given a sentence

[TABLE]

where $n$ is written in unary and $\varphi$ is a Boolean formula, we define a formula $\xi_{\Phi}$ in parameters $p_{i},q,r$, and variables $x,x_{\alpha},z_{\alpha,i}$ for $i<n$ and $\alpha<m$, as the conjunction of the formulas

[TABLE]

and

[TABLE]

for $\alpha<m$, where

[TABLE]

Claim 5.10.1

If $\Phi$ is true, then $\xi_{\Phi}$ is $\mathbf{K4}$-unifiable.

Proof:   Let $W=U_{\mathbf{K4}}\mathopen{(}\vec{p},q,r\mathclose{)}$; we will construct a valuation in $W$ that makes $\xi_{\Phi}$ true. Let $X$ be a witness for the truth of $\Phi$, and for each $Y\subseteq\mathcal{P}(n)$, let us fix sets $t_{0}^{Y},\dots,t_{m-1}^{Y}\subseteq n$ such that

[TABLE]

is true. Let $P=\{p_{i}:i<n\}$. For each point $u\in W$, we put

[TABLE]

and we define

[TABLE]

As in the proof of Claim 5.6.1, if $u$ is a $\lnsim$-maximal point satisfying $q$, then $u\vDash\gamma$, which shows that $W$ satisfies (32). Moreover, if $u$ is any point such that $u\vDash q\land\gamma$, then

[TABLE]

hence (35) (with $Y=Y(u)$) implies

[TABLE]

establishing the truth of (33).

It is also straightforward to check (34): if its premise holds in $u$, let $t\subseteq n$ be such that

[TABLE]

for all $i<n$. Then all points $v\geq u$ satisfying $q$ have $t_{\alpha}^{Y(v)}=t$, thus

[TABLE]

while all points $w\geq u$ satisfying $r$ have $\operatorname{Sat}_{P}(w)=t$, thus

[TABLE]

again.     $\Box\hbox{ (Claim 5.10.1)}$

Claim 5.10.2

If $\xi_{\Phi}$ is $L$-unifiable, and some $L$-frame weakly subreduces onto ({\circ}+{\mathchoice{\vbox{\hbox to12.22218pt{\hss\scriptstyle l\hss}}\kern-12.22218pt\hbox{\displaystyle\bigcirc}}{\vbox{\hbox to12.22218pt{\hss\scriptstyle l\hss}}\kern-12.22218pt\hbox{\textstyle\bigcirc}}{\vbox{\hbox to9.22218pt{\hss\scriptscriptstyle l\hss}}\kern-9.22218pt\hbox{\scriptstyle\bigcirc}}{\vbox{\hbox to7.22217pt{\hss\scriptscriptstyle l\hss}}\kern-7.22217pt\hbox{\scriptscriptstyle\bigcirc}}})^{\circ} for $l>2^{n}$, then $\Phi$ is true.

Proof:   Let $\sigma$ be an $L$-unifier of $\xi_{\Phi}$ such that the target formulas of $\sigma$ include no parameters except those occurring in $\xi_{\Phi}$, and no variables. By the assumption, we may fix a rooted $L$-frame $W$, and disjoint nonempty admissible subsets $A_{j},B\subseteq W$, $j\leq 2^{n}$, such that B\cap A_{j}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}=A_{j}\cap B{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}=\varnothing, and $A_{j}\subseteq A_{j^{\prime}}\mathord{\downarrow}$ for $j,j^{\prime}\leq 2^{n}$. This implies $A_{j}\mathord{\downarrow}=A_{j^{\prime}}\mathord{\downarrow}$ for all $j,j^{\prime}\leq 2^{n}$. Moreover, we may assume

[TABLE]

by adding the excess A_{j}\mathord{\downarrow}\smallsetminus\bigl{(}B\mathord{\downarrow}\cup\bigcup_{i\leq 2^{n}}A_{i}\bigr{)} to $A_{2^{n}}$.

In order to verify that $\Phi$ is true, we first construct a purported witness $X\subseteq\mathcal{P}(n)$ to the first existential quantifier. For any $t\subseteq n$, let $W_{t}$ denote the parametric frame based on $W$ such that $r\land P^{t}$ holds in $B$, and no parameters elsewhere. Then the root of $W$ satisfies the premise of $\sigma(\ref{eq:32})$ (for arbitrary $\alpha<m$), hence

[TABLE]

We define

[TABLE]

Next, let an arbitrary $Y\subseteq\mathcal{P}(n)$ be given; we need to find $t_{0},\dots,t_{m-1}\subseteq n$ satisfying $\varphi$. Let $l=\lvert Y\rvert\leq 2^{n}$, and fix an enumeration $Y=\{s_{j}:j<l\}$. We define a parametric frame $W^{Y}$ based on $W$ so that $A_{j}\vDash P^{s_{j}}$ for $j<l$, $A_{j}\vDash q$ for $l\leq j\leq 2^{n}$, and no parameters are true elsewhere. Since the root satisfies $\Diamond q$, $W^{Y}\vDash\sigma(\ref{eq:33})$ ensures we can find $u\vDash q\land\sigma(\gamma)$, thus there are $t_{0},\dots,t_{m-1}\subseteq n$ such that

[TABLE]

for all $\alpha<m$ and $i<n$. It remains to prove that

[TABLE]

is true. We have

[TABLE]

by $W^{Y}\vDash\sigma(\ref{eq:34})$,

[TABLE]

for all $\alpha<m$ and $i<n$ by (36), and (36) also implies

[TABLE]

for all $\alpha<m$ as in the proof of Claim 5.6.2. Thus, to complete the proof, we only need to show

[TABLE]

for all $\alpha<m$.

We proceed by constructing a parametric frame combining $W^{Y}$ and $W_{t_{\alpha}}$, exploiting $\vdash_{L}\sigma(\ref{eq:32})$, but we will need to be more careful than in the proof of Claim 5.3.2, because there may be other points satisfying $q\land\sigma(\gamma)$ in the model than $u$, and they may disagree on (36). Thus, let us consider the parametric frame $W^{\prime}$ based on $W$ such that $r\land P^{t_{\alpha}}$ holds in $B$ (as in $W_{t_{\alpha}}$), $P^{s_{j}}$ holds in $A_{j}$ for $j<l$ (as in $W^{Y}$), and $q$ holds in the set

[TABLE]

Notice that $u\in A^{\prime}$, and in fact $W^{\prime}$ agrees with $W^{Y}$ in u{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} (using u{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\cap B=\varnothing), thus

[TABLE]

The definition of $W^{\prime}$ ensures that the premise of $\sigma(\ref{eq:32})$ for $\alpha$ is satisfied in the root, hence

[TABLE]

But $W^{\prime}$ agrees with $W_{t_{\alpha}}$ in B{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}, hence

[TABLE]

by the definition of $X$, which implies

[TABLE]

in view of $W^{\prime},u\vDash q$. Thus, (37) holds.     $\Box\hbox{ (Claim 5.10.2)}$

∎

Corollary 5.11

Let $L$ be a nonlinear clx logic of unbounded cluster size, or a nonlinear logic of bounded depth, bounded width, and unbounded cluster size. Then $L$-unifiability is $\Sigma_{2}^{\exp}$-complete, and $L$-admissibility is $\Pi_{2}^{\exp}$-complete.

Proof:   By Theorems 4.2, 4.25, and 5.10.     ∎

Example 5.12

The previous corollary applies to the basic transitive logics $\mathbf{K4}$, $\mathbf{D4}$, and $\mathbf{S4}$, their variants with the McKinsey axiom $\mathbf{K4.1}$, $\mathbf{D4.1}$, $\mathbf{S4.1}$, and extensions of these logics with the bounded branching axioms $\mathbf{BB}_{k}$ for $k\geq 2$, possibly combined with the bounded depth axioms $\mathbf{BD}_{l}$ for $l\geq 2$.

5.2 $\mathrm{NEXP}$ lower bounds with $O(1)$ parameters

The lower bounds in the previous subsection relied on the supply of arbitrarily many parameters, and it is clear from the upper bounds in Section 4 that Theorems 5.6 and 5.10 intrinsically need them. This leaves the possibility of an $\mathrm{NEXP}$ lower bound on unifiability or inadmissibility with a constant number of parameters. However, Theorems 4.6 and 4.19 show that we need considerably stronger assumptions than in Theorem 5.3 for that to happen: in particular, no fixed finite frame pattern is enough, even allowing for infinite clusters. It is unclear what should be the optimal condition that, on the one hand, guarantees $\mathrm{NEXP}$-hardness of $L$-unifiability (or at least $L$-admissibility) with finitely many parameters, and on the other hand applies to a class of logics as wide as possible.

One such lower bound already appeared in [5]: inadmissibility with no parameters at all is $\mathrm{NEXP}$-complete in logics satisfying a certain ad hoc extensibility condition that operates only with frames of depth $\leq 3$, but requires unbounded width at that depth. As a special case, it applies to all clx logics of unbounded branching. While, as we mentioned, it is not clear what is the optimal lower bound to expect, we will present variants of this construction that apply to $\langle{\bullet},2\rangle$-extensible or $\langle{\circ},2\rangle$-extensible logics, including all nonlinear clx logics.

We will actually present several lower bounds, trading the number of parameters for the strength of assumptions on the logic. All the statements will be proved by varying the details of the same generic construction. As in Theorem 5.3, the overall strategy is to provide a reduction from the truth problem for sentences of the form

[TABLE]

Assume we have an efficiently computable list of formulas

[TABLE]

that do not contain the variable $x$. (In fact, they will not contain any variables in most cases.) We will use points satisfying $\beta_{i}$ as a kind of labels for encoding of the sets $t_{\alpha}\subseteq n$ in (38): a valid encoding of $t_{\alpha}$ will be a point that satisfies $\theta_{\alpha}$, and sees $\beta_{i}$ for $i\in t_{\alpha}$. We will also make use of encoding of $t\subseteq n$ without reference to $\alpha<m$, which will employ $\theta$ instead of $\theta_{\alpha}$. The formulas $\theta_{\alpha}$ and $\theta$ in turn will be defined, on a case-by-case basis, in terms of seeing points satisfying certain other formulas $\gamma_{\alpha}$ and $\delta$. (The precise meaning of this vague description will be made clear in the specific proofs.)

Given (39), we define a formula $\xi_{\Phi}$ as the conjunction of the two formulas

[TABLE]

and

[TABLE]

Lemma 5.13

If $\Phi$ is true, then $\xi_{\Phi}$ is $\mathbf{K4}$-unifiable.

Proof:   Let W=U_{\mathbf{K4}}\mathopen{\big{missing}}(\mathrm{Par}\cap\operatorname{Sub}(\xi_{\Phi})\mathclose{\big{missing}}); we will construct a valuation in $W$ that makes $\xi_{\Phi}$ true. If there are any variables other than $x$, we fix their valuation in an arbitrary way. In order to define the valuation of $x$, we fix a witness $X\subseteq\mathcal{P}(n)$ for $\Phi$. For any $u\in W$, we define

[TABLE]

and we put

[TABLE]

It is easy to see that this makes (40) true, as the value of $x$ in any given point is completely determined by the values of $\Diamond\beta_{i}$ for $i<n$.

As for (41), if its premise holds in $u$, let $t_{0},\dots,t_{m-1}\subseteq n$ be such that

[TABLE]

for each $\alpha<m$ and $i<n$. Since also $u\vDash\Diamond\theta_{\alpha}$, this makes

[TABLE]

Moreover, $t^{v}=t_{\alpha}$ for any $v>u$ such that $v\vDash\theta_{\alpha}$, hence the definition of $v\vDash x$ implies

[TABLE]

Thus,

[TABLE]

follows from the truth of $\varphi(\dots,i\in t_{\alpha},\dots,t_{\alpha}\in X,\dots)$.     ∎

Remark 5.14

We can extract from the proof of Lemma 5.13 a completely explicit unifier $\sigma$ of $\xi_{\Phi}$, namely

[TABLE]

with $\sigma(y)=y$ for all variables $y$ other than $x$.

We are ready for our first lower bound. Recall Definition 3.11.

Theorem 5.15

Unifiability of formulas with $1$ parameters and $1$ variable is uniformly $\mathrm{NEXP}$-hard in the class of logics cofinally subframe-universal for trees.

Proof:   We need to define the formulas (39) in such a way that $\xi_{\Phi}$ is not $L$-unifiable if $\Phi$ is false. The basic idea is that in order to construct a sufficiently large antichain of formulas in one parameter, we identify suitable antichains in $U_{\mathbf{K4}}\mathopen{(}p\mathclose{)}$ (actually, in $U_{\mathbf{S4GrzBB_{2}}}\mathopen{(}p\mathclose{)}$), and describe their points by formulas in a uniform and algorithmically efficient way. This would be easy enough, but there is an additional serious complication that will force us to tread very carefully: our formulas have to work not only in the original subframe $F\subseteq\mathrel{\cdot}\!U_{\mathbf{K4}}\mathopen{(}p\mathclose{)}$, but in an $L$-frame that just weakly cofinally subreduces to $F$.

Formally, we will define a sequence of auxiliary formulas $\{\beta^{d}_{i},\eta^{d}_{i}:i<n_{d}\}$ in parameter $p$ by induction on $d$, and we will simultaneously build a finite parametric frame $F\subseteq\mathrel{\cdot}\!U_{\mathbf{S4}}\mathopen{(}p\mathclose{)}$ with domain $\{a^{d}_{i}:d\in\omega,i<n_{d}\}$ such that $\beta^{d}_{i}$ holds in $a^{d}_{i}$, and $\eta^{d}_{i}$ in a^{d}_{i}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}.

For $d=0$, we put $n_{0}=2$, and

[TABLE]

for $i<2$. The points $a^{0}_{0},a^{0}_{1}\in F$ are incomparable, and $a^{0}_{i}\vDash p^{i}$.

Assume everything has been defined for $2d$. We put $n_{2d+1}=n_{2d}$, and for each $i<n_{2d}$, let

[TABLE]

We introduce new points $\{a^{2d+1}_{i}:i<n_{2d}\}$ in $F$ such that $a^{2d+1}_{i}$ is an immediate predecessor of $a^{2d}_{i}$, and $a^{2d+1}\vDash\neg p$; however, as an exception, $a^{1}_{0}$ will not be a new point: we put $a^{1}_{0}=a^{0}_{0}$. (Notice that $\beta^{1}_{0}$, $\eta^{1}_{0}$, $\beta^{0}_{0}$, and $\eta^{0}_{0}$ are all equivalent.)

At the next level, we put $n_{2d+2}=\binom{n_{2d}+1}{2}$. We will identify $i<n_{2d+2}$ with sets $\{j,k\}$ for $j,k<n_{2d}$ (where $j$ may be equal to $k$) in some canonical way, and we define

[TABLE]

For each $j,k<n_{2d}$, the point $a^{2d+2}_{\{j,k\}}\in F$ is an immediate predecessor of $a^{2d+1}_{j}$ and $a^{2d+1}_{k}$, and $a^{2d+2}_{\{j,k\}}\vDash p$.

Thus, we have $a^{2d+e}_{i}\vDash p^{e}$ for $e=0,1$, except that $a^{0}_{0}=a^{1}_{0}\vDash\neg p$.

The topmost part of $F$ is depicted in Fig. 1.

Claim 5.15.1

For each $d,d^{\prime}\in\omega$ and $i<n_{d}$, $i^{\prime}<n_{d^{\prime}}$,

[TABLE]

Proof:   (43) and (44) are obvious from the definition. As for (45), apart from the exceptional case $a^{0}_{0}\leq a^{1}_{0}$ (where it holds), it suffices to prove it when $a^{d}_{i}$ is an immediate successor of $a^{d^{\prime}}_{i^{\prime}}$, i.e., $d^{\prime}=d+1$, and $i^{\prime}=i$ for $d$ even, or $i^{\prime}=\{i,j\}$ for $d$ odd. In both cases it follows immediately from the definition of $\eta^{d^{\prime}}_{i^{\prime}}$, using (44).

We will prove (46) by induction on $d+d^{\prime}$. We distinguish several cases.

Assume $d$ is odd. If $a^{d^{\prime}}_{i^{\prime}}\nleq a^{d-1}_{i}$, then \vdash\beta^{d}_{i}\to{\mathchoice{\lower 0.0pt\hbox to6.66669pt{\hss\displaystyle\mathop{\cdot}\hss}\hbox{\displaystyle\Diamond}}{\lower 0.0pt\hbox to6.66669pt{\hss\textstyle\mathop{\cdot}\hss}\hbox{\textstyle\Diamond}}{\lower 0.0pt\hbox to4.66667pt{\hss\scriptstyle\mathop{\cdot}\hss}\hbox{\scriptstyle\Diamond}}{\lower 0.0pt\hbox to3.33334pt{\hss\scriptscriptstyle\mathop{\cdot}\hss}\hbox{\scriptscriptstyle\Diamond}}}\beta^{d-1}_{i} by definition, while $\vdash\eta^{d^{\prime}}_{i^{\prime}}\to{\boxdot}\neg\beta^{d-1}_{i}$ by (44) and the induction hypothesis. Otherwise $a^{d^{\prime}}_{i^{\prime}}\leq a^{d-1}_{i}$ and $a^{d^{\prime}}_{i^{\prime}}\nleq a^{d}_{i}$, which is only possible if $\langle d^{\prime},i^{\prime}\rangle=\langle d-1,i\rangle\neq\langle 0,0\rangle$. In particular, $d^{\prime}$ is even. If $d^{\prime}=0$, we thus have $\eta^{d^{\prime}}_{i^{\prime}}={\boxdot}p$, while $\beta^{d}_{i}$ implies $\neg p$. If $d^{\prime}>0$, let $i=\{j,k\}$. Since $\beta^{d}_{i}$ implies $\neg p$, the definition of $\eta^{d^{\prime}}_{i^{\prime}}$ ensures that $\eta^{d^{\prime}}_{i^{\prime}}\land\beta^{d}_{i}$ implies ${\boxdot}(p\to\eta^{d^{\prime}-2}_{j}\lor\eta^{d^{\prime}-2}_{k})$. Also, \vdash\beta^{d}_{i}\to{\mathchoice{\lower 0.0pt\hbox to6.66669pt{\hss\displaystyle\mathop{\cdot}\hss}\hbox{\displaystyle\Diamond}}{\lower 0.0pt\hbox to6.66669pt{\hss\textstyle\mathop{\cdot}\hss}\hbox{\textstyle\Diamond}}{\lower 0.0pt\hbox to4.66667pt{\hss\scriptstyle\mathop{\cdot}\hss}\hbox{\scriptstyle\Diamond}}{\lower 0.0pt\hbox to3.33334pt{\hss\scriptscriptstyle\mathop{\cdot}\hss}\hbox{\scriptscriptstyle\Diamond}}}\beta^{d^{\prime}}_{i}, where $\vdash\beta^{d^{\prime}}_{i}\to p$, hence

[TABLE]

This implies a contradiction by the induction hypothesis, as $a^{d^{\prime}-2}_{j}\nleq a^{d^{\prime}}_{i}$ and $a^{d^{\prime}-2}_{k}\nleq a^{d^{\prime}}_{i}$.

If $d$ is even and $d^{\prime}$ is odd, then $\vdash\beta^{d}_{i}\to p\lor\Box\neg p$, hence the definition of $\eta^{d^{\prime}}_{i^{\prime}}$ ensures $\vdash\beta^{d}_{i}\land\eta^{d^{\prime}}_{i^{\prime}}\to\eta^{d^{\prime}-1}_{i^{\prime}}$, which leads to a contradiction by the induction hypothesis as $a^{d^{\prime}-1}_{i^{\prime}}\nleq a^{d}_{i}$.

The remaining case is if both $d$ and $d^{\prime}$ are even. First, if one of the immediate successors $a^{d-1}_{j}$ of $a^{d}_{i}$ satisfies $a^{d^{\prime}}_{i^{\prime}}\nleq a^{d-1}_{j}$, then $\vdash\beta^{d}_{i}\to\Diamond\beta^{d-1}_{j}$, while $\vdash\eta^{d^{\prime}}_{i^{\prime}}\to\Box\neg\beta^{d-1}_{j}$ by (44) and the induction hypothesis. Thus, we may assume that all immediate successors of $a^{d}_{i}$ are above $a^{d^{\prime}}_{i^{\prime}}$.

If $d^{\prime}=0$, this forces $d=0$ as well; since $i\neq i^{\prime}$, $\beta^{d}_{i}\land\eta^{d^{\prime}}_{i^{\prime}}$ is ${\boxdot}p\land{\boxdot}\neg p$, which is contradictory.

If $d^{\prime}>0$, let $i^{\prime}=\{j^{\prime},k^{\prime}\}$. If $\langle d,i\rangle=\langle 0,0\rangle$, i.e., $\beta^{d}_{i}={\boxdot}\neg p$, the definition of $\eta^{d^{\prime}}_{i^{\prime}}$ gives

[TABLE]

and the disjuncts $\eta^{d^{\prime}-2}_{j^{\prime}}$ and $\eta^{d^{\prime}-2}_{k^{\prime}}$ lead to contradiction by the induction hypothesis, as $a^{d^{\prime}-2}_{j^{\prime}}\nleq a^{d}_{i}$ and $a^{d^{\prime}-2}_{k^{\prime}}\nleq a^{d}_{i}$. Otherwise $\vdash\beta^{d}_{i}\to p$, hence the definition of $\eta^{d^{\prime}}_{i^{\prime}}$ gives

[TABLE]

where $\eta^{d^{\prime}-2}_{j^{\prime}}$ and $\eta^{d^{\prime}-2}_{k^{\prime}}$ lead to contradiction as above, hence

[TABLE]

Notice that $\vdash\beta^{d^{\prime}-1}_{j^{\prime}/k^{\prime}}\to\neg p$. Thus, (47) directly leads to contradiction if $\langle d,i\rangle=\langle 0,1\rangle$, as $\beta^{d}_{i}={\boxdot}p$. If $d>0$ and $i=\{j,k\}$, then the definition of $\beta^{d}_{i}$ ensures

[TABLE]

Since also \vdash\beta^{d^{\prime}-1}_{j^{\prime}/k^{\prime}}\to{\mathchoice{\lower 0.0pt\hbox to6.66669pt{\hss\displaystyle\mathop{\cdot}\hss}\hbox{\displaystyle\Diamond}}{\lower 0.0pt\hbox to6.66669pt{\hss\textstyle\mathop{\cdot}\hss}\hbox{\textstyle\Diamond}}{\lower 0.0pt\hbox to4.66667pt{\hss\scriptstyle\mathop{\cdot}\hss}\hbox{\scriptstyle\Diamond}}{\lower 0.0pt\hbox to3.33334pt{\hss\scriptscriptstyle\mathop{\cdot}\hss}\hbox{\scriptscriptstyle\Diamond}}}\beta^{d^{\prime}-2}_{j^{\prime}/k^{\prime}}, where $\beta^{d^{\prime}-2}_{j^{\prime}/k^{\prime}}$ implies $p\lor\Box\neg p$, (47) yields

[TABLE]

Recall that $a^{d^{\prime}}_{i^{\prime}}\leq a^{d-1}_{j}$ and $a^{d^{\prime}}_{i^{\prime}}\leq a^{d-1}_{k}$. This means

[TABLE]

and similarly for $a^{d-1}_{k}$; in particular, $d^{\prime}\geq d$. On the other hand, using the induction hypothesis, (48) gives the desired $\vdash\neg(\beta^{d}_{i}\land\eta^{d^{\prime}}_{i^{\prime}})$ unless

[TABLE]

and similarly for $a^{d^{\prime}-2}_{k^{\prime}}$. In particular, this implies $d\geq d^{\prime}$, thus $d=d^{\prime}$. Then (49) actually means $j\in\{j^{\prime},k^{\prime}\}$, and together with the analogous property of $k$ we obtain $\{j,k\}\subseteq\{j^{\prime},k^{\prime}\}$, while (50) and its analogue for $k^{\prime}$ give $\{j^{\prime},k^{\prime}\}\subseteq\{j,k\}$. Thus $i=\{j,k\}=\{j^{\prime},k^{\prime}\}=i^{\prime}$, a contradiction.     $\Box\hbox{ (Claim 5.15.1)}$

Notice that $n_{2d}$ is strictly increasing. Since $n_{d}$ roughly squares every other step, it is asymptotically doubly exponential in $d$: $n_{d}=2^{2^{\Omega(d)}}$. On the other hand, the size of the formulas $\beta^{d}_{i}$, $\eta^{d}_{i}$ is $2^{O(d)}$.

For our application, we take the least even $D$ such that $n_{D}\geq n+m+2$, and we define the formulas (39) as follows: $\beta_{i}=\beta^{D}_{i}$ for $i<n$, $\gamma_{\alpha}=\beta^{D}_{n+\alpha}$ for $\alpha<m$, $\delta=\beta^{D}_{n+m}$, and

[TABLE]

for each $\alpha<m$. We have $D=O(\log\log(n+m))$, thus $\lvert\beta^{D}_{i}\rvert=(\log(n+m))^{O(1)}$. It is not difficult to check that the formulas are logspace-constructible. Claim 5.15.1 shows the key property

[TABLE]

In particular, $\theta_{\alpha}$ implies $\theta$.

We also need to construct some finite trees (in the form of parametric reflexive frames) related to the representation of $\Phi$ by $\xi_{\Phi}$. We use $+$ or $\sum$ to denote disjoint sum as usual, and $F^{p}$ (or $F^{\neg p}$) denotes $F$ extended below with a with new root, satisfying $p$ (or $\neg p$, respectively).

First, for any $d\in\omega$ and $i<n_{d}$, let $T^{d}_{i}$ be $F_{x^{d}_{i}}$ unravelled into a tree: that is, $T^{0}_{i}=\varnothing^{p^{i}}$ (i.e., the trivial tree satisfying $p^{i}$) for $i<2$; $T^{2d+1}_{i}$ is $(T^{2d}_{i})^{\neg p}$ for $i<n_{2d}$, $\langle d,i\rangle\neq\langle 0,0\rangle$, while $T^{1}_{0}=T^{0}_{0}$; and $T^{2d+2}_{\{j,k\}}=(T^{2d+1}_{j}+T^{2d+1}_{k})^{p}$ (it does not matter if we simplify this to $(T^{2d+1}_{j})^{p}$ in the case $j=k$ or not).

We put $T_{\beta_{i}}=T^{D}_{i}$ for $i<n$, $T_{\gamma_{\alpha}}=T^{D}_{n+\alpha}$, and $T_{\delta}=T^{D}_{n+m}$ in accordance with the definition of the formulas. We also define a “dummy” tree $T_{-}=T^{D}_{n+m+1}$.

For every $t\subseteq n$, let T_{t}=\bigl{(}T_{-}+T_{-}+\sum_{i\in t}T_{\beta_{i}}\bigr{)}^{p}. Next, we put $T_{t,\alpha}=(T_{\delta}+T_{\gamma_{\alpha}}+T_{t})^{p}$ for each $\alpha<m$. Then, for every $\vec{t}=\langle t_{0},\dots,t_{c-1}\rangle\in(\mathcal{P}(n))^{m}$, we define T_{\vec{t}}=\bigl{(}\sum_{\alpha<m}T_{t_{\alpha},\alpha}\bigr{)}^{p}. Finally, we pack all this into one huge tree T=\bigl{(}\sum_{\vec{t}}T_{\vec{t}}\bigr{)}^{p}.

If $T_{\dots}$ is any of the trees above, let $r_{\dots}$ denote its root; in particular, $r$ denotes the root of $T$.

We now assume that $L$ is cofinally subframe-universal for trees, thus there exists an $L$-frame $W$ and a weak cofinal subreduction $g$ from $W$ onto (the underlying frame of) $T$. We might assume that $W$ is rooted, and its root is mapped to $r$ by $f$. We adjust the subreduction by putting

[TABLE]

for all $u\in W$ and $x\in T$. It is easy to see that the purported $f$-preimages of points of $T$ are disjoint, hence $f$ is a well-defined partial map $W\to T$. Moreover, $g^{-1}[x]\subseteq f^{-1}[x]$ and f^{-1}[x]{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}=g^{-1}[x]{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}} for each $x\in T$. This implies that $f$ is still a cofinal weak subreduction from $W$ to $T$. Moreover, the preimages $f^{-1}[x]$ are convex: f^{-1}[x]{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\cap f^{-1}[x]{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}\subseteq f^{-1}[x]. We now define a valuation of the parameter $p$ in $W$ by

[TABLE]

Let $h$ be the p-morphism from $T$ to $F$ mapping the root of each embedded copy of $T^{d}_{i}$ to $x^{d}_{i}$. Since $\operatorname{dom}(h)$ is a cofinal generated subframe of $T$, $h\circ f$ is a cofinal weak subreduction from $W$ to $F$ with convex preimages.

Claim 5.15.2

For any $u\in\operatorname{dom}(h\circ f)$,

[TABLE]

Proof:   By induction on $d$. If $d=0$, then $a^{d}_{i}$ is a leaf of $F$, thus (h\circ f)[u{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}]=\{a^{d}_{i}\}. By cofinality and convexity of $h\circ f$, we have in fact u{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\subseteq(h\circ f)^{-1}[a^{d}_{i}]. Thus, $u\vDash{\boxdot}p^{i}$.

Assume the result holds up to $2d$, and let $h(f(u))=a^{2d+1}_{i}$. Clearly, $u\vDash\neg p$, and u\vDash{\mathchoice{\lower 0.0pt\hbox to6.66669pt{\hss\displaystyle\mathop{\cdot}\hss}\hbox{\displaystyle\Diamond}}{\lower 0.0pt\hbox to6.66669pt{\hss\textstyle\mathop{\cdot}\hss}\hbox{\textstyle\Diamond}}{\lower 0.0pt\hbox to4.66667pt{\hss\scriptstyle\mathop{\cdot}\hss}\hbox{\scriptstyle\Diamond}}{\lower 0.0pt\hbox to3.33334pt{\hss\scriptscriptstyle\mathop{\cdot}\hss}\hbox{\scriptscriptstyle\Diamond}}}\beta^{2d}_{i} by the induction hypothesis. In order to check $u\vDash\eta^{2d+1}_{i}$, let $u\leq v\vDash p\lor\Box\neg p$. If $v\vDash p$, we have $v\in\operatorname{dom}(f)$, thus $h(f(v))=a^{d^{\prime}}_{i^{\prime}}\geq a^{2d+1}_{i}$; since $h(f(v))\vDash p$, actually $a^{d^{\prime}}_{i^{\prime}}\geq a^{2d}_{i}$. By the induction hypothesis, $v\vDash\beta^{d^{\prime}}_{i^{\prime}}$, hence $v\vDash\eta_{i}^{2d}$ by Claim 5.15.1. Otherwise, $v\vDash{\boxdot}\neg p$; by cofinality, there is $w\geq v$ such that $w\in\operatorname{dom}(h\circ f)$, and we may choose it so that $h(f(w))$ is a leaf. By the $d=0$ case, we cannot have $h(f(w))=a^{0}_{1}$, as $w\vDash{\boxdot}\neg p$. Thus, $h(f(w))=a^{0}_{0}$; since $h\circ f$ is a subreduction, $a^{2d}_{i}\leq a^{0}_{0}$, thus $\vdash{\boxdot}\neg p\to\eta^{2d}_{i}$ by Claim 5.15.1, thus $v\vDash\eta^{2d}_{i}$.

Now, let $h(f(u))=a^{2d+2}_{\{j,k\}}$. Again, $u\vDash p$ holds by definition, and $u\vDash\Diamond\beta^{2d+1}_{j}\land\Diamond\beta^{2d+1}_{k}$ by the induction hypothesis, hence it suffices to show $u\vDash\eta^{2d+2}_{\{j,k\}}$.

If $u\leq v\vDash p$, then $v\in\operatorname{dom}(h\circ f)$, and $a^{d^{\prime}}_{i^{\prime}}:=h(f(v))$ satisfies $a^{d^{\prime}}_{i^{\prime}}=a^{2d+2}_{\{j,k\}}$ or $a^{d^{\prime}}_{i^{\prime}}\geq a^{2d}_{j}$ or $a^{d^{\prime}}_{i^{\prime}}\geq a^{2d}_{k}$. In the first case, we have $v\vDash\Diamond\beta^{2d+1}_{j}\land\Diamond\beta^{2d+1}_{k}$ by the induction hypothesis; otherwise, the induction hypothesis gives $v\vDash\beta^{d^{\prime}}_{i^{\prime}}$, hence $v\vDash\eta^{2d}_{j}$ or $v\vDash\eta^{2d}_{k}$ by Claim 5.15.1.

Assume $u\leq v\leq w$, $v\vDash\neg p$, and $w\vDash p\lor\Box\neg p$. If $w\vDash p$, then again $w\in\operatorname{dom}(h\circ f)$, and $a^{d^{\prime}}_{i^{\prime}}:=h(f(w))$ satisfies $a^{d^{\prime}}_{i^{\prime}}=a^{2d+2}_{\{j,k\}}$ or $a^{d^{\prime}}_{i^{\prime}}\geq j$ or $a^{d^{\prime}}_{i^{\prime}}\geq a^{2d}_{k}$. The first case is in fact impossible: if $h(f(u))=h(f(w))=a^{2d+2}_{\{j,k\}}$, then $h(f(v))=a^{2d+2}_{\{j,k\}}$ as well by convexity, contradicting $v\nvDash p$. Thus, we have $w\vDash\eta^{2d}_{j}$ or $w\vDash\eta^{2d}_{k}$ as above333It may happen here that $v\notin\operatorname{dom}(f)$, while $v\in(h\circ f)^{-1}[a^{2d}_{j}]$ and $v\in(h\circ f)^{-1}[a^{2d}_{k}]$, even if $j\neq k$. Then $v$ satisfies neither $\eta^{2d+1}_{j}$ nor $\eta^{2d+1}_{k}$. It is precisely for this reason that we did not simplify the second conjunct of $\eta^{2d+2}_{\{j,k\}}$ to ${\boxdot}(\neg p\to\eta^{2d+1}_{j}\lor\eta^{2d+1}_{k})$, as one might be tempted to do just looking at $F$.. The remaining case $w\vDash{\boxdot}\neg p$ is left to the reader.     $\Box\hbox{ (Claim 5.15.2)}$

Claim 5.15.2 and (53) imply that each of the formulas $\beta_{0},\dots,\beta_{n-1},\gamma_{0},\dots,\gamma_{m-1},\delta$ holds in $W$ only in points $u$ such that $f(u)$ is the root of a copy of the corresponding tree $T_{\beta_{0}},\dots,T_{\delta}$. Consequently, $\theta_{\alpha}$ holds only in preimages of copies of $r_{t,\alpha}$ for some $t\subseteq n$.

We are getting ready to bring the proof of Theorem 5.15 to an end. Assume that $\xi_{\Phi}$ is $L$-unifiable, and let $\sigma$ be its unifier. We may assume $\sigma(x)$ uses no parameters except for $p$, and no variables.

We need to define a witness $X$ for $\Phi$. For any $t\subseteq n$, we put $t\in X$ if a preimage of some copy of $r_{t,\alpha}$ for some $\alpha<m$ satisfies $\sigma(x)$. Crucially, this definition does not depend on the choices:

Claim 5.15.3

If $t\subseteq n$, and $u,v\in W$ are such that $f(u)$ is a copy of $r_{t,\alpha}$ and $f(v)$ a copy of $r_{t,\beta}$ for some $\alpha,\beta<m$, then

[TABLE]

Proof:   Let $T^{\prime}$ be the frame $T$ with valuation of $p$ modified so that $p$ is false everywhere outside copies of $T_{t,\alpha}$ or $T_{t,\beta}$. Let $W^{\prime}$ be the corresponding modification of $W$:

[TABLE]

In $W^{\prime}$, $\theta$ holds only in points $w$ such that $f(w)$ is a copy of $r_{t,\alpha}$ or $r_{t,\beta}$. All these points satisfy the same formulas of the form $\Diamond\beta_{i}$, namely $w\vDash\Diamond\beta_{i}$ iff $i\in t$. Thus, the root $r$ of $W^{\prime}$ satisfies the premise of $\sigma(\ref{eq:40})$. This implies

[TABLE]

and in particular, $u\vDash\sigma(x)$ iff $v\vDash\sigma(x)$.     $\Box\hbox{ (Claim 5.15.3)}$

Now, let $t_{0},\dots,t_{m-1}\subseteq n$; we need to show

[TABLE]

Let $u\in\operatorname{dom}(f)$ be such that $f(u)$ is a copy of $r_{\vec{t}}$. The only points above $u$ that satisfy $\theta_{\alpha}$ are preimages of the embedded copy of $T_{t_{\alpha},\alpha}$, and these satisfy the same formulas of the form $\Diamond\beta_{i}$ (viz., such that $i\in t_{\alpha}$). In other words, $u$ satisfies the premise of $\sigma(\ref{eq:41})$, hence

[TABLE]

Moreover,

[TABLE]

hence (54) follows. This completes the proof of Theorem 5.15.     ∎

Corollary 5.16

Unifiability of formulas with $1$ parameters and $1$ variable is $\mathrm{NEXP}$-hard for all logics with the disjunction property.

Proof:   By Theorems 5.15 and 3.13.     ∎

Example 5.17

The cofinality condition in the statement of Theorem 5.15 cannot be dropped. For example, the logic $L=\mathbf{S4.2Grz}$ is subframe-universal for trees, but $L$-unifiability of formulas with one parameter is $\mathrm{NP}$-complete. The universal frame $U_{L}\mathopen{(}p\mathclose{)}$ consists of two disjoint infinite descending chains alternating between $p$ and $\neg p$, one with $p$ on top, and the other with $\neg p$ on top. It is easy to show that a formula $\varphi\in\operatorname{Form}(\{p\},\mathrm{Var})$ is $L$-unifiable iff there exists a valuation $\vDash$ in $U_{L}(p)$ that makes $U_{L}(p)\vDash\varphi$ iff there exists a valuation that makes $\varphi$ true in the top $2n$ levels of $U_{L}(p)$, where $n=\lvert\{\psi:\Box\psi\subseteq\varphi\}\rvert+1$. This condition can be checked in $\mathrm{NP}$.

Nevertheless, the result holds under somewhat weaker assumptions. In particular, if the single-atom fragment of $L$ is included in a logic cofinally subframe-universal for trees, then $L$-unifiability of formulas in $1$ parameter and $1$ variable is $\mathrm{NEXP}$-hard. For example, this applies to bounded top-width logics such as $L=\mathbf{S4BTW_{2}}$: the single-atom fragment of $L$ is included in $\mathbf{S4Grz}$ (which is cofinally subframe-universal for trees), as $U_{\mathbf{S4Grz}}(p)$ has top width $2$.

Unification with $1$ parameter is also $\mathrm{NEXP}$-hard for logics that are subframe-universal in a way that respects reflexivity of points, see Theorem 5.20.

Moreover, we can easily generalize the lower bound to all subframe-universal logics at the expense of using one more parameter:

Theorem 5.18

Unifiability of formulas with $2$ parameters and $1$ variable is uniformly $\mathrm{NEXP}$-hard in the class of logics subframe-universal for trees.

Proof:   We use almost the same construction as in the proof of Theorem 5.15, except that we take another parameter $q$, and relativize the formulas (39) (recall Definition 3.5): instead of $\beta_{i}$, $\theta_{\alpha}$, and $\theta$, we use $q\land\beta_{i}^{q}$, $q\land\theta_{\alpha}^{q}$, and $q\land\theta^{q}$. The proof proceeds as before, but the subreduction $f$ is not necessarily cofinal, and we put

[TABLE]

The only place where we used the cofinality of $f$ in the proof of Theorem 5.15 was in Claim 5.15.3, to ensure that $(h\circ f)^{-1}[a^{0}_{1}]\vDash{\boxdot}p$, and that certain points satisfying ${\boxdot}\neg p$ are in (h\circ f)^{-1}[a^{0}_{0}]{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}. Relativization side-steps both issues: the former property turns into $(h\circ f)^{-1}[a^{0}_{1}]\vDash{\boxdot}(q\to p)$, which follows immediately from $h\circ f$ being a subreduction and the definition of satisfaction of $q$; the latter property holds because the points in question will now satisfy $q$, hence they will be in the domain of $h\circ f$.     ∎

Going in the opposite direction, we may ask if at least one parameter is needed for $\mathrm{NEXP}$-hardness of unification in, say, nonlinear clx logics. In general, the answer is yes: parameter-free unifiability is in $\mathrm{NP}$ for a large class of logics, including all extensions of $\mathbf{D4}$ or $\mathbf{GL}$. However, we can prove $\mathrm{NEXP}$-hardness for logics that allow enough mixing of reflexive and irreflexive points. The theorem below gives a typical and reasonably useful sufficient condition, but similar results also holds for some other logics—basically, what is needed is that we can construct embeddings of arbitrarily large trees into $U_{L}\mathopen{(}\varnothing\mathclose{)}$ in a uniform and efficient manner.

Using the relativization technique, we can also obtain additional $\mathrm{NEXP}$-hardness results for unifiability with one parameter in this way. Specifically, it applies to logics that satisfy a variant of subframe-universality for trees including both reflexive and irreflexive points. As with Definition 3.11, we may equivalently state the definition for trees, for binary trees, or for arbitrary frames without proper clusters; this time we chose the last one, to emphasize that we treat the objects as frames rather than combinatorial shapes, hence their reflexivity matters.

Definition 5.19

A logic $L\supseteq\mathbf{K4}$ is subframe-universal for simple frames if for each finite rooted frame $F$ without proper clusters, there exists an $L$-frame that subreduces onto $F$; equivalently, if $\vdash_{L}\mathsf{R}(\varphi)$ implies $\vdash_{\mathbf{K4Grz}}\varphi$ for all formulas $\varphi$.

For example, $\mathbf{D4.2}$ is subframe-universal for simple frames, but not cofinally subframe-universal for trees, and parameter-free $\mathbf{D4.2}$-unifiability is in $\mathrm{NP}$.

Theorem 5.20

1. (i)

Unifiability of formulas without parameters and with $1$ variable is uniformly $\mathrm{NEXP}$-hard in sublogics of $\mathbf{K4.2GrzBB_{2}}$. 2. (ii)

Unifiability of formulas with $1$ parameters and $1$ variable is uniformly $\mathrm{NEXP}$-hard in the class of logics subframe-universal for simple frames.

Proof:

(i): We follow similar strategy as in the proof of Theorem 5.15. We construct $\beta_{i}$ as formulas defining points in a certain antichain in $U_{L}\mathopen{(}\varnothing\mathclose{)}$; instead of the parameter $p$, we will distinguish points by their reflexivity.

We will define antichains $\{a^{d}_{i}:i<n_{d}\}\subseteq U_{L}\mathopen{(}\varnothing\mathclose{)}$ by induction on $d$. There is more than one way to do it. For conciseness of notation, if $X$ is a finite subset of $U_{L}\mathopen{(}\varnothing\mathclose{)}$, and ${*}\in\{{\bullet},{\circ}\}$, let $\operatorname{tp}_{*}(X)$ denote the unique ${*}$-tp of X{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} in $U_{\mathbf{K4}}\mathopen{(}\varnothing\mathclose{)}$. We will only use this notation if it is guaranteed that actually $\operatorname{tp}_{*}(X)\in U_{L}\mathopen{(}\varnothing\mathclose{)}$ (in particular, $X$ is generated by at most $2$ points), and if X{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} is not rooted with a reflexive root, so that always \operatorname{tp}_{*}(X)\notin X{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}.

We put $n_{0}=1$, $n_{1}=n_{2}=2$, $n_{3}=4$, and $n_{d+1}=\binom{n_{d}+1}{2}$ for $d\geq 3$. Let $a^{0}_{0}=\operatorname{tp}_{\bullet}(\varnothing)$ be the irreflexive leaf of $U_{L}\mathopen{(}\varnothing\mathclose{)}$, $a^{1}_{0}=\operatorname{tp}_{\circ}(a^{0}_{0})$, and $a^{1}_{1}=\operatorname{tp}_{\bullet}(a^{0}_{0})$. All remaining points will be irreflexive: $a^{2}_{0}=\operatorname{tp}_{\bullet}(a^{1}_{0},a^{1}_{1})$, $a^{2}_{1}=\operatorname{tp}_{\bullet}(a^{1}_{1})$, $a^{3}_{0}=\operatorname{tp}_{\bullet}(a^{2}_{0})$, $a^{3}_{1}=\operatorname{tp}_{\bullet}(a^{2}_{0},a^{2}_{1})$, $a^{3}_{2}=\operatorname{tp}_{\bullet}(a^{1}_{0},a^{2}_{1})$, and $a^{3}_{3}=\operatorname{tp}_{\bullet}(a^{2}_{1})$. For $d\geq 3$, we identify $i<\binom{n_{d}+1}{2}$ with sets $\{j,k\}$ for $j,k<n_{d}$ (not necessarily distinct), and we put $a^{d+1}_{\{j,k\}}=\operatorname{tp}_{\bullet}(a^{d}_{j},a^{d}_{k})$. (See Fig. 2.)

We define $\beta^{d}_{i}$ as the formulas $\beta_{a^{d}_{i}}$ from (1). As in the proof of Theorem 5.15, we have $n_{d}=2^{2^{\Omega(d)}}$. In order to see that $\lvert\beta^{d}_{i}\rvert=2^{O(d)}$, it is better to present the formulas in a slightly different way. Let $\eta_{u}=\bigvee_{v\geq u}\beta_{v}$; we may define $\beta_{u}$ and $\eta_{u}$ by simultaneous recursion

[TABLE]

where $\{u_{i}:i<m_{u}\}$ are the immediate successors of $u$, and $u$ is irreflexive. (We leave the reflexive case to the reader, as with our choice of antichains, it is irrelevant.) Since in our case $m_{u}\leq 2$, the formulas $\beta_{u}$ and $\eta_{u}$ are built from $O(1)$ instances of $\beta_{v}$ and $\eta_{v}$ for $v$ of lower depth, hence the bound $\lvert\beta^{d}_{i}\rvert\leq 2^{O(d)}$ follows by induction on $d$.

As in the proof of Theorem 5.15, we take $D$ minimal such that $n_{D}\geq n+m+2$, and define the formulas (39) by $\beta_{i}=\beta^{D}_{i}$ for $i<n$, $\gamma_{\alpha}=\beta^{D}_{n+\alpha}$ for $\alpha<m$, $\delta=\beta^{D}_{n+m}$, and

[TABLE]

We have $D=O(\log\log(n+m))$, thus $\lvert\beta^{D}_{i}\rvert=(\log(n+m))^{O(1)}$, and it is routine to verify that the formulas are logspace-constructible. We denote $a_{\beta_{i}}=a^{D}_{i}$ for $i<n$, $a_{\gamma_{\alpha}}=a^{D}_{n+\alpha}$ for $\alpha<m$, $a_{\delta}=a^{D}_{n+m}$, and $a_{-}=a^{D}_{n+m+1}$.

For each $t\subseteq n$, we define $a_{t}\in U_{L}\mathopen{(}\varnothing\mathclose{)}$ as a predecessor of $\{a_{-}\}\cup\{a_{\beta_{i}}:i\in t\}$ arranged in a binary tree of tp’s: that is, if $t=\{i_{j}:j<l\}$, we put

[TABLE]

For any $\alpha<m$, we define

[TABLE]

Finally, for each $\vec{t}\in(\mathcal{P}(n))^{m}$, let

[TABLE]

We have to show that if $\vdash_{L}\sigma(\xi_{\Phi})$, then $\Phi$ is true. We may assume that $\sigma(x)\in\operatorname{Form}(\varnothing,\varnothing)$. We define a set $X\subseteq\mathcal{P}(n)$ by

[TABLE]

for any $t\subseteq n$ and $\alpha<m$. This definition is independent of the choice of $\alpha$: putting $u=\operatorname{tp}_{\bullet}(a_{t,\alpha},a_{t,\alpha^{\prime}})$, the only element of u{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} that satisfies $\delta$ is $a_{\delta}$, hence $\theta$ only holds in the three points $u,a_{t,\alpha},a_{t,\alpha^{\prime}}$. These all see $a_{\beta_{i}}$ for $i\in t$, and for no other $i<n$. Thus, $u$ satisfies the premise of $\sigma(\ref{eq:40})$, hence its conclusion, which gives

[TABLE]

To check that $X$ is a witness for $\Phi$, let $\vec{t}\in(\mathcal{P}(n))^{m}$. As above, it is easy to see that $\theta_{\alpha}$ is satisfied in a_{\vec{t}}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} only in the point $a_{t_{\alpha},\alpha}$, hence $a_{\vec{t}}$ satisfies the premise of $\sigma(\ref{eq:41})$, hence

[TABLE]

Moreover,

[TABLE]

hence (54) is true.

(ii): We relativize the formulas used in (i), i.e., we define $\beta_{i}=p\land(\beta^{D}_{i})^{p}$, $\gamma_{\alpha}=p\land(\beta^{D}_{n+\alpha})^{p}$, $\delta=p\land(\beta^{D}_{n+m})^{p}$, and we define $\theta,\theta_{\alpha}$ as in (51) and (52).

Continuing the argument from (i), let $a\in U_{\mathbf{K4}}\mathopen{(}\varnothing\mathclose{)}$ be a common predecessor of all the points $a_{\vec{t}}$ for $\vec{t}\in(\mathcal{P}(n))^{m}$. By assumption, there exists an $L$-frame $W$, and a subreduction f\colon W\twoheadrightarrow a{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}. We make $W$ into a parametric frame by putting

[TABLE]

Recall that by Lemma 3.9, we have

[TABLE]

for all $u\in\operatorname{dom}(f)$ and $\varphi\in\operatorname{Form}(\varnothing,\varnothing)$.

Let $\sigma$ be an $L$-unifier of $\xi_{\Phi}$ such that $\sigma(x)\in\operatorname{Form}(p,\varnothing)$. We define $X\subseteq\mathcal{P}(n)$ by

[TABLE]

Using (40) and a modified valuation that makes $p$ true only in f^{-1}[a_{t,\alpha}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\cup a_{t,\alpha^{\prime}}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}], we may check that the definition of $X$ does not depend on the choice of $\alpha$ or $u$ in (55).

Then, for any $\vec{t}\in(\mathcal{P}(n))^{m}$, we take $u\in f^{-1}[a_{\vec{t}}]$, and using (41) we obtain

[TABLE]

from which (54) follows as usual.     ∎

As we already mentioned, parameter-free unification is in $\mathrm{NP}$ for a large number of logics of interest. One way to make it harder is to use parameters, but another way is to consider admissibility rather than unification: parameter-free admissibility is $\mathrm{coNEXP}$-hard for typical logics of unbounded branching, as shown in [5]. We will generalize this result to a class of logics that includes all $\langle{\circ},2\rangle$-extensible or $\langle{\bullet},2\rangle$-extensible logics, and in particular, all nonlinear clx logics.

While we can prove hardness of unification using “static” conditions requiring the presence of suitable subframes, it seems that hardness of admissibility requires “dynamic” conditions expressing closure properties of the class of $L$-frames. Thus, the condition we employ is a little peculiar to formulate:

Definition 5.21

Let $T$ be a (finite) tree. A logic $L\supseteq\mathbf{K4}$ has the weak $T$-extension property if for every labelling of the leaves of $T$ by finite clusters that are $L$-frames, there exists an $L$-frame $W$ with skeleton $T$ such that the final clusters of $W$ are isomorphic to their labels in $T$.

If $\mathcal{T}$ is a family of trees, $L$ has the weak extension property wrt $\mathcal{T}$ if if has the weak $T$-extension property for each $T\in\mathcal{T}$.

A family of trees $\mathcal{T}$ is depth-$3$-universal if every tree of depth $3$ embeds (as a poset) in a tree $T\in\mathcal{T}$.

Example 5.22

The depth-$3$ weak extension property, proved to imply $\mathrm{coNEXP}$-hardness of parameter-free admissibility in [5, Thm. 4.13], is nothing else than the weak extension property wrt the family of all trees of depth $3$.

The family of all depth-$3$ trees is trivially depth-$3$-universal. The family of all binary trees is also depth-$3$-universal.

Recall that a caterpillar is a tree that becomes a single path if we remove all leaves; a binary caterpillar tree thus consists of a central path $x_{0}<x_{1}<\dots<x_{n}$, with at most one additional leaf vertex attached to each $x_{i}$. Let us define a squared caterpillar to be a tree obtained from a caterpillar by replacing each of its leaves with a caterpillar. Then the family of binary squared caterpillars is depth-$3$-universal.

Theorem 5.23

Single-conclusion admissibility without parameters is uniformly $\mathrm{coNEXP}$-hard in the class of all logics satisfying the weak extension property wrt a depth-$3$-universal family of trees (including all $\langle{\circ},2\rangle$-extensible or $\langle{\bullet},2\rangle$-extensible logics).

Proof:   Given a sentence $\Phi$ as in (38), we define formulas

[TABLE]

using variables $\{z_{i}:i<n+m+4\}$, and we define $\xi_{\Phi}$ as $(\ref{eq:40})\land(\ref{eq:41})$. We aim to prove

[TABLE]

For the left-to-right implication, Lemma 5.13 and Remark 5.14 show that there is a $\mathbf{K4}$-unifier $\sigma$ of $\xi_{\Phi}$ such that $\sigma(z_{i})=z_{i}$ for all $i<n+m+4$, thus $\sigma(\zeta_{\Phi})=\zeta_{\Phi}$. It remains to observe that $\nvdash_{L}\zeta_{\Phi}$: it suffices to take a finite rooted $L$-frame with $\geq n+m+4$ final clusters, where we make $z_{i}$ (and consequently, $\beta_{i}$) true only in the $i$th cluster; the existence of such an $L$-frame follows from the weak extension property.

For the right-to-left implication, let $\sigma$ be an $L$-unifier of $\xi_{\Phi}$ such that $\nvdash_{L}\sigma(\zeta_{\Phi})$. For each $i<n+m+4$, $\sigma(\beta_{i})$ is satisfiable in a finitely generated descriptive $L$-frame $W_{i}$. Since it has the form ${\boxdot}(\dots)$, it holds on a cone; using descriptivity, this cone contains a final cluster, which is finite due to $W_{i}$ being finitely generated. Thus, we may fix a finite single-cluster model $B_{i}\vDash\sigma(\beta_{i})$ based on an $L$-frame. We will write $C_{\alpha}=B_{n+\alpha}$ for $\alpha<m$, and $D_{p}=B_{n+m+p}$ for $p<4$.

At least two of the clusters $D_{1},D_{2},D_{3}$ have the same reflexivity; w.l.o.g. $\operatorname{refl}(D_{1})=\operatorname{refl}(D_{2})$. We may also assume $\lvert D_{1}\rvert=\lvert D_{2}\rvert$ by replicating some point from the smaller cluster if necessary.

Let $S$ be the depth-$3$ tree consisting of a root with $m2^{n+1}$ immediate successors, each of which has $n+4$ successors. By assumption, $S$ embeds in a tree $T$ such that $L$ has the weak $T$-extension property. This means that $T$ includes an antichain $A$ of size $m2^{n+1}$ such that each element $a\in A$ sees at least $n+4$ leaves. If an element $a\in A$ has only one immediate successor $a^{\prime}$, we may replace $a$ with $a^{\prime}$ while keeping the number of leaves. Thus, we may assume w.l.o.g. that every $a\in A$ splits. Going in the opposite direction, let $a^{-}\leq a$ be the minimal element below $a$ such that no element of the chain $[a^{-},a]$ splits except $a$.

We can find a subset $A_{0}\subseteq A$ of size $\geq m2^{n}$ such that for each $a\in A_{0}$, $a^{-}$ has a sibling that sees a leaf in T\smallsetminus A_{0}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}. Indeed, let $\sim$ be the equivalence relation on $A$ defined by $a_{0}\sim a_{1}$ iff $a_{0}^{-}$ is a sibling of $a_{1}^{-}$, and let $A_{0}$ be constructed from $A$ by removing one element from each $\sim$-equivalence class of size $\geq 2$. Since we removed at most half of the elements, we have $\lvert A_{0}\rvert\geq\lvert A\rvert/2=m2^{n}$, and it is easy to see that $A_{0}$ has the required property. We name $m2^{n}$ elements of $A_{0}$ as $\{r_{t,\alpha}:t\subseteq n,\alpha<m\}$.

We will label each leaf of $T$ with one of the clusters $B_{i}$, $i<n+m+4$, as follows. Let $t\subseteq n$ and $\alpha<m$. There are $\geq n+4$ leaves in r_{t,\alpha}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}. For each $p=1,2,3$, we choose one leaf above $r_{t,\alpha}$ and label it with $D_{p}$; we do it in such a way that the leaves labelled with $D_{1}$ and $D_{2}$ are above different immediate successors of $r_{t,\alpha}$, thus no element strictly above $r_{t,\alpha}$ sees both. For each $i\in t$, we label one leaf above $r_{t,\alpha}$ with $B_{i}$. We label the remaining leaves above $r_{t,\alpha}$ with $C_{\alpha}$. Finally, we label every leaf of $T$ that is not above any $r_{t,\alpha}$ with $D_{0}$.

By the weak $T$-extension property, there exists an $L$-frame $W$ obtained from $T$ by choosing the reflexivity of each inner node, and replacing each leaf with (the underlying frame of) its label. We will identify the corresponding inner nodes of $T$ and $W$. We consider $W$ not just as a frame, but also as a model: the valuation of variables in leaf clusters is taken from the corresponding $B_{i}$ models, and the valuation in inner nodes is arbitrary (say, all variables are false).

Notice that $\vdash_{\mathbf{K4}}\beta_{i}\to{\boxdot}\neg\beta_{i^{\prime}}$ for $i\neq i^{\prime}$. Each leaf cluster of $W$ is labelled with some $B_{i}$, and it then satisfies $\sigma(\beta_{i})$, and $\neg\sigma(\beta_{i^{\prime}})$ for all $i^{\prime}\neq i$. An inner node of $W$ that sees leaves with two different labels cannot satisfy any $\sigma(\beta_{i})$.

It follows that for any $u\in W$,

[TABLE]

Indeed, the right-to-left implications follow easily from the definition. On the other hand, if $u$ is not above any $r_{t,\alpha^{\prime}}^{-}$, the construction of $A_{0}$ ensures that $u$ sees a leaf labelled $D_{0}$, hence u\vDash\sigma({\mathchoice{\lower 0.0pt\hbox to6.66669pt{\hss\displaystyle\mathop{\cdot}\hss}\hbox{\displaystyle\Diamond}}{\lower 0.0pt\hbox to6.66669pt{\hss\textstyle\mathop{\cdot}\hss}\hbox{\textstyle\Diamond}}{\lower 0.0pt\hbox to4.66667pt{\hss\scriptstyle\mathop{\cdot}\hss}\hbox{\scriptstyle\Diamond}}{\lower 0.0pt\hbox to3.33334pt{\hss\scriptscriptstyle\mathop{\cdot}\hss}\hbox{\scriptscriptstyle\Diamond}}}\delta_{0}), which implies $u\nvDash\sigma(\theta)$. If $u\gnsim r_{t,\tilde{\alpha}}$ for some $t\subseteq n$ and $\tilde{\alpha}<m$, then $u\nvDash\sigma(\Diamond\delta_{1}\land\Diamond\delta_{2})$, hence $u\nvDash\sigma(\theta)$ again. And if $r_{t,\alpha^{\prime}}^{-}\leq u\leq r_{t,\alpha^{\prime}}$ for some $t$ and $\alpha^{\prime}\neq\alpha$, then $u\vDash\Diamond\gamma_{\alpha^{\prime}}$, which implies $u\nvDash\sigma(\theta_{\alpha})$.

Claim 5.23.1

Let $t\subseteq n$, $\alpha,\alpha^{\prime}<m$, and $u,u^{\prime}\in W$ be such that $r_{t,\alpha}^{-}\leq u\leq r_{t,\alpha}$ and $r_{t,\alpha^{\prime}}^{-}\leq u^{\prime}\leq r_{t,\alpha^{\prime}}$. Then

[TABLE]

Proof:   We define a modified valuation $\vDash^{t}$ in $W$ as follows: for any leaf cluster labelled $D_{1}$ above some $r_{\tilde{t},\tilde{\alpha}}$, where $\tilde{t}\neq t$, we change the valuation to match $D_{2}$. (This is possible because $D_{1}$ and $D_{2}$ have isomorphic underlying frames.) This ensures that no point $v\geq r_{\tilde{t},\tilde{\alpha}}^{-}$ satisfies $\sigma(\Diamond\delta_{1})$, and consequently, $v\nvDash\sigma(\theta)$. Thus, the only points that satisfy $\sigma(\theta)$ in $\langle W,{\vDash^{t}}\rangle$ are the elements of $\bigcup_{\tilde{\alpha}<c}[r_{t,\tilde{\alpha}}^{-},r_{t,\tilde{\alpha}}]$. All these points satisfy the same formulas of the form $\sigma(\Diamond\beta_{i})$, namely those such that $i\in t$.

This means $\langle W,{\vDash^{t}}\rangle$ satisfies the premise of $\sigma(\ref{eq:40})$ in the root, hence

[TABLE]

In particular, (59) follows, as the valuation in r_{t,\alpha}^{-}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}}\cup r_{t,\alpha^{\prime}}^{-}{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} is unchanged, and $u,u^{\prime}\vDash\sigma(\theta)$.     $\Box\hbox{ (Claim 5.23.1)}$

In view of Claim 5.23.1, we may define a set $X\subseteq\mathbf{2}^{n}$ such that

[TABLE]

for all $t\subseteq n$, $\alpha<m$, and $u\in W$. We claim that $X$ is a witness for the truth of $\Phi$. Let $\vec{t}\in(\mathcal{P}(n))^{m}$, we need to show that

[TABLE]

holds. Similarly to the proof of Claim 5.23.1, we consider a modified valuation $\vDash^{\vec{t}}$ where we “disable” $D_{1}$ leaf clusters that are not above $r_{t_{\alpha},\alpha}$ for any $\alpha<m$ by turning them into a $D_{2}$. The new valuation satisfies $\sigma(\theta_{\alpha})$ only in the interval $[r_{t_{\alpha},\alpha}^{-},r_{t_{\alpha},\alpha}]$, hence the premise of $\sigma(\ref{eq:41})$ holds in the root $r$ of $W$, hence also

[TABLE]

Moreover, we have

[TABLE]

hence (60) follows.     ∎

Remark 5.24

We could slightly relax the weak $T$-extension property: it is enough to ask that there exists an $L$-frame $W$, and a weak p-morphism $f\colon W\twoheadrightarrow T$ (i.e., a p-morphism $f\colon W^{\circ}\twoheadrightarrow T$) such that for each leaf $a\in T$ with label $C$, there is a p-morphism $f_{C}\colon f^{-1}[a]\twoheadrightarrow C$. Since the class of $L$-frames is stable under p-morphic images, this is almost equivalent to Definition 5.21; the only difference arises because a single node of $T$ may have both reflexive and irreflexive preimages in $W$, hence it may not be possible to choose reflexivity of inner nodes of $T$ in a consistent way so that $f$ becomes a true p-morphism from $W$. However, we do not know of any interesting application where this would make a difference, hence we prefer the simpler formulation of Definition 5.21.

5.3 $\mathrm{PSPACE}$ and below

Theorem 5.25

1. (i)

For any $d>0$, unifiability in logics of depth at least $d$ is uniformly $\Pi^{p}_{2d}$-hard. 2. (ii)

Unifiability of formulas with $2$ parameters and $1$ variable in logics of unbounded depth is uniformly $\mathrm{PSPACE}$-hard.

Proof:   Let us define auxiliary formulas

[TABLE]

for $i\in\omega$ and $e\in\mathbf{2}$. The meaning is that $w\vDash\delta_{i,e}$ iff there is a chain $w=w_{i}<w_{i-1}<\dots<w_{0}$ where $q$ is alternately true and false, with it being true (false) in $w_{i}$ if $e=1$ ([math], resp.), and $w\vDash\theta_{i,e}$ if, in addition, there is no longer chain. The formula $\theta_{i}$ is normalized so that the chain has $w_{0}\nvDash q$ on top. (If $w\vDash q^{e}$ sees a proper cluster in which both $q$ and $\neg q$ are realized, then $w\vDash\delta_{i,e}$ and $w\nvDash\theta_{i,e}$ for all $i\in\omega$.)

In particular, $w\vDash\theta_{i}$ (or $w\vDash\delta_{i,e}$) implies that $w$ has depth $>i$, and in a model where $q$ holds exactly in points of even depth, we have $w\vDash\theta_{i}$ iff the depth of $w$ is $i+1$. It follows from the description that

[TABLE]

Let

[TABLE]

be a given quantified Boolean sentence with $\varphi$ quantifier-free, where each $\vec{a}_{i}$ stands for an $m$-tuple $a_{i,0},\dots,a_{i,m-1}$, and similarly for $\vec{b}_{i}$. We define a formula $\xi_{\Phi}$ in $m+1$ parameters $p_{0},\dots,p_{m-1},q$, and $m$ variables $x_{0},\dots,x_{m-1}$, as the conjunction of the formulas

[TABLE]

where

[TABLE]

Notice that $\lvert\theta_{i}\rvert=O(i)$, hence \lvert\xi_{\Phi}\rvert=O\bigl{(}d^{2}m+d\lvert\varphi\rvert\bigr{)}=O\bigl{(}\lvert\Phi\rvert^{2}\bigr{)}; it is also easy to see that the mapping $\Phi\mapsto\xi_{\Phi}$ is logspace-computable.

Claim 5.25.1

If $\Phi$ is true, then $\xi_{\Phi}$ is $\mathbf{K4}$-unifiable.

Proof:   For $i\leq d$, denote

[TABLE]

Note that $\Phi_{0}=\Phi$ and $\Phi_{d}=\varphi$. For every $i<d$ and $\vec{a}_{0},\dots,\vec{a}_{i},\vec{b}_{0},\dots,\vec{b}_{i-1}\in\mathbf{2}^{m}$ such that $\exists\vec{b}_{i}\,\Phi_{i+1}(\vec{a}_{0},\dots,\vec{a}_{i},\vec{b}_{0},\dots,\vec{b}_{i})$ is true, fix a witness $F_{i}(\vec{a}_{0},\dots,\vec{a}_{i},\vec{b}_{0},\dots,\vec{b}_{i-1})\in\mathbf{2}^{m}$ for the $\exists\vec{b}_{i}$ quantifier block. Also, define

[TABLE]

by induction on $i<d$. Since $\Phi_{0}$ is true, we can show by induction on $i$ that

[TABLE]

is true for every $i\leq d$ and every $\vec{a}_{0},\dots,\vec{a}_{i-1}\in\mathbf{2}^{m}$.

Let $W=U_{\mathbf{K4}}\mathopen{(}\vec{p},q\mathclose{)}$; by [8, Thm. 5.18], it suffices to construct a valuation of $\vec{x}$ in $W$ that makes $W\vDash\xi_{\Phi}$. Let $w\in W$. If $w\vDash\theta_{i}\land\gamma$ for some $i<d$ (which is unique by (61)), let $\vec{a}_{0}(w),\dots,\vec{a}_{i}(w)\in\mathbf{2}^{m}$ be the unique Boolean vectors such that $v\vDash p_{j}^{a_{i^{\prime},j}(w)}$ for every $i^{\prime}\leq i$, $j<m$, and $v\geq w$ such that $v\vDash\theta_{i^{\prime}}$: their existence and uniqueness follows from (62) and $w\vDash\gamma$. Putting \vec{b}_{i}(w)=G_{i}\bigl{(}\vec{a}_{0}(w),\dots,\vec{a}_{i}(w)\bigr{)}, we define valuation of $\vec{x}$ in $w$ so that $w\vDash x_{j}^{b_{i,j}(w)}$ for each $j<m$. If $w\nvDash\gamma$, or $w\nvDash\theta_{i}$ for any $i<d$, we define $w\vDash x_{j}$ arbitrarily.

Assume that $w\vDash\gamma$, and fix $i<d$. Then every $v,v^{\prime}\geq w$ satisfying $\theta_{i}$ also satisfy $\gamma$, and we have $\vec{a}_{i^{\prime}}(v)=\vec{a}_{i^{\prime}}(v^{\prime})$ for every $i^{\prime}\leq i$, hence $v$ and $v^{\prime}$ agree on the satisfaction of $\vec{x}$. It follows that $w\vDash{\boxdot}(\theta_{i}\to x_{j})\lor{\boxdot}(\theta_{i}\to\neg x_{j})$ for each $j<m$. As $i$ was arbitrary, (64) is true in $W$.

By the same argument, if $w\vDash\theta_{d-1}\land\gamma$, then

[TABLE]

for each $i<d$ and $j<m$. Since $\Phi_{d}=\varphi$, we have \varphi\bigl{(}\vec{a}_{0}(w),\dots,\vec{a}_{d-1}(w),\vec{b}_{0}(w),\dots,\vec{b}_{d-1}(w)\bigr{)} by (67) and the choice of $\vec{b}_{i}(w)$, thus (65) holds in $W$ as well.     $\Box\hbox{ (Claim 5.25.1)}$

Claim 5.25.2

If a logic $L$ has depth at least $d$, and $\xi_{\Phi}$ is $L$-unifiable, then $\Phi$ is true.

Proof:   By the assumption, there exists a finite $L$-frame $F$ of depth $d$ with root $r$. Let $\sigma$ be an $L$-unifier of $\xi_{\Phi}$, w.l.o.g. chosen so that its target formulas contain no variables, and only the parameters $\vec{p},q$. Assume for contradiction that $\Phi$ is false. Put $w\vDash q$ iff $w\in F$ has even depth, so that $w\vDash\theta_{i}$ iff $w$ has depth $i+1$.

By induction on $i\leq d$, we will fix valuation of $\vec{p}$ in points of $F$ of depth at most $i$, and $\vec{a}_{0},\dots,\vec{a}_{i-1},\vec{b}_{0},\dots,\vec{b}_{i-1}\in\mathbf{2}^{m}$ such that $\Phi_{i}(\vec{a}_{0},\dots,\vec{a}_{i-1},\vec{b}_{0},\dots,\vec{b}_{i-1})$ is false. The valuation will be defined so that $w\vDash p_{j}^{a_{i^{\prime},j}}$ and $w\vDash\sigma(x_{j})^{b_{i^{\prime},j}}$ for every $w\in F$ of depth $i^{\prime}+1$, where $i^{\prime}<i$; notice that $\sigma(x_{j})$ is a formula in the parameters $\vec{p},q$, and its value in $w$ is only affected by the valuation of $p_{j}$ in points of depth $i^{\prime}+1\leq i$ or less, hence it will not change in later steps.

The base step $i=0$ is trivial—we only observe that $\Phi_{0}$ is false by assumption. Assume the construction has been carried out up to $i<d$. Since $\Phi_{i}(\vec{a}_{0},\dots,\vec{a}_{i-1},\vec{b}_{0},\dots,\vec{b}_{i-1})$ is false, we can fix $\vec{a}_{i}\in\mathbf{2}^{m}$ such that

[TABLE]

Define $w\vDash p_{j}^{a_{i,j}}$ for all $j<m$ and $w\in F$ of depth $i+1$, and temporarily put (say) $w\nvDash p_{j}$ for all $w$ of depth more than $i+1$. By the definition and the induction hypothesis, this makes $\gamma$ true in $r$. Since $\vdash_{L}\sigma(\xi_{\Phi})$, we have $r\vDash{\boxdot}(\theta_{i}\to\sigma(x_{j}))\lor{\boxdot}(\theta_{i}\to\neg\sigma(x_{j}))$. Thus, there exists a unique $\vec{b}_{i}\in\mathbf{2}^{m}$ such that $w\vDash\sigma(x_{j})^{b_{i,j}}$ for every $w$ of depth $i+1$ and $j<m$. As explained above, this is independent of the temporary definition of valuation of $\vec{p}$, as the valuation in points of depth at most $i+1$ has already been fixed. The formula $\Phi_{i+1}(\vec{a}_{0},\dots,\vec{a}_{i},\vec{b}_{0},\dots,\vec{b}_{i})$ is false by (68).

When the construction is finished, we have $r\vDash\theta_{d-1}\land\gamma$, and the valuation of {\mathchoice{\lower 0.0pt\hbox to6.66669pt{\hss\displaystyle\mathop{\cdot}\hss}\hbox{\displaystyle\Diamond}}{\lower 0.0pt\hbox to6.66669pt{\hss\textstyle\mathop{\cdot}\hss}\hbox{\textstyle\Diamond}}{\lower 0.0pt\hbox to4.66667pt{\hss\scriptstyle\mathop{\cdot}\hss}\hbox{\scriptstyle\Diamond}}{\lower 0.0pt\hbox to3.33334pt{\hss\scriptscriptstyle\mathop{\cdot}\hss}\hbox{\scriptscriptstyle\Diamond}}}(\theta_{i}\land p_{j}) and {\mathchoice{\lower 0.0pt\hbox to6.66669pt{\hss\displaystyle\mathop{\cdot}\hss}\hbox{\displaystyle\Diamond}}{\lower 0.0pt\hbox to6.66669pt{\hss\textstyle\mathop{\cdot}\hss}\hbox{\textstyle\Diamond}}{\lower 0.0pt\hbox to4.66667pt{\hss\scriptstyle\mathop{\cdot}\hss}\hbox{\scriptstyle\Diamond}}{\lower 0.0pt\hbox to3.33334pt{\hss\scriptscriptstyle\mathop{\cdot}\hss}\hbox{\scriptscriptstyle\Diamond}}}(\theta_{i}\land\sigma(x_{j})) in $r$ agrees with $a_{i,j}$ and $b_{i,j}$, respectively, for each $i<d$ and $j<m$, hence $\varphi(\vec{a}_{0},\dots,\vec{a}_{d-1},\vec{b}_{0},\dots,\vec{b}_{d-1})$ is true due to $\vdash_{L}\sigma(\xi_{\Phi})$. However, this is a contradiction, as $\varphi=\Phi_{d}$.     $\Box\hbox{ (Claim 5.25.2)}$

For fixed $d$, validity of quantified Boolean sentences of the form (63) is a $\Pi^{p}_{2d}$-complete problem, hence Claims 5.25.1 and 5.25.2 imply (i). When $d$ is unrestricted, the validity problem for (63) is $\mathrm{PSPACE}$-complete, and we may arrange $m=1$ by inserting dummy quantifiers to make universal and existential quantifiers alternate. This shows (ii).     ∎

We may strengthen Theorem 5.25 by combining it with our other lower bounds, observing that $\mathrm{PSPACE}$ (and $\Pi^{p}_{2d}$) is included in both $\mathrm{NEXP}$ and $\mathrm{coNEXP}$:

Corollary 5.26

1. (i)

Unifiability in all logics except tabular logics of width $1$ is uniformly $\mathrm{PSPACE}$-hard. 2. (ii)

For every $d>0$, unifiability in all logics except tabular logics of width $1$ and depth at most $d-1$ is uniformly $\Pi^{p}_{2d}$-hard.

In particular, unifiability in all consistent logics is uniformly $\Pi^{p}_{2}$-hard.

Proof:   Let $A$ be a language in $\mathrm{PSPACE}$ or $\Pi^{p}_{2d}$ as appropriate. Let $w\mapsto\xi^{0}_{w}$, $w\mapsto\xi^{1}_{w}$, and $w\mapsto\xi^{2}_{w}$ be the reductions supplied by Theorems 5.3, 5.6, and 5.25 (respectively). We may assume that the formulas $\xi^{0}_{w}$, $\xi^{1}_{w}$, and $\xi^{2}_{w}$ use disjoint sets of variables. Then $\xi_{w}:=\xi^{0}_{w}\land\xi^{1}_{w}\land\xi^{2}_{w}$ is $L$-unifiable if and only if each $\xi^{i}_{w}$ is, thus:

• •

if $w\in A$, then $\xi_{w}$ is $\mathbf{K4}$-unifiable;

• •

if $w\notin A$, then $\xi_{w}$ is not $L$-unifiable for any logic $L$ that is nonlinear, or of unbounded cluster size, or of sufficiently large depth.

The three classes of logics in the second point together cover the class from the statement of this corollary.     ∎

Corollary 5.27

Let $L$ be a consistent linear clx logic of bounded cluster size. If $L$ has branching at least $1$ (hence unbounded depth), then $L$-unifiability and $L$-admissibility are $\mathrm{PSPACE}$-complete; otherwise, $L$-unifiability is $\Pi^{p}_{2}$-complete, and $L$-admissibility $\Sigma^{p}_{2}$-complete.

If $L$ is a linear tabular logic of depth (exactly) $d\geq 1$, then $L$-unifiability is $\Pi^{p}_{2d}$-complete, and $L$-admissibility is $\Sigma^{p}_{2d}$-complete.

Proof:   By Theorems 4.3, 4.21, and 5.25.     ∎

Example 5.28

$L$-unifiability and $L$-admissibility are $\mathrm{PSPACE}$-complete for the logics $L=\mathbf{GL.3}$, $\mathbf{S4.3Grz}$, and $\mathbf{K4.3Grz}$. Unifiability in $L\oplus\mathbf{BD}_{d}$ is $\Pi^{p}_{2d}$-complete for $d\geq 1$.

Unifiability is also $\Pi^{p}_{2}$-complete in the logics $\mathbf{Verum}=\mathbf{K4}\oplus\Box\bot$ or $\mathbf{S5}\oplus\mathbf{Alt}_{k}$ for $k\geq 1$.

In general, two parameters are necessary in Theorem 5.25 (ii):

Example 5.29

The logic $L=\mathbf{S4.2Grz}$ or the clx logic $L=\mathbf{S4Grz.3}$ have unbounded depth, but $L$-unifiability of formulas with one parameter is $\mathrm{NP}$-complete, as shown in Example 5.17.

Unifiability with one parameter in $\mathbf{S4.3}$ is also $\mathrm{NP}$-complete: the universal frame is only modified by attaching copies of the two-element cluster realizing both $p$ and $\neg p$ below each original node, and including an additional copy as a third connected component. We leave the details to the reader.

However, we will show for completeness that one parameter is sufficient under a stronger hypothesis, namely that the logic admits arbitrarily long irreflexive chains (possibly embedded among reflexive points). Note that at least one parameter is needed anyway, as parameter-free unifiability is in $\mathrm{NP}$ even for irreflexive logics such as $\mathbf{GL}$.

Definition 5.30

A logic $L$ has irreflexive depth at least $n$ if there exists an $L$-frame that subreduces onto an $n$-element irreflexive chain. A logic has unbounded irreflexive depth if it has irreflexive depth at least $n$ for all $n\in\omega$.

Theorem 5.31

Unifiability of formulas with $1$ parameter and $1$ variable in logics of unbounded irreflexive depth is uniformly $\mathrm{PSPACE}$-hard.

Proof:   As in the proof of Theorem 5.25 (i), we will provide a reduction from validity of quantified Boolean sentences of the form (63) with $m=1$, but instead of $p_{0}$ and $q$, we will need to reuse a single parameter $q$ for detecting the depth and for specifying $a_{i}$. (Since $m=1$, we will omit the vector signs, and write just $a_{i},b_{i}$ instead of $a_{i,0},b_{i,0}$.) Roughly, the idea is that each quantifier pair $\forall a_{i}\,\exists b_{i}$ corresponds to three irreflexive points in a chain: the top one will satisfy $\neg q$, the bottom one $q$, and the middle one will depend on $a_{i}$. In this way, we get two alternations in the value of $q$ for each $i$ irrespective of the value of $a_{i}$, while we can read off $a_{i}$ by checking if the $i$th layer of points satisfying $q$ contains a nontrivial chain $u<v$. (Here we are using the irreflexivity.) The value of $b_{i}$ will be given using a variable $x$, one level lower still (so that $a_{i}$ is reliably fixed).

Formally, let $\theta_{i}$ denote the formulas defined in the proof of Theorem 5.25, and let $\xi_{\Phi}$ be the conjunction of the formulas

[TABLE]

where

[TABLE]

Again, $\Phi\mapsto\xi_{\Phi}$ is a logspace-computable mapping.

Claim 5.31.1

If $\Phi$ is true, then $\xi_{\Phi}$ is $\mathbf{K4}$-unifiable.

Proof:   Define the functions $F_{i}$ and $G_{i}$ as in Claim 5.25.1. Let $W=U_{\mathbf{K4}}\mathopen{(}q\mathclose{)}$; we will construct a valuation of the variable $x$ in $W$ as follows. Let $w\in W$. If $w\vDash\theta_{2i+2}$ for some $i<d$, let $a_{0}(w),\dots,a_{i}(w)\in\mathbf{2}$ be defined by

[TABLE]

Put b_{i}(w)=G_{i}\bigl{(}a_{0}(w),\dots,a_{i}(w)\bigr{)}, and define $w\vDash x^{b_{i}(w)}$. For other $w$, define $w\vDash x$ in an arbitrary way.

A similar argument as in Claim 5.31.1 shows that under this valuation, all points of $W$ satisfy (69) and (70). Thus, $\xi_{\Phi}$ is $\mathbf{K4}$-unifiable by [8, Thm. 5.18].     $\Box\hbox{ (Claim 5.31.1)}$

Claim 5.31.2

If $L$ has irreflexive depth at least $3d+1$, and $\xi_{\Phi}$ is $L$-unifiable, then $\Phi$ is true.

Proof:   Let us fix an $L$-frame $W$, and a subreduction $f$ from $W$ onto the irreflexive chain of length $3d+1$, whose elements we label as $c_{0}>c_{1}>\dots>c_{3d}$. We may assume that $W$ is rooted, and its root $r$ maps to $c_{3d}$. For any $i\leq 3d$, put $D_{i}=f^{-1}[c_{i}]$. The sets $D_{i}$ are pairwise disjoint admissible subsets of the frame $W$; each $D_{i}$ is a nonempty irreflexive antichain, and for each $i^{\prime}<i$, $D_{i^{\prime}}$ is a cover of $D_{i}$ (i.e., every element of $D_{i}$ sees some element of $D_{i^{\prime}}$). We have $D_{3d}=\{r\}$.

For each $a=\langle a_{0},\dots,a_{d-1}\rangle\in\mathbf{2}^{d}$, let $W_{a}$ denote the parametric frame for parameter $q$ based on $W$ such that

[TABLE]

It is straightforward to check that in $W_{a}$:

• •

For each $i<d$, points of $D_{3i+2}$ satisfy $\theta_{2i+1}$.

• •

Points of W\smallsetminus D_{1}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}} satisfy $\theta_{0}$, points of $D_{3d-1}\mathord{\downarrow}$ satisfy $\theta_{2d}$, and for each $0<i<d$, points of D_{3i-1}\mathord{\downarrow}\smallsetminus D_{3i+1}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}} satisfy $\theta_{2i}$. In particular, for each $i\leq d$, points of $D_{3i}$ satisfy $\theta_{2i}$.

• •

For each $i<d$, points of D_{3i+1}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}}\smallsetminus D_{3i+2}{\raise 6.94444pt\hbox to5.00002pt{\hss\vrule width=4.0pt,depth=0.4pt\hss}\kern-5.00002pt\hbox{\downarrow}} (which includes $D_{3i+1}$) satisfy $\theta_{2i}$ or $\theta_{2i+1}$ according to the value of $a_{i}$.

As a consequence, $W_{a}\vDash\gamma$: specifically, for any $i<d$, $W_{a}\vDash\theta_{2i+1}\to\Box\neg\theta_{2i+1}$ if $a_{i}=0$, and $W_{a}\vDash\theta_{2i+2}\to\Diamond(\theta_{2i+1}\land\Diamond\theta_{2i+1})$ if $a_{i}=1$.

Now, assume that $\xi_{\Phi}$ is $L$-unifiable, and let us fix a unifier $\sigma$ of $\xi_{\Phi}$ whose target formulas contain no variables, and no parameters save $q$. We define a function $G\colon\mathbf{2}^{d}\to\mathbf{2}^{d}$ as follows: given $a\in\mathbf{2}^{d}$, we have $W_{a}\vDash\sigma(\xi_{\Phi})$ as $\sigma$ is a unifier, and we know $W_{a}\vDash\gamma$, thus using (69), there is for each $i<d$ a unique $b_{i}\in\mathbf{2}$ such that $W_{a}\vDash\theta_{2i+2}\to\sigma(x)^{b_{i}}$. We put $G(a)=\langle b_{0},\dots,b_{d-1}\rangle$.

By the breakdown above, points $w\in D_{3i+3}$ satisfy $\theta_{2i+2}$ in $W_{a}$, and the valuation of $q$ in w{\lower 1.94443pt\hbox to5.00002pt{\hss\vrule width=4.0pt,height=0.4pt\hss}\kern-5.00002pt\hbox{\uparrow}} is determined by $a_{0},\dots,a_{i}$, hence so is the valuation of $\sigma(x)$. That is, $b_{i}$ only depends on $a_{0},\dots,a_{i}$: there are functions $G_{i}\colon\mathbf{2}^{i+1}\to\mathbf{2}$, $i<d$, such that

[TABLE]

for each $a\in\mathbf{2}^{d}$. Since $W_{a}\vDash\sigma(\xi_{\Phi})$, we have

[TABLE]

using (70). This makes $G_{0},\dots,G_{d-1}$ Skolem functions witnessing the truth of $\Phi$: formally, we may show

[TABLE]

by reverse induction on $i\leq d$, with $\Phi_{i}$ defined by (66).     $\Box\hbox{ (Claim 5.31.2)}$

The result now follows from Claims 5.31.1 and 5.31.2.     ∎

Corollary 5.32

Unifiability of formulas with $1$ parameter and $1$ variable is $\mathrm{PSPACE}$-hard in all consistent $\langle{\bullet},1\rangle$-extensible logics.     ∎

6 Conclusion

We have undertaken a thorough investigation of the complexity of admissibility and unifiability with parameters in transitive modal logics. In particular, we obtained a classification of these problems for cluster-extensible logics, a number of results for logics of bounded depth and width, and several very general lower bounds on hardness of unifiability in broad classes of transitive logics.

When we reflect on the effect of parameters on the complexity, one recurring observation is that the power of having an unlimited supply of parameters can be fully exploited only for logics that allow arbitrary large clusters, but in that case it blows up the complexity of unifiability to $\mathrm{coNEXP}$ (or from $\mathrm{NEXP}$ to $\Sigma^{\exp}_{2}$). This is perhaps most striking for $\mathbf{S5}$, which is at the same time one of the most fundamental and one of the most simple modal logics; the derivability problem for $\mathbf{S5}$ is $\mathrm{coNP}$-complete, and this also holds for parameter-free admissibility, or even admissibility with a constant number of parameters. However, $\mathbf{S5}$-unifiability with arbitrary parameters is $\mathrm{coNEXP}$-complete, i.e., exponentially harder.

A perhaps more intriguing effect is that already the addition of $1$–$2$ parameters may raise the complexity of unifiability from $\mathrm{NP}$ to $\mathrm{PSPACE}$ in logics of unbounded depth. Even better, we saw that for some logics such as $\mathbf{GL}$ or $\mathbf{D4}$, unifiability with $1$ parameter is $\mathrm{NEXP}$-complete, but parameter-free unifiability is $\mathrm{NP}$-complete, hence again we have an exponential blow-up. In these cases, the complexity of parameter-free unifiability is exceptionally low (e.g., parameter-free inadmissibility is already $\mathrm{NEXP}$-complete).

This brings us to one of the rough spots where our analysis is incomplete, even for clx logics: what is the complexity of parameter-free unifiability in nonlinear clx logics? There are some cases where it is $\mathrm{NEXP}$-complete (see Theorem 5.20), and some cases where it is $\mathrm{NP}$-complete (e.g., extensions of $\mathbf{GL}$ or $\mathbf{D4}$, as just mentioned), but we do not know where exactly is the dividing line, or even if there are cases of intermediate complexity.

In the regime with $O(1)$ parameters, our results are enough to settle the complexity for clx logics and some other logics of interest, nevertheless the results are far from satisfactory: the conditions used for the lower bounds have an ad hoc feeling to them, and are unlikely to be exhaustive. We suspect that a more comprehensive classification might be quite hard here.

Finally, in the regime with arbitrarily many parameters, our lower and upper bounds do not match for some interesting classes of logics that are nonlinear and of unbounded cluster size, but do not satisfy the hypothesis of Theorem 5.10. As we already mentioned in the introduction, this gap will be addressed in the sequel.

Acknowledgements

I want to thank the anonymous referee whose suggestions improved the presentation of the paper.

The research was supported by grant 19-05497S of GA ČR. The Institute of Mathematics of the Czech Academy of Sciences is supported by RVO: 67985840.