Complexity of Cubical Cofibration Logics I: coNP-Complete Examples

Rose, Robert; Licata, Daniel R.

doi:10.4230/LIPIcs.TYPES.2024.9

Complexity of Cubical Cofibration Logics I: $\mathrm{coNP}$ -Complete Examples

Robert Rose

Dept. of Mathematics & Computer Science, Wesleyan University, Middletown, CT, USA Daniel R. Licata

Dept. of Mathematics & Computer Science, Wesleyan University, Middletown, CT, USA

Abstract

We provide a comprehensive classification of the cofibration entailment problem, $\mathrm{COFENT}$ , for the cofibration logics of various cubical type theories in use today. The problem $\mathrm{COFENT}$ arose from the need of cubical proof assistants to automate reasoning about cubical complexes included in an $n$ -dimensional hypercube. Intuitively, it asks: given logical descriptions of two such complexes, is one a subcomplex of the other? We show that the common variants of $\mathrm{COFENT}$ are $\mathrm{coNP}$ -complete.

Keywords and phrases:

cubical sets, internal language, intuitionistic logic, dependent type theory, homotopy type theory, decision procedures

Funding:

Robert Rose: US Air Force Research Lab, FA-95502110009 and FA-95501510053

Daniel R. Licata: US Air Force Research Lab, FA-95502110009 and FA-95501510053

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Type theory

Funding:

This material is based upon work supported by the Air Force Office of Scientific Research under Grant No.FA9550-21-0009 (Tristan Nguyen, program manager). Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the Air Force Office of Scientific Research.

DOI:

10.4230/LIPIcs.TYPES.2024.9

Event:

30th International Conference on Types for Proofs and Programs (TYPES 2024)

Editors:

Rasmus Ejlers Møgelberg and Benno van den Berg

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

A well-known tool in topos theory for reasoning about a given topos is its Mitchell-Bénabou language [5] (or simply, its “language”), a formal abstraction of the topos as a typed (i.e., multi-sorted) first-order intuitionistic language with a fixed interpretation in that topos. Because the syntax of the Mitchell-Bénabou language is defined directly from the topos (e.g., the types of the logic are just the objects of the topos), this interpretation is nearly trivial: terms denote morphisms and are represented by syntax for certain categorical operations which produce morphisms, such as pairing or post-composition with a given morphism; formulas are, idiosyncratically, terms whose type is the subobject classifier of the topos (or a subobject thereof).

Proving or disproving that a topos has a given property expressed in the Mitchell-Bénabou language is greatly facilitated by the Kripke-Joyal semantics (or “sheaf semantics”, for a topos of sheaves), which provides a rigorous translation of arguments in this language to ordinary classical mathematics. The semantics has the familiar form of a Tarskian truth definition. (However, because the interpretation is fixed, the forcing relation is defined a priori in terms of this definition, and the semantics is presented as a theorem.)

This semantics affords a convenient point of departure for investigating the computability and complexity theoretic properties of formal first-order reasoning in a topos. Specifically, this area gives rise to generalizations of the model-checking problem. It is a rich area which has received relatively little attention.

1.1 Language fragments for cubical homotopy theory

One application of Mitchell-Bénabou language is to the homotopy theory of cubical sets, where by cubical set we mean a contravariant functor on a particular indexing category $\mathcal{C}$ (a “cube category”). The topos is the category of cubical sets which are sheaves for a given Grothendieck topology on $\mathcal{C}$ . In this paper, this topology is trivial: the toposes are presheaf toposes.

The language of a topos of cubical sets is expressive enough to define important homotopical structure: notably, to specify which morphisms of cubical sets qualify as maps of spaces (i.e., “fibrations”) and which maps of spaces further qualify as equivalences (i.e., “trivial fibrations”). This is usually achieved first by selecting a collection of subfunctors of representable functors (e.g., in the case of simplicial homotopy theory, a standard choice is the “horn inclusions”) and hence by taking a fibration to be a morphism $f$ for which any map from a select subfunctor inclusion to $f$ affords an extension to the base representable. Trivial fibrations have this extension property with respect to a larger selection of such subfunctors. These collections of subfunctors form the bases for generating classes of morphisms called, respectively, “trivial cofibrations” and “cofibrations”. Extension of maps along trivial cofibrations is the fundamental operation provided by homotopical structure.

While these extension properties are readily expressible in the language of the topos, a more restricted usage of the language may suffice in certain frameworks (e.g., homotopy type theory). For example, the language of the topos may be used just for the purposes of specifying cofibrations into representables and expressing their inclusion relation. Since cofibrations are classified by $\Omega$ , the inclusion relation is naturally expressed by entailment in the language. The sacrifice in expressivity brings significant computational benefits. In Section 3, we will define a number of such language fragments.

1.2 Applications for cubical type theory

Our interest in decision problems arising from the language of a topos indeed began with a practical need. A key component of a proof assistant we were designing would automatically decide formula entailment in a fragment of the language of a topos: namely, presheaves on the finite-product theory of distributive lattices, an important definitional variant of the category of cubical sets. Analogous decision procedures are core components in existing implementations of cubical type theories. For example, entailment in a fragment of the language of the topos of presheaves on the finite-product theory of De Morgan algebras is decided in the proof assistant Agda’s cubical mode, which is an implementation of the cubical type theory presented in [3]. Entailment in a fragment of the language of the topos of presheaves on the finite-product theory of bipointed sets is decided in the proof assistant cooltt, which is an implementation of the cubical type theory presented in [1]. Our original motivation began with investigating the feasibility of implementing the directed cubical type theory presented in [7], which is an adaptation of the directed simplicial type theory presented in [6].

2 Motivating examples

For the sake of intuition, we present some instances and non-instances of the decision problems of interest before launching into the technical development.

2.1 Cube boundary inclusion

Consider a 3-dimensional cube, with 8 corner points $(0,0,0),\dotsc,(1,1,1)$ . As a cubical set, it is modeled by a representable functor $\operatorname{Hom}(-,\operatorname{X}^{3})$ . The object $\operatorname{X}$ is a formal element which corresponds to a single dimension. The identity morphism on $\operatorname{X}$ corresponds to a variable $x_{1}$ along that dimension. Hence, the object $\operatorname{X}^{3}$ corresponds to three dimensions; and $x_{1}$ , $x_{2}$ and $x_{3}$ each correspond to a dimension in the given cube. Let us picture $x_{1}$ as varying from left to right; $x_{2}$ as varying bottom to top; and $x_{3}$ as varying from front to back.

By means of equations involving these variables and end points 0 and 1, we can describe certain parts of this cube. For example, the equation $(x_{1}=0)$ describes just the left face, and $(x_{1}=1)$ describes just the right face. We can combine these using $\lor$ to get exactly the left and the right faces: ${(x_{1}=0)\lor(x_{1}=1)}$ . The entire 2-dimensional boundary of the 3-cube is described by the formula

(x_{1}=0)\lor(x_{1}=1)\lor(x_{2}=0)\lor(x_{2}=1)\lor(x_{3}=0)\lor(x_{3}=1)

(1)

We can also describe the 1-dimensional edges of the 3-cube by combining formulas describing faces using $\land$ . For example, the top-front edge is described by the formula $(x_{2}=1)\land(x_{3}=0)$ . The 1-dimensional boundary of the 3-cube is described by the formula

	$\displaystyle\hskip 14.22636pt(x_{1}=0)\land(x_{2}=0)\hskip 5.69054pt\lor% \hskip 5.69054pt(x_{1}=0)\land(x_{2}=1)\hskip 5.69054pt\lor\hskip 5.69054pt(x_% {1}=0)\land(x_{3}=0)$
	$\displaystyle\lor\,\,(x_{1}=0)\land(x_{3}=1)\hskip 5.69054pt\lor\hskip 5.69054% pt(x_{1}=1)\land(x_{2}=0)\hskip 5.69054pt\lor\hskip 5.69054pt(x_{1}=1)\land(x_% {2}=1)$
	$\displaystyle\lor\,\,(x_{1}=1)\land(x_{3}=0)\hskip 5.69054pt\lor\hskip 5.69054% pt(x_{1}=1)\land(x_{3}=1)\hskip 5.69054pt\lor\hskip 5.69054pt(x_{2}=0)\land(x_% {3}=0)$
	$\displaystyle\lor\,\,(x_{2}=0)\land(x_{3}=1)\hskip 5.69054pt\lor\hskip 5.69054% pt(x_{2}=1)\land(x_{3}=0)\hskip 5.69054pt\lor\hskip 5.69054pt(x_{2}=1)\land(x_% {3}=1)$		(2)

(Recall that $\land$ has higher precedence than $\lor$ .)

Let $\phi_{1}$ be the formula (1), and let $\phi_{2}$ be the formula (2). Here are two queries for a decision problem: does $\phi_{1}$ entail $\phi_{2}$ ? or does $\phi_{2}$ entail $\phi_{1}$ ? Geometric intuition tells us no and yes. The internal language of the topos of cubical sets will also tell us this.

2.2 Simplex and pyramid

The last pair of problems are common to all of the cubical type theories mentioned in Section 1.2. We now present an example which, among the three, can be expressed only in the language fragment used in [7].

We just saw how to combine equations using $\land$ and $\lor$ to describe parts of a cube. It is also possible to combine variables directly to describe the minimum of two variables or the maximum of two variables. The notation is the same: $x_{1}\land x_{2}$ denotes the min of $x_{1}$ and $x_{2}$ , while $x_{1}\lor x_{2}$ denotes their max.

The 2-simplex below the diagonal from $(0,0)$ to $(1,1)$ of the solid square (2-cube) is described by $(x_{1}=x_{1}\lor x_{2})$ (or alternatively by $(x_{2}=x_{1}\land x_{2})$ ). The same formula can be used to describe part of the 3-cube: it is the wedge containing the right face and the bottom face. Similarly, $(x_{2}=x_{2}\lor x_{3})$ describes the wedge formed between the 2-simplices above the diagonal on the left and right faces. Combining the two wedges with $\land$ yields a 3-simplex:

(x_{1}=x_{1}\lor x_{2})\land(x_{2}=x_{2}\lor x_{3})

The pyramid whose apex is the corner point $(0,0,0)$ and whose base is the right face of the 3-cube is described by $(x_{1}=x_{1}\lor x_{2}\lor x_{3})$ . Thus, we have two more queries for a decision problem. Is this formula valid?

(x_{1}=x_{1}\lor x_{2})\land(x_{2}=x_{2}\lor x_{3})\hskip 2.84526pt\Rightarrow% \hskip 2.84526pt(x_{1}=x_{1}\lor x_{2}\lor x_{3})

(3)

Or this one?

(x_{1}=x_{1}\lor x_{2}\lor x_{3})\hskip 2.84526pt\Rightarrow\hskip 2.84526pt(x% _{1}=x_{1}\lor x_{2})\land(x_{2}=x_{2}\lor x_{3})

(4)

2.3 Example reduction

In what follows, we will show that the instances (2) $\Rightarrow$ (1), (1) $\Rightarrow$ (2), (3), and (4) may be decided by an efficient translation into second-order logic, where the problem of checking the truth of the corresponding formula in a suitable model is in the complexity class $\mathrm{coNP}$ . For example, the translation of (3) to second-order logic is

	$\displaystyle\forall R\,\big{(}$	$\displaystyle\chi_{3}\to\forall x\,(R(x)\to x_{1}=x_{1}\lor x_{2})\hskip 2.845% 26pt\land\hskip 2.84526pt\forall x\,(R(x)\to x_{2}=x_{2}\lor x_{3})$
		$\displaystyle\hskip 22.76219pt\to\forall x\,(R(x)\to x_{1}=x_{1}\lor x_{2}\lor x% _{3})\big{)}$

where $\chi_{3}$ is a formula encoding the constraint that ternary relations assigned to $R$ have minimal and maximal elements. The entailment (3) holds if and only if the formula above is true in the model $\mathcal{A}=(\{0,1\},0^{\mathcal{A}}=0,1^{\mathcal{A}}=1,\land^{\mathcal{A}}=% \min,\lor^{\mathcal{A}}=\max)$ .

The translation alone provides the core of a practical decision procedure. What remains is boilerplate and optimizations. The model-checking instance above may in turn be efficiently encoded in propositional logic and checked with a state-of-the-art $\mathrm{SAT}$ -solver. Alternatively, the model-checking instance may be handed almost as-is (after some lightweight wrangling) to an $\mathrm{SMT}$ -solver like z3 or to an answer-set programming system like clingo.

3 Decision problems

Because terms in the language of a topos are built directly from its morphisms, this language is not in general recursively enumerable, and is often a proper class. Thus, it may not be that the entire language of a topos can be encoded as a countable set of strings over a finite alphabet. In computability and complexity theory, however, decision problems are ordinarily framed as such. For example, in a sheaf topos, any set at all induces a sheaf, and hence a type in the language. But for the purposes of defining a conventional decision problem, we can reasonably expect to encode no more than a countable number of types.

Furthermore, because terms in the language of a topos are formal combinations of morphisms, morphism equality is reducible to term equality: in particular, if morphism equality is undecidable, so is term equality. In contrast, equality of instances of a conventional decision problem is efficiently reducible to equality of strings over a finite alphabet.

Hence, one straightforward strategy is simply to limit one’s focus to a suitable fragment of the language of the topos, and to define our decision problems relative to this fragment. To this end, we will next consider fragments which are “finitely presented” by formula languages.

3.1 Formula languages

Given a set $A$ , we will denote a generic element of $A^{m}$ by $a\in A^{m}$ where $a=(a_{1},\dotsc,a_{m})$ . We will extend this notational convention to variables, parameters, and terms: $x$ will denote an $m$ -tuple of variables $x=(x_{1},\dotsc,x_{m})$ ; and likewise for $\alpha=(\alpha_{1},\dotsc,\alpha_{m})$ and for $s=(s_{1},\dotsc,s_{m})$ . Annotations or constructors may be “broadcast” over an $m$ -tuple: for example, $\forall x\,\psi$ abbreviates $\forall x_{1}\,\dotsb\forall x_{m}\,\psi$ . The concatenation of a $k$ -tuple $a$ and an $m$ -tuple $b$ will be denoted by $a\,;b$ . We will freely omit parentheses when they may be inferred.

3.1.1 Types and terms

We will define a term language $T$ prior to the formula language in the conventional way. Fix a finite set $F$ of morphisms in $\mathcal{E}$ . The term types of the fragment are generated by the domains and codomains appearing in $F$ . The terms of the formula language will be the fragment of the language of the topos generated by the identity morphisms on term types under the term-forming operations corresponding to post-composition by morphisms $f\in F$ , post-composition by projections $\pi_{i}$ , and pairing [5, Section VI.5]. Thus, terms can be viewed as composable chains of tuples of morphisms, generated from a finite set of morphisms and projections. For any given domain type $S_{1}\times\dotsb\times S_{m}$ , we fix a variable set $\{x_{1},\dotsc,x_{m}\}$ where each $x_{i}$ is interpreted by the corresponding projection. We will refer to such a term language as finitely presented. Equality of terms (“syntactic equality”) is clearly efficient to decide.

3.1.2 Parameterized first-order formulas

We consider formulas with parameters, or metavariables. From the point of view of the language of the topos, parameters are just variables defined on a subobject of $\Omega$ . In addition to term types, the definition of the fragment includes a finite collection of subobjects $\Phi_{i}\subseteq\Omega$ . For convenience, we assume that formulas are given with domain in the form $S_{1}\times\dotsb\times S_{m}\times\Phi_{1}\times\dotsb\times\Phi_{k}$ . We fix a variable set $\{\alpha_{1},\alpha_{2},\dotsc\}$ where each $\alpha_{i}$ is interpreted by the corresponding projection from $\Phi_{i}$ .

Definition 1.

Let $T$ be a finitely presented term language. The corresponding language of formulas $L_{T,S\times\Phi}$ is inductively defined by:

	$\displaystyle\bot$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}$
	$\displaystyle\top$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}$
	$\displaystyle\alpha_{i}$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}\quad\text{% where }1\leq i\leq k$
	$\displaystyle(f=g)$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}\quad\text{% where }f,g:S\to R\in T\text{ for some }R\in\mathcal{E}$
	$\displaystyle\phi_{1}\land\phi_{2}$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}\quad\text{% for }\phi_{1},\phi_{2}\in L_{T,S\times\Phi}$
	$\displaystyle\phi_{2}\lor\phi_{2}$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}\quad\text{% for }\phi_{1},\phi_{2}\in L_{T,S\times\Phi}$
	$\displaystyle\phi_{2}\Rightarrow\phi_{2}$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}\quad\text{% for }\phi_{1},\phi_{2}\in L_{T,S\times\Phi}$
	$\displaystyle\exists x_{m+1}\,\psi$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}\quad\text{% for }\psi\in L_{T,S\times S_{m+1}\times\Phi}$
	$\displaystyle\forall x_{m+1}\,\psi$	$\displaystyle\hskip 2.84526pt\in\hskip 2.84526ptL_{T,S\times\Phi}\quad\text{% for }\psi\in L_{T,S\times S_{m+1}\times\Phi}$

We define the language $L_{T}=\bigcup_{S\times\Phi}L_{T,S\times\Phi}$ . For a given $\phi\in L_{T}$ denotes the set of subformulas of $\phi$ .

We will usually abbreviate $L_{T,S\times\Phi}$ to $L_{S}$ when $T$ and $\Phi$ are inferable from context or are arbitrary. When the term type language is generated by a single type, we will index $L$ by the length of $S$ instead.

3.2 Semantics

Our focus in this paper is on the problem of deciding when a formula in the language of the topos holds when interpreted “locally”. One way to make this concept precise is in terms of a forcing relation, which is the basis the sheaf semantics.

3.2.1 Forcing relation

For an object $C$ in a category $\mathcal{C}$ , $\operatorname{t}(C)$ will denote the sieve $\bigcup_{D\in\mathcal{C}}\operatorname{Hom}(D,C)$ . We first recall the definition of forcing in toposes of sheaves from [5, Section VI.7]:

Definition 2.

Let $\mathcal{E}$ be a topos of sheaves with indexing category $\mathcal{C}$ , and let $S\in\mathcal{E}$ . Let $\phi$ be a formula defined on $S$ in the language of $\mathcal{E}$ . Let $X\in\mathcal{C}$ , and let $s\in SX$ . The forcing relation is defined by

X\Vdash\phi\,(s)\hskip 11.38109pt\text{iff}\hskip 11.38109pts\in\{x\mid\phi(x)\}X

where

is a pullback square.

We will refer to the element $s\in SX$ in Definition 2 as a local assignment. When we say “ $X$ forces $\phi$ with local assignment $s$ ” we mean that $X\Vdash\phi\,(s)$ .

The forcing relation models a form of “truth definition”, which is attributed to Kripke and Joyal, and which we also call the sheaf semantics. Furthermore, the truth definition may be usefully refined in light of specific features of the topos of sheaves in question.

3.2.2 Presheaf semantics

Next we present the presheaf semantics for a language fragment $L$ (Definition 1). The following theorem is adapted from [5, Theorem VI.7.1]. It will be our main tool for proving the correctness of mapping reductions. We recall that for an element $s\in SX$ and a morphism $f:Y\to X$ , the restriction of $s$ along $f$ , denoted by $s\cdot f$ , is defined as $S(f)(s)$ .

Theorem 3.

Let $\mathcal{C}$ be a category, and let $\mathcal{E}$ be the topos of presheaves on $\mathcal{C}$ . Let $S=S_{1}\times\dotsb\times S_{m},S_{m+1}\in\mathcal{E}$ . Let $\Phi=\Phi_{1}\times\dotsb\times\Phi_{k}\in\mathcal{E}$ with each $\Phi_{i}\subseteq\Omega$ . Let $\phi_{1},\phi_{2}:S\times\Phi\to\Omega$ and $\psi:S\times S_{m+1}\times\Phi\to\Omega$ be formulas. Let $X\in\mathcal{C}$ , let $s\in SX$ , and let $h\in\Phi X$ .

$\blacktriangleright$ Remark 4.

We may extend Theorem 3 to formulas in the language of the topos of the form $\forall\alpha_{1}\,\dotsb\,\forall\alpha_{k}\,\phi$ where $\phi\in L$ and $k$ is the maximal parameter index in $\phi$ :

	$\displaystyle X\Vdash\forall\alpha_{1}\,\dotsb\,\forall\alpha_{k}\,\phi\,(s)$	$\displaystyle\hskip 14.22636pt\text{iff for all }Y\in\mathcal{C},t\in% \operatorname{Hom}(Y,X),\text{ and }h\in\Phi_{1}\times\dotsb\times\Phi_{k}Y,$
		$\displaystyle\hskip 25.60747ptY\Vdash\phi\,(s\cdot t\,;h)$

Corollary 5.

In the context of Theorem 3, the semantics of the universal quantifier when $S_{m+1}=\operatorname{Hom}_{\mathcal{C}}(-,U)$ for some $U\in\mathcal{C}$ and $\mathcal{C}$ is Cartesian validates the following equivalence:

X\Vdash\forall x_{m+1}\,(\psi_{1}\lor\psi_{2})\Leftrightarrow\forall x_{m+1}\,% \psi_{1}\lor\forall x_{m+1}\,\psi_{2}\,(x)

3.3 Languages of representable types

One natural way to obtain a finitely presented formula language is to restrict attention to sheaves of the form $S=\operatorname{Hom}(-,U)$ for a selection of $U\in\mathcal{C}$ . Elements of $S$ would just be morphisms in $\mathcal{C}$ from $X$ to $U$ . Thus, we may induce a formula language from a collection of morphisms from $\mathcal{C}$ .

Coincidentally, elements of $SX=\operatorname{Hom}(X,U)$ then have a compositional structure analogous to that induced by a formal term system. Below, this coincidence will be taken further: the indexing category $\mathcal{C}$ will be presented as a quotiented term language, and the term language defining $\mathcal{C}$ will take the place of the term language used to define the formula language. Conveniently, restrictions will then be computed by term substitution.

3.4 Indexing category from a finite algebra

The indexing categories for cubical sets – “cube categories” – are readily and usefully definable as quotients of formal term languages.

Beyond encodability, another requirement for bringing a decision problem under the purview of complexity theory is that it be decidable. But an indexing category $\mathcal{C}$ may fail to have decidable equality of morphisms; and so even validity of the atomic formulas of the language may fail to be decidable. The following method of construction however ensures that the morphisms of $\mathcal{C}$ at least have decidable equality.¹¹1We are grateful to Alex Kruckman for directing our attention to the central role played by finite algebras in this area. See also [2].

3.4.1 Generation by a finite algebra

Fix a finite algebraic signature $\sigma$ . Let $\mathcal{T}_{\sigma,n}$ be the term algebra of type $\sigma$ over the variable set $\{x_{1},\dots,x_{n}\}$ . We will abbreviate $\mathcal{T}_{\sigma,n}$ to $\mathcal{T}_{n}$ . For $m\geq 0$ , the $m$ -fold (left-associated) product algebra $\mathcal{T}_{n}\times\dotsb\times\mathcal{T}_{n}$ will be denoted by $\mathcal{T}^{m}_{n}$ . The term algebra $\mathcal{T}$ is defined by $\mathcal{T}=\bigcup_{n}\mathcal{T}_{n}$ .

For $s\in\mathcal{T}_{m}$ and $t\in\mathcal{T}^{m}_{n}$ , the simultaneous substitution of the terms $t_{i}$ for variables $x_{i}$ in $s$ will be denoted by $s[t_{1}/x_{1},\dotsc,t_{m}/x_{m}]$ , by $s[t/x]$ , or simply by $s t$ . Let $\mathcal{A}$ be a finite $\sigma$ -algebra. The equational theory of $\mathcal{A}$ contains the universally quantified equations of terms satisfied by $\mathcal{A}$ . The variety of this theory, denoted by $\operatorname{V}(\mathcal{A})$ , contains the $\sigma$ -algebras which satisfy this theory (i.e., its models). Examples of varieties generated by a finite algebra $\mathcal{A}$ include Boolean algebras, De Morgan algebras, (bounded) distributive lattices, (bounded) meet (join) semi-lattices, bi-pointed sets, pointed sets, and sets. All save Boolean algebras and sets have been used in the construction of indexing categories of cubical sets. Bounded distributive lattices have also been used to construct the indexing category in a variant definition of simplicial sets.

We may use the term algebra $\mathcal{T}_{n}$ to give a formal definition of a free algebra in $\operatorname{V}(\mathcal{A})$ generated by variables $x_{1},\dotsc,x_{n}$ . We will denote these algebras by $\mathcal{F}_{\mathcal{A},n}$ , or more briefly by $\mathcal{F}_{n}$ . Given terms $r,s\in\mathcal{T}_{n}$ , we say that $r$ and $s$ denote the same elements in $\mathcal{F}_{n}$ if and only if $r^{\mathcal{A}}=s^{\mathcal{A}}$ (i.e., their interpretation as term functions on $\mathcal{A}^{n}$ are equal). Recall that this relation respects term substitution: for $s\in\mathcal{T}_{m}$ and $t\in\mathcal{T}^{m}_{n}$ , $s[t/x]^{\mathcal{A}}=s^{\mathcal{A}}\circ t^{\mathcal{A}}$ .

3.4.2 Finite product theories

From here, we may use the free algebras $\mathcal{F}_{n}$ to give a formal definition of an indexing category $\mathcal{C}$ . We will denote these categories by $\mathcal{C}_{\mathcal{A}}$ , or more briefly by $\mathcal{C}$ . The object set of $\mathcal{C}_{\mathcal{A}}$ contains a formal object $\operatorname{X}$ , and its remaining objects are formal $n$ -fold (left-associated) products of $\operatorname{X}$ for $n\geq 0$ . The set of morphisms from $\operatorname{X}^{n}$ to $\operatorname{X}^{m}$ is simply the (left-associated) product algebra $\mathcal{F}^{m}_{n}$ . Thus, morphisms are denoted by $m$ -tuples of terms in $n$ -variables, and two morphisms denoted by tuples of terms $r$ and $s$ are equal if and only if their interpretations as term functions on $\mathcal{A}^{n}$ are equal. For $n\geq 0$ , the identity morphism on $\operatorname{X}^{n}$ is $(x_{1},\dotsc,x_{n})$ . Composition of morphisms is given by composition of denoted term functions; which factors through the substitution of the representing tuples of terms.

The category $\mathcal{C}_{\mathcal{A}}$ is an example of a finite-product theory (or Lawvere theory). A well-known alternative view of this construction is as the category opposite to a chosen skeleton of the category of free algebras on a finite number of generators and homomorphisms. Note however that the language of a topos is interpreted by contravariant functors on $\mathcal{C}_{\mathcal{A}}$ . This usage is different than the usage for which the concept of a finite-product theory was developed by Lawvere: the categorification of universal algebra. Models of this finite-product theory would be product-preserving functors on $\mathcal{C}_{\mathcal{A}}$ , not arbitrary functors on $\mathcal{C}_{\mathcal{A}}^{op}$ satisfying sheaf conditions.

3.5 Cofibration formulas

From now on, we will assume that the formula language $L$ is defined over a term algebra $\mathcal{T}$ corresponding to a finite algebra $\mathcal{A}$ which induces the indexing category $\mathcal{C}$ , and that the term translation is the natural one. The letter $c$ will denote a generic constant term in the signature of $\mathcal{A}$ .

Standard cofibration formulas (i.e., those used in cubical type theories) constitute only a small fragment of $L$ : specifically, the entailment connective $\Rightarrow$ and existential quantifier $\exists$ do not appear in cofibration formulas. Another restriction which appears concerns allowable atomic equations: in some cubical type theories, an equation may compare a given non-constant term $f$ only to a constant.

Definition 6.

We define several fragments of $L$ by inductive generation:

$\blacksquare$

$L_{\mathit{cof}}$ is generated by $\bot$ , $\top$ , $(f=g)$ , $\land$ , $\lor$ , and $\forall$
$\blacksquare$

$L_{\mathit{coftc}}$ is generated by $\bot$ , $\top$ , $(f=c)$ , $\land$ , $\lor$ , and $\forall$
$\blacksquare$

$L_{\mathit{cofvc}}$ is generated by $\bot$ , $\top$ , $(x_{i}=c)$ , $\land$ , $\lor$ , and $\forall$

Each fragment above also has a variant – $L_{\mathit{pcof}}$ , $L_{\mathit{pcoftc}}$ , $L_{\mathit{pcofvc}}$ – whose generators also contain $\alpha_{i}$ .

A formula in $L_{\mathit{cof}}$ is called a cofibration formula. The variants $L_{\mathit{coftc}}$ and $L_{\mathit{cofvc}}$ are called term-constant and variable-constant. The variants containing $\alpha_{i}$ are called parameterized. Although the focus of our study is on these fragments, it is natural to investigate related decision problems for the full language. In several cases, the methods we use below do apply more generally. In the future, the provisional definition above of what is a cofibration formula may merit revisiting.

3.6 Entailment problems

We are at last in position to define the decision problems we aim to classify in this paper.

Definition 7.

Let $\mathcal{A}$ be a finite algebra with signature $\sigma$ . Let $\mathcal{T}$ be the term algebra of type $\sigma$ over variable set $\{x_{1},x_{2},\dotsc\}$ , let $\mathcal{C}$ be the finite-product theory induced by $\mathcal{A}$ , and let $\operatorname{X}$ be the generating object of $\mathcal{C}$ . The cofibration entailment problem for $\mathcal{A}$ is the subset of $L_{\mathit{cof}}\times L_{\mathit{cof}}$ defined by

\mathrm{COFENT}=\big{\{}(\phi_{1},\phi_{2})\mid\exists m\,\operatorname{X}^{m}% \Vdash\phi_{1}\Rightarrow\phi_{2}\,(x)\big{\}}

The parameterized cofibration entailment problem for $\mathcal{A}$ and $\Phi$ is the subset of $L_{\mathit{pcof}}\times L_{\mathit{pcof}}$ defined by

\mathrm{PCOFENT}=\big{\{}(\phi_{1},\phi_{2})\mid\exists m\,\operatorname{X}^{m% }\Vdash\forall\alpha\,\big{(}\phi_{1}\Rightarrow\phi_{2}\big{)}\,(x)\big{\}}

Lastly, for algebras $\mathcal{A}$ with at least one constant, we denote the term-constant and variable-constant variants of each problem with the suffixes TC and VC.

3.7 Problem characterization in terms of derivability

Given the proof-theoretic character of many presentations of cubical type theories, it is reasonable to wonder if there is an alternative, logical characterization of $\mathrm{COFENT}$ . Is there a suitable notion of derivability such that $\mathrm{COFENT}=\{(\phi_{1},\phi_{2})\mid\phi_{1}\vdash\phi_{2}\}$ ?

For this discussion, let us consider the cube category corresponding to the theory of bounded distributive lattices. We know that the language of a topos can be viewed as an intuitionistic first-order logic. A natural first pass is intuitionistic derivability from this theory. This notion of derivability is sound with respect to the Kripke-Joyal semantics. Unsurprisingly, it is not complete. For example,

(x_{1}\land x_{2}=0)\Rightarrow(x_{1}=0)\lor(x_{2}=0)

is valid in the language of the topos; but a corresponding derivation does not exist (not even classically: consider the smallest congruence on the free distributive lattice on two generators which identifies the meet of the generators and 0). Another example is Corollary 5, which is certainly not derivable. The notion of derivability above, it seems, would need to be significantly augmented with axioms to accommodate the structural peculiarities of categories of cubical sets as well as semantic properties specific to the choice of generating algebra and of language fragment.

However, even given a complete axiomatization, we do not expect a notion of derivability to yield an efficient-enough decision procedure to prove our main results. In practice, where this approach has been made to work, it remains the case that the smallest-known derivability proofs may be exponential in the length of the given instance. So instead, we ask, what form might a “short witness” of $\phi_{1}\nvdash\phi_{2}$ take? The answer in logic traditionally has been a countermodel.

4 Results

To classify $\mathrm{COFENT}$ and related problems for various cube categories, we will first show uniformly that they are all $\mathrm{coNP}$ -hard by a reduction from the canonical $\mathrm{coNP}$ -hard problem $\mathrm{UNSAT}$ . Next we will show more-or-less on a case-by-case basis that they belong to $\mathrm{coNP}$ via efficient translations to the fragment of second-order logic $\forall$ SO. Here we rely on Fagin’s theorem, the foundational result in descriptive complexity theory (cf. [4, Section 9.2]). Note that the Cook-Levin theorem is an easy corollary of Fagin’s theorem, and its typical proof contains an efficient translation to $\mathrm{UNSAT}$ (ibid.); so these translations may also be viewed as indirect reductions to $\mathrm{UNSAT}$ .

4.1 Reduction from $\mathrm{UNSAT}$

Proposition 8.

If $\sigma_{0}$ has constants 0 and 1 denoting distinct elements of $\mathcal{A}$ , then the decision problem $\mathrm{COFENTVC}$ is $\mathrm{coNP}$ -hard.

Proof.

Let $F$ be a formula of propositional logic in disjunctive normal form. Assume wlog that $\operatorname{Var}(F)\subseteq\{x_{1},\dotsc,x_{m}\}$ . Let $F^{\prime}\in L_{\mathit{cof},m}$ be the formula induced by mapping positive literals $x_{i}$ to equations $(x_{i}=1)$ and negative literals to equations $(x_{i}=0)$ . The edge cases: empty clauses are mapped to $\top$ while empty formulas are mapped to $\bot$ . We claim that

F\in\mathrm{UNSAT}\hskip 11.38109pt\text{iff}\hskip 11.38109pt\operatorname{X}% ^{m}\Vdash F^{\prime}\Rightarrow\bot\,(x)

First, we prove the case where $F$ is a single clause $C$ . Suppose that $C$ is unsatisfiable. Then $C$ contains literals $x_{i}$ and $\lnot x_{i}$ for some $i$ . So $(x_{i}=1),(x_{i}=0)\in\operatorname{SF}(F^{\prime})$ . Let $s\in\mathcal{T}^{m}_{n}$ . Note that $\operatorname{X}^{n}\Vdash C\,(s)$ implies both $s_{i}=0$ and $s_{i}=1$ , which is a contradiction. So $\operatorname{X}^{n}\nVdash C\,(s)$ , as desired. Conversely, suppose that $C$ is satisfiable. Let $b\in\{0,1\}^{m}$ be a satisfying assignment (whereby $x_{i}\mapsto b_{i}$ ). Note that for $x_{i}\in\operatorname{Var}(C)$ , $b_{i}=0$ if and only if $C$ contains $\lnot x_{i}$ . Hence, for $x_{i}\in\operatorname{Var}(C)$ , $b_{i}=0$ if and only if $(x_{i}=0)\in\operatorname{SF}(C^{\prime})$ and $b_{i}=1$ if and only if $(x_{i}=1)\in\operatorname{SF}(C^{\prime})$ . Therefore, $\operatorname{X}^{0}\Vdash C^{\prime}\,(b)$ .

We finish with an induction on $F$ . If $F$ is the empty formula, then $F$ is unsatisfiable while $\operatorname{X}^{m}\Vdash\bot\Rightarrow\bot\,(x)$ . Now suppose $F=F_{1}\vee F_{2}$ . On the one hand, observe that $F_{1}\vee F_{2}$ is unsatisfiable if and only if $F_{1}$ and $F_{2}$ are unsatisfiable. On the other hand, $\operatorname{X}^{m}\Vdash F^{\prime}_{1}\vee F^{\prime}_{2}\Rightarrow\bot\,(x)$ if and only if $\operatorname{X}^{m}\Vdash F^{\prime}_{1}\Rightarrow\bot\,(x)$ and $\operatorname{X}^{m}\Vdash F^{\prime}_{2}\Rightarrow\bot\,(x)$ . The conclusion follows by induction. $\hfill\blacktriangleleft$

Corollary 9.

If $\sigma_{0}$ has constants 0 and 1 denoting distinct elements of $\mathcal{A}$ , then any of the decision problems defined in Definition 7 is $\mathrm{coNP}$ -hard.

4.2 Reduction to $\forall$ SO

4.2.1 Translation of $L_{\mathit{cof}}$ to second-order logic

Consider the equation $(f=g)\in L$ . We would like to transform this equation into the sentence $\forall x\,\big{(}R(x)\to f(x)=g(x)\big{)}$ . Informally, this sentence holds if the equation holds for all $m$ -tuples satisfying $R$ . Given $\phi\in L_{\mathit{cof}}$ , the purpose of the following transformation is to replace equations $(f=g)\in\operatorname{SF}(\phi)$ with such formulas.

Below, $\vDash$ denotes the conventional formula satisfaction relation from mathematical logic for second-order logic ([4, Section 7.1]). The term function interpreting a tuple of terms $s\in\mathcal{T}^{m}_{n}$ will be denoted by $s^{\mathcal{A}}:\mathcal{A}^{n}\to\mathcal{A}^{m}$ .

Definition 10.

Let $m,n\geq 0$ , and let $\phi\in L_{\mathit{cof},m}$ . We define the second-order formula $\phi^{\prime}_{n}$ with a free second-order variable $R$ of arity $n$ as follows:

\phi^{\prime}_{n}=\begin{cases}\bot&\phi=\bot\\ \top&\phi=\top\\ \forall x\,\big{(}R(x)\to f(x)=g(x)\big{)}&\phi=(f=g)\\ \phi^{\prime}_{1,n}\land\phi^{\prime}_{2,n}&\phi=\phi_{1}\land\phi_{2}\\ \phi^{\prime}_{1,n}\lor\phi^{\prime}_{2,n}&\phi=\phi_{1}\lor\phi_{2}\\ \forall x_{m+1}\,\psi^{\prime}_{n}&\phi=\forall x_{m+1}\,\psi\end{cases}

When $n=m$ , we will abbreviate $\phi^{\prime}_{n}$ to $\phi^{\prime}$ . Note that $\phi^{\prime}$ has no free first-order variables.

$\blacktriangleright$ Remark 11.

The transformation in Definition 10 admits a reduction of the universal quantifier:

\mathcal{A}\vDash\forall x_{m+1}\,\psi^{\prime}_{m}\,(M)\hskip 11.38109pt\text% {iff}\hskip 11.38109pt\mathcal{A}\vDash\psi^{\prime}_{m+1}\,(M\times\mathcal{A})

4.2.2 First schema

As it turns out, if a formula in the fragment $L_{\mathit{cof}}$ is forced by a given index with local assignment $s$ , it is forced by any other index and local assignment provided it has the same term-functional image as $s$ . We now present a reduction schema which takes advantage of this fact to obtain a bound on the number of tuples of terms which must be considered to force an entailment.

Lemma 12 (Term image invariance).

Let $\phi\in L_{\mathit{cof},m}$ . Let $s\in\mathcal{T}^{m}_{n}$ and let $t\in\mathcal{T}^{m}_{p}$ . If $\operatorname{img}(s^{\mathcal{A}})=\operatorname{img}(t^{\mathcal{A}})$ and $\operatorname{X}^{n}\Vdash\phi\,(s)$ , then $\operatorname{X}^{p}\Vdash\phi\,(t)$ .

Proof.

Induction on $\phi$ . The only interesting case is when $\phi=(f=g)$ . Then it suffices to prove that if $fs^{\mathcal{A}}=gs^{\mathcal{A}}$ , then $ft^{\mathcal{A}}=gt^{\mathcal{A}}$ . Let $a\in\mathcal{A}^{p}$ . By assumption, there exists $b\in\mathcal{A}^{n}$ such that $s^{\mathcal{A}}(b)=t^{\mathcal{A}}(a)$ . But then

ft^{\mathcal{A}}(a)\hskip 5.69054pt=\hskip 5.69054ptfs^{\mathcal{A}}(b)\hskip 5% .69054pt=\hskip 5.69054ptgs^{\mathcal{A}}(b)\hskip 5.69054pt=\hskip 5.69054% ptgt^{\mathcal{A}}(a)\

$\hfill\blacktriangleleft$

As a consequence, forcing of a cofibration formula $\phi$ with a local assignment $s$ is reducible to checking that $\phi^{\prime}$ holds with respect to the term-functional image of $s$ given an assignment to the second-order variable $R$ .

Lemma 13.

Let $m,n\geq 0$ , let $\phi\in L_{\mathit{cof},m}$ , and let $s\in\mathcal{T}^{m}_{n}$ . Let $M=\operatorname{img}(s^{\mathcal{A}})$ . Then

X^{n}\Vdash\phi\,(s)\hskip 11.38109pt\text{iff}\hskip 11.38109pt\mathcal{A}% \vDash\phi^{\prime}(M)

Proof.

Induction on $\phi$ . We omit the cases which follow directly by induction.

$\blacksquare$

Suppose $\phi=\bot$ or $\phi=\top$ . Immediate.
$\blacksquare$

Suppose $\phi=(f=g)$ . Fix $a\in\mathcal{A}^{m}$ , and suppose that $a\in M$ . Let $b\in\mathcal{A}^{n}$ satisfy $s^{\mathcal{A}}(b)=a$ . By assumption, $X^{n}\Vdash(f=g)\,(s)$ , and so $fs^{\mathcal{A}}=gs^{\mathcal{A}}$ . Hence $f^{\mathcal{A}}(a)=fs^{\mathcal{A}}(b)=gs^{\mathcal{A}}(b)=g^{\mathcal{A}}(a)$ .

For the converse, we need to show that $fs^{\mathcal{A}}=gs^{\mathcal{A}}$ . Fix $b\in\mathcal{A}^{n}$ . Because $s^{\mathcal{A}}(b)\in M$ , $fs^{\mathcal{A}}(b)=gs^{\mathcal{A}}(b)$ by assumption.
$\blacksquare$

Suppose $\phi=\forall x_{m+1}\,\psi$ . Recall that $\operatorname{X}^{n}\Vdash\forall x_{m+1}\,\psi\,(s)$ if and only if $\operatorname{X}^{n+1}\Vdash\psi\,(s,x_{n+1})$ ; while the induction hypothesis is that

$X^{n+1}\Vdash\psi\,(s,x_{n+1})\hskip 11.38109pt\text{iff}\hskip 11.38109pt% \mathcal{A}\vDash\psi^{\prime}_{m+1}(M\times\mathcal{A})$

The conclusion follows by Remark 11.

$\hfill\blacktriangleleft$

In the event that the cofibration $\phi$ is a conjunction of atomic formulas, we can dispense with the translation (Definition 10) altogether:

Corollary 14.

Let $m,n\geq 0$ , and let $\phi\in L_{\mathit{cof},m}$ be a conjunction of atomic formulas. Let $s\in\mathcal{T}^{m}_{n}$ , and let $M=\operatorname{img}(s^{\mathcal{A}})$ . Then

X^{n}\Vdash\phi\,(s)\hskip 11.38109pt\text{iff}\hskip 11.38109pt\text{for all % }a\in M,\mathcal{A}\vDash\phi(a)

To extend the translation (Definition 10) of formulas to entailment instances, we must reduce the quantification over all $m$ -tuples of terms. Term image invariance allows us to reduce this to quantification over all term-functional images included by $\mathcal{A}^{m}$ . Whence stems the decidability of the problem as well as its inefficiency. Notice that while belonging to a term-functional image of a given $s\in\mathcal{T}^{m}$ defines an $m$ -ary relation over $\mathcal{A}$ , being a term-functional image defines a property of $m$ -ary relations over $\mathcal{A}$ , one which we may try to capture by a second-order formula:

Definition 15.

Let $m\geq 0$ . Let $\chi_{m}$ be a formula in the second-order language over the signature of $\mathcal{A}$ whose only free variable is the second-order variable $R$ with arity $m$ . We say that $\chi_{m}$ characterizes images for $\mathcal{A}$ -term functions whenever the following conditions are equivalent for all $M\subseteq\mathcal{A}^{m}$ :

1.

$\mathcal{A}\vDash\chi_{m}\,(M)$
2.

there exist $n\geq 0$ and $s\in\mathcal{T}^{m}_{n}$ such that $M=\operatorname{img}(s^{\mathcal{A}})$

Indeed, a second-order characterization of term-functional images is all that is needed for this reduction schema.

Theorem 16.

Let $m\geq 0$ , let $\phi_{1},\phi_{2}\in L_{\mathit{cof},m}$ . Let $\chi_{m}$ be a formula which characterizes images for $\mathcal{A}$ -term functions. Then

\operatorname{X}^{m}\Vdash\phi_{1}\Rightarrow\phi_{2}\,(x)\hskip 11.38109pt% \text{iff}\hskip 11.38109pt\mathcal{A}\vDash\forall R\,\big{(}\chi_{m}\to\phi^% {\prime}_{1}\to\phi^{\prime}_{2}\big{)}

Proof.

Fix $M\subseteq\mathcal{A}^{m}$ and $a\in\mathcal{A}^{m}$ . Suppose that $\mathcal{A}\vDash\chi_{m}\,(M)$ . Fix $n\geq 0$ and $s\in\mathcal{T}^{m}_{n}$ according to Definition 15. Specializing the assumption, we have that $\operatorname{X}^{n}\Vdash\phi_{1}\,(s)$ implies $\operatorname{X}^{n}\Vdash\phi_{2}\,(s)$ . Hence, by Lemma 13, we have that $\mathcal{A}\vDash\phi^{\prime}_{1}\,(M)$ implies $\mathcal{A}\vDash\phi^{\prime}_{2}\,(M)$ .

For the converse, fix $n\geq 0$ and $s\in\mathcal{T}^{m}_{n}$ . Let $M=\operatorname{img}(s^{\mathcal{A}})$ . According to Definition 15, we have that $\mathcal{A}\vDash\chi_{m}\,(M)$ . And by assumption, $\mathcal{A}\vDash\phi^{\prime}_{1}\,(M)$ implies $\mathcal{A}\vDash\phi^{\prime}_{2}\,(M)$ . So, by Lemma 13, $\operatorname{X}^{n}\Vdash\phi^{\prime}_{1}\,(s)$ implies $\operatorname{X}^{n}\Vdash\phi^{\prime}_{2}\,(s)$ . $\hfill\blacktriangleleft$

4.2.3 Second schema

We will now present a reduction schema which applies to generating algebras with language fragments which have the property of local factorization (Definition 17). To abstract over the choice of language fragment, we let the variable $\gamma$ denote a generic element of $\{\mathit{cof},\mathit{coftc},\mathit{cofvc}\}$ .

Definition 17.

Let $m\geq 0$ . A formula $\rho\in L_{\gamma,m}$ is locally prime if $\rho$ does not entail $\bot$ , and for all $\phi_{1},\phi_{2}\in L_{\gamma,m}$ , if $\rho$ entails $\phi_{1}\lor\phi_{2}$ , then either $\rho$ entails $\phi_{1}$ or $\rho$ entails $\phi_{2}$ . An algebra $\mathcal{A}$ paired with a language fragment $L_{\gamma}$ has local factorization if for all $m$ and formulas $\phi\in L_{\gamma,m}$ , $\phi$ is equivalent to the disjunction (in $L_{\gamma,m}$ ) of locally prime formulas which entail $\phi$ .

We assume for the remainder of this section that $(\mathcal{A},L_{\gamma})$ has local factorization.

Lemma 18.

Let $m\geq 0$ , and let $\phi,\rho\in L_{\gamma,m}$ . Let ${M=\{a\in\mathcal{A}^{m}\mid\mathcal{A}\vDash\rho\,(a)\}}$ . Assume that for all terms $f,g\in\mathcal{T}_{m}$ ,

\operatorname{X}^{m}\Vdash\rho\Rightarrow(f=g)\,(x)\hskip 11.38109pt\text{iff}% \hskip 11.38109pt\mathcal{A}\vDash(f=g)^{\prime}\,(M)

If $\rho$ is locally prime, then

\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi\,(x)\hskip 11.38109pt\text{iff}% \hskip 11.38109pt\mathcal{A}\vDash\phi^{\prime}\,(M)

Proof.

Induction on $\phi$ .

$\blacksquare$

Suppose $\phi=\bot$ or $\phi=\top$ . Trivial.
$\blacksquare$

Suppose $\phi=(f=g)$ . By assumption.
$\blacksquare$

Suppose $\phi=\phi_{1}\land\phi_{2}$ . Directly by induction.
$\blacksquare$

Suppose $\phi=\phi_{1}\lor\phi_{2}$ . Suppose that $\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi_{1}\lor\phi_{2}\,(x)$ . Because $\rho$ is $\lor$ -prime, either $\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi_{1}\,(x)$ or $\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi_{2}\,(x)$ . The conclusion follows by induction. The converse also follows directly by induction.
$\blacksquare$

Suppose $\phi=\forall x_{m+1}\,\psi$ . Recall that $\operatorname{X}^{m}\Vdash\rho\Rightarrow\forall x_{m+1}\,\psi\,(x)$ if and only if $\operatorname{X}^{m+1}\Vdash\rho\Rightarrow\psi\,(x)$ ; while the induction hypothesis is that

$X^{n+1}\Vdash\rho\Rightarrow\psi\,(x)\hskip 11.38109pt\text{iff}\hskip 11.3810% 9pt\mathcal{A}\vDash\psi^{\prime}_{m+1}(M\times\mathcal{A})$

The conclusion follows by Remark 11.

$\hfill\blacktriangleleft$

Lemma 19.

Let $m\geq 0$ , and let $\phi_{1},\phi_{2}\in L_{\gamma,m}$ . Let $P$ be the set of locally prime formulas in $L_{\gamma,m}$ . Then

	$\displaystyle\operatorname{X}^{m}\Vdash\phi_{1}\Rightarrow\phi_{2}\,(x)\hskip 1% 1.38109pt\text{iff}\hskip 11.38109pt$
	$\displaystyle\text{for all }\rho\in P,\;\operatorname{X}^{m}\Vdash\rho% \Rightarrow\phi_{1}\,(x)\text{ implies }\operatorname{X}^{m}\Vdash\rho% \Rightarrow\phi_{2}\,(x)$

Proof.

The forward direction follows directly by the semantics. For the converse, let $s\in\mathcal{T}^{m}_{n}$ and suppose that $\operatorname{X}^{n}\Vdash\phi_{1}\,(s)$ . Let $P^{\prime}=\{\rho\in P\mid\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi_{1}\,(% x)\}$ . From local factorization, we have

\operatorname{X}^{m}\Vdash\phi_{1}\Leftrightarrow\bigvee_{\rho\in P^{\prime}}% \rho\,(x)

Fix $\rho\in P^{\prime}$ such that $\operatorname{X}^{n}\Vdash\rho\,(s)$ . By definition of $P^{\prime}$ and hypothesis, $\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi_{2}\,(x)$ . In particular, $\operatorname{X}^{m}\Vdash\phi_{2}\,(s)$ . $\hfill\blacktriangleleft$

Definition 20.

Let $m\geq 0$ . Let $P$ be the set of locally prime formulas in $L_{\gamma,m}$ . Let $\chi_{m}$ be a formula in the second-order language over the signature of $\mathcal{A}$ whose only free variable is the second-order variable $R$ with arity $m$ . We say that $\chi_{m}$ defines $P$ (the locally prime formulas in $L_{\gamma,m}$ ) when the following are equivalent for all $M\subseteq\mathcal{A}^{m}$ :

$\blacksquare$

$\mathcal{A}\vDash\chi_{m}\,(M)$
$\blacksquare$

there exists $\rho\in P$ such that $M=\{a\in\mathcal{A}^{m}\mid\mathcal{A}\vDash\rho\,(a)\}$

Theorem 21.

Let $m\geq 0$ , and let $\phi_{1},\phi_{2}\in L_{\gamma,m}$ . Let $P$ be the set of locally prime formulas in $L_{\gamma,m}$ . Let the formula $\chi_{m}$ define $P$ (Definition 20). If for all $\rho\in P$ , and for all terms $f,g\in\mathcal{T}_{m}$ ,

\operatorname{X}^{m}\Vdash\rho\Rightarrow(f=g)\,(x)\hskip 11.38109pt\text{iff}% \hskip 11.38109pt\mathcal{A}\vDash(f=g)^{\prime}\,(M)

then

\operatorname{X}^{m}\Vdash\phi_{1}\Rightarrow\phi_{2}\,(x)\hskip 11.38109pt% \text{iff}\hskip 11.38109pt\mathcal{A}\vDash\forall R\,(\chi_{m}\to\phi^{% \prime}_{1}\to\phi^{\prime}_{2})

Proof.

By Lemma 19, it suffices to show that

	$\displaystyle\text{for all }\rho\in P,\;\operatorname{X}^{m}\Vdash\rho% \Rightarrow\phi_{1}\,(x)\text{ implies }\operatorname{X}^{m}\Vdash\rho% \Rightarrow\phi_{2}\,(x)$
	$\displaystyle\text{iff}\hskip 11.38109pt\mathcal{A}\vDash\forall R\,(\chi_{m}% \to\phi^{\prime}_{1}\to\phi^{\prime}_{2})$

Let $M\subseteq\mathcal{A}^{m}$ , and suppose that $\mathcal{A}\vDash\chi_{m}\,(M)$ and $\mathcal{A}\vDash\phi^{\prime}_{1}\,(M)$ . Then, by Lemma 18, there exists $\rho\in P$ such that $\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi_{1}\,(x)$ ; and by assumption, $\mathcal{A}\vDash\phi^{\prime}_{2}\,(M)$ .

For the converse, suppose $\rho\in P$ , and that $\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi_{1}\,(x)$ . Let $M=\{a\in\mathcal{A}^{m}\mid\mathcal{A}\vDash\rho\,(a)\}$ . Then $\mathcal{A}\vDash\chi_{m}\,(M)$ , and by Lemma 18, $\mathcal{A}\vDash\phi^{\prime}_{1}\,(M)$ ; and by assumption, $\operatorname{X}^{m}\Vdash\rho\Rightarrow\phi_{2}\,(x)$ . $\hfill\blacktriangleleft$

4.3 Parameter elimination

In this section we will prove the following proposition, which will allow us to transport a classification of $\mathrm{COFENT}$ to $\mathrm{PCOFENT}$ :

Proposition 22.

There exist efficient mapping reductions from $\mathrm{PCOFENT}$ to $\mathrm{COFENT}$ , from $\mathrm{PCOFENTTC}$ to $\mathrm{COFENTTC}$ , and from $\mathrm{PCOFENTVC}$ to $\mathrm{COFENTVC}$ .

Proof.

Corollaries 24 and 29 $\hfill\blacktriangleleft$

For the remainder of this subsection, let $\operatorname{B}\subseteq\Omega$ be defined by $\operatorname{B}C=\{\emptyset,\operatorname{t}(C)\}$ for all $C\in\mathcal{C}$ . Let $\Phi$ be an arbitrary subobject satisfying the constraint $\operatorname{B}\subseteq\Phi\subseteq\Omega$ .

4.3.1 Bivalent parameters

Lemma 23.

Let $\phi\in L_{\mathit{pcof},m}$ . Let $k$ be the maximal parameter index of $\phi$ . Let $n\geq 0$ , let $s\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{n},\operatorname{X}^{m})$ , and let $h\in\Phi\operatorname{X}^{n}$ . Define $b_{h}\in\operatorname{B}^{k}\operatorname{X}^{n}$ by

b_{h,i}=\begin{cases}h_{i}&h_{i}=\operatorname{t}(\operatorname{X}^{n})\\ \emptyset&\text{otherwise}\end{cases}

Then $\operatorname{X}^{n}\Vdash\phi\,(s\,;b_{h})$ if and only if $\operatorname{X}^{n}\Vdash\phi\,(s\,;h)$ .

Proof.

Induction on $\phi$ . When $\phi=\alpha_{i}$ , we have

	$\displaystyle\operatorname{X}^{n}\Vdash\alpha_{i}\,(s\,;b_{h})$	$\displaystyle\hskip 11.38109pt\text{iff}\hskip 11.38109ptb_{h,i}=\operatorname% {t}(\operatorname{X}^{n})$
		$\displaystyle\hskip 11.38109pt\text{iff}\hskip 11.38109pth_{i}=\operatorname{t% }(\operatorname{X}^{n})$
		$\displaystyle\hskip 11.38109pt\text{iff}\hskip 11.38109pt\operatorname{X}^{n}% \Vdash\alpha_{i}\,(s\,;h)$

When $\phi$ is otherwise atomic, then $\operatorname{X}^{n}\Vdash\phi\,(s\,;b_{h})$ if and only if $\operatorname{X}^{n}\Vdash\phi\,(s)$ ; and likewise for $\operatorname{X}^{n}\Vdash\phi\,(s\,;h)$ . The induction cases are straightforward. $\hfill\blacktriangleleft$

Corollary 24.

Let $\phi_{1},\phi_{2}\in L_{\mathit{pcof},m}$ . Let $k$ be the maximal parameter index of $\phi_{1}\Rightarrow\phi_{2}$ . Then

\operatorname{X}^{m}\Vdash\forall\alpha^{\Phi}\,\big{(}\phi_{1}\Rightarrow\phi% _{2}\big{)}\,(x)\hskip 11.38109pt\text{iff}\hskip 11.38109pt\operatorname{X}^{% m}\Vdash\forall\alpha^{B}\,\big{(}\phi_{1}\Rightarrow\phi_{2}\big{)}\,(x)

Proof.

The forward direction is trivial. For the converse, fix $n\geq 0$ , $s\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{n},\operatorname{X}^{m})$ , and $h\in\Phi^{k}\operatorname{X}^{n}$ . Our goal is to show that $\operatorname{X}^{n}\Vdash\phi_{1}\Rightarrow\phi_{2}\,(s\,;h)$ . Hence, fix $p\geq 0$ and $t\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{p},\operatorname{X}^{n})$ , and suppose that $\operatorname{X}^{p}\Vdash\phi_{1}\,(st\,;f\cdot t)$ . We must show that $\operatorname{X}^{p}\Vdash\phi_{2}\,(st\,;f\cdot t)$ . By Lemma 23, it suffices to check that $\operatorname{X}^{p}\Vdash\phi_{2}\,(st\,;b_{f\cdot t})$ ; and by assumption, that $\operatorname{X}^{p}\Vdash\phi_{1}\,(st\,;b_{f\cdot t})$ ; which follows again from Lemma 23. $\hfill\blacktriangleleft$

4.3.2 Formula lifting

Next we introduce a piece of technical machinery to weaken a formula in $L_{m}$ : that is, add to the list of available free variables, irrespective of their non-occurrence. Because variables are bound in order of decreasing index, dummy free variables should be inserted before existing variables.

Definition 25.

Let $l,m\geq 0$ , and let $\phi\in L_{m}$ . We define $\operatorname{lift}_{l,m}:L_{m}\to L_{l+m}$ by

\operatorname{lift}_{l,m}(\phi)=\begin{cases}\bot&\phi=\bot\\ \top&\phi=\top\\ (f=g)[x_{l+1}/x_{1},\dotsc,x_{l+m}/x_{m}]&\phi=(f=g)\\ \alpha_{i}&\phi=\alpha_{i}\\ \operatorname{lift}_{l,m}(\phi_{1})\land\operatorname{lift}_{l,m}(\phi_{2})&% \phi=\phi_{1}\land\phi_{2}\\ \operatorname{lift}_{l,m}(\phi_{1})\lor\operatorname{lift}_{l,m}(\phi_{2})&% \phi=\phi_{1}\lor\phi_{2}\\ \operatorname{lift}_{l,m}(\phi_{1})\Rightarrow\operatorname{lift}_{l,m}(\phi_{% 2})&\phi=\phi_{1}\Rightarrow\phi_{2}\\ \exists x_{l+m+1}\,\operatorname{lift}_{l,m+1}(\psi)&\phi=\exists x_{m+1}\,% \psi\\ \forall x_{l+m+1}\,\operatorname{lift}_{l,m+1}(\psi)&\phi=\forall x_{m+1}\,% \psi\end{cases}

Proposition 26.

Let $k,l,m\geq 0$ . Let $\phi\in L_{m}$ with maximal index $k$ . Let $\Phi=\Phi_{1}\times\dotsb\times\Phi_{k}$ , where $\Phi_{i}\subseteq\Omega$ for all $i$ . Let $R=R_{1}\times\dotsb\times R_{l}$ and let $S=S_{1}\times\dotsb\times S_{m}$ . Let $X\in\mathcal{C}$ , let $h\in\Phi X$ , let $r\in RX$ , and let $s\in SX$ . Then $X\Vdash\phi\,(s\,;h)$ if and only if $X\Vdash\operatorname{lift}(\phi)\,(r\,;s\,;h)$ .

4.3.3 Grounding

In Lemmas 27, 28, and 29 below, given $k\geq 0$ , let $\epsilon\in L^{k}_{2k}$ be the $k$ -tuple of equations defined so that $\epsilon_{i}=(x_{i}=x_{k+i})$ .

Lemma 27.

Let $\phi\in L_{\mathit{pcof},m}$ . Let $k$ be the maximal parameter index of $\phi$ . Let $n,p\geq 0$ , let $s\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{n},\operatorname{X}^{m})$ , and let $t\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{p},\operatorname{X}^{k+% n})$ . Define $b_{t}\in\operatorname{B}^{k}\operatorname{X}^{p}$ by

b_{t,i}=\begin{cases}\operatorname{t}(\operatorname{X}^{p})&t_{i}=1\\ \emptyset&\text{otherwise}\end{cases}

The following are equivalent:

$\blacksquare$

$\operatorname{X}^{p}\Vdash\phi\,(s(t_{k+1},\dotsc,t_{k+n})\,;b_{t})$
$\blacksquare$

$\operatorname{X}^{p}\Vdash\operatorname{lift}(\phi)\big{[}\epsilon/\alpha\big{% ]}\,(t_{1},\dotsc,t_{k}\,;1,\dotsc,1\,;s(t_{k+1},\dotsc,t_{k+n}))$

Proof.

Induction on $\phi$ . When $\phi=\alpha_{i}$ , we have

	$\displaystyle\operatorname{X}^{p}\Vdash\alpha_{i}\,(s(t_{k+1},\dotsc,t_{k+n})% \,;b_{t})$
	$\displaystyle\text{iff }b_{t,i}=\operatorname{t}(\operatorname{X}^{n})$
	$\displaystyle\text{iff }t_{i}=1$
	$\displaystyle\text{iff }\operatorname{X}^{p}\Vdash(x_{i}=x_{k+i})\,(t_{1},% \dotsc,t_{k}\,;1,\dotsc,1\,;s(t_{k+1},\dotsc,t_{k+n}))$

When $\phi$ is otherwise atomic, then

\operatorname{X}^{p}\Vdash\phi\,(s(t_{k+1},\dotsc,t_{k+n})\,;b_{t})\hskip 11.3% 8109pt\text{iff}\hskip 11.38109pt\operatorname{X}^{p}\Vdash\phi\,(s(t_{k+1},% \dotsc,t_{k+n}))

This holds, by Proposition 26, if and only if

\operatorname{X}^{p}\Vdash\operatorname{lift}(\phi)\big{[}\epsilon/\alpha\big{% ]}\,(t_{1},\dotsc,t_{k}\,;1,\dotsc,1\,;s(t_{k+1},\dotsc,t_{k+n}))

The induction cases are straightforward. $\hfill\blacktriangleleft$

Lemma 28.

Let $\phi\in L_{\mathit{pcof},m}$ . Let $k$ be the maximal parameter index of $\phi$ . Let $n\geq 0$ , let $s\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{n},\operatorname{X}^{m})$ , and let $b\in\operatorname{B}^{k}\operatorname{X}^{n}$ . Define $a_{b}\in\operatorname{B}^{k}\operatorname{X}^{n}$ by

a_{b,i}=\begin{cases}1&b_{i}=\operatorname{t}(\operatorname{X}^{n})\\ 0&\text{otherwise}\end{cases}

Then

\operatorname{X}^{n}\Vdash\phi\,(s\,;b)\hskip 11.38109pt\text{iff}\hskip 11.38% 109pt\operatorname{X}^{n}\Vdash\operatorname{lift}(\phi)\big{[}\epsilon/\alpha% \big{]}\,(a_{b}\,;1,\dotsc,1\,;s)

Proof.

Induction on $\phi$ . When $\phi=\alpha_{i}$ , we have

	$\displaystyle\operatorname{X}^{n}\Vdash\alpha_{i}\,(s\,;b)$	$\displaystyle\hskip 11.38109pt\text{iff}\hskip 11.38109ptb_{i}=\operatorname{t% }(\operatorname{X}^{n})$
		$\displaystyle\hskip 11.38109pt\text{iff}\hskip 11.38109pta_{b,i}=1$
		$\displaystyle\hskip 11.38109pt\text{iff}\hskip 11.38109pt\operatorname{X}^{n}% \Vdash(x_{i}=x_{k+i})\,(a_{b}\,;1,\dotsc,1\,;s)$

When $\phi$ is otherwise atomic, then $\operatorname{X}^{n}\Vdash\phi\,(s\,;b)$ if and only if $\operatorname{X}^{n}\Vdash\phi\,(s)$ ; which holds, by Proposition 26, if and only if $\operatorname{X}^{n}\Vdash\operatorname{lift}(\phi)[\epsilon/\alpha]\,(a_{b}\,% ;1,\dotsc,1\,;s)$ . The induction cases are straightforward. $\hfill\blacktriangleleft$

Corollary 29.

Let $\phi_{1},\phi_{2}\in L_{\mathit{pcof},m}$ . Let $k$ be the maximal parameter index of $\phi_{1}\Rightarrow\phi_{2}$ . The following are equivalent:

$\blacksquare$

$\operatorname{X}^{m}\Vdash\forall\alpha^{B}\,\big{(}\phi_{1}\Rightarrow\phi_{2% }\big{)}\,(x)$
$\blacksquare$

$\operatorname{X}^{k+m}\Vdash\operatorname{lift}(\phi_{1}\Rightarrow\phi_{2})% \big{[}\epsilon/\alpha\big{]}\,(x_{1},\dotsc,x_{k}\,;1,\dotsc,1\,;x_{k+1},% \dotsc,x_{k+m})$

Proof.

Fix $n\geq 0$ and $s\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{n},\operatorname{X}^{k+% m})$ , and suppose that

\operatorname{X}^{n}\Vdash\operatorname{lift}(\phi_{1})\big{[}\epsilon/\alpha% \big{]}\,(s_{1},\dotsc,s_{k}\,;1,\dotsc,1\,;s_{k+1},\dotsc,s_{k+m})

By Lemma 27 and by assumption, $\operatorname{X}^{n}\Vdash\phi_{2}\,(s_{k+1},\dotsc,s_{k+m}\,;b_{t})$ . And again by Lemma 27,

\operatorname{X}^{n}\Vdash\operatorname{lift}(\phi_{2})\big{[}\epsilon/\alpha% \big{]}\,(s_{1},\dotsc,s_{k}\,;1,\dotsc,1\,;s_{k+1},\dotsc,s_{k+m})

For the converse, fix $n\geq 0$ , $s\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{n},\operatorname{X}^{m})$ , and $b\in\operatorname{B}^{k}\operatorname{X}^{n}$ . Our goal is to check that $\operatorname{X}^{n}\Vdash\phi_{1}\Rightarrow\phi_{2}\,(s\,;b)$ . So fix $p\geq 0$ and $t\in\operatorname{Hom}_{\mathcal{C}}(\operatorname{X}^{p},\operatorname{X}^{n})$ , and suppose that $\operatorname{X}^{p}\Vdash\phi_{1}\,(st\,;b\cdot t)$ . By Lemma 28 and by assumption,

\operatorname{X}^{p}\Vdash\operatorname{lift}(\phi_{2})\big{[}\epsilon/\alpha% \big{]}\,(a_{b\cdot t}\,;1,\dotsc,1\,;st)

So by Lemma 28, $\operatorname{X}^{p}\Vdash\phi_{2}\,(st\,;b\cdot t)$ . $\hfill\blacktriangleleft$

4.4 Applications

To apply the first reduction schema to a concrete algebra $\mathcal{A}$ , it suffices to supply a formula $\chi$ (Definition 15) characterizing local images for $\mathcal{A}$ . To apply the second reduction schema to a concrete algebra $\mathcal{A}$ and language $L_{\gamma}$ , it suffices to supply a formula $\chi$ (Definition 20) which defines the locally prime formulas of $L_{\gamma}$ .

For either schema, if the prenex normal form of $\chi$ contains no universal second-order quantifiers, and it is efficiently computable from $m$ , then the sentence checked in Theorem 16 is in $\forall$ SO; and by Fagin’s theorem, the corresponding model-checking problem is in $\mathrm{coNP}$ (cf. [4, Section 9.2]). This is the case for all of the following applications.

Below, $\leq$ will denote the standard ordering on the set $\{0,1\}$ , as well as this ordering extended component-wise to $\{0,1\}^{n}$ . We will denote the minimal and maximal elements of the poset $\{0,1\}^{n}$ also by 0 and 1.

4.4.1 Bipointed sets

For a theory of bipointed sets, the signature will be $\sigma_{0}=\{0,1\}$ . We take the generating algebra $\mathcal{A}$ to be $\{0,1\}$ with the constants interpreted as $0^{\mathcal{A}}=0$ and $1^{\mathcal{A}}=1$ . When needed, we will annotate constructions associated to this algebra with $b p$ .

We apply the first schema. The following second order formula encodes each term function $s^{\mathcal{A}}_{i}:\mathcal{A}^{m}\to\mathcal{A}$ as a second-order variable $T^{m+1}$ : the first conjunct ensures that $T$ encodes either a projection or a constant, and the second conjunct ensures that $R$ is indeed the image of functions encoded by the $T_{i}$ .

Definition 30.

Let $m\geq 0$ . Define $\chi_{m}$ (for $b p$ terms) to be the formula

	$\displaystyle\exists T^{m+1}_{1}\,\dotsc\exists T^{m+1}_{m}\,$	$\displaystyle\Big{(}\bigwedge_{i}\big{(}\bigvee_{j}\forall y\,\forall x\,\big{% (}T_{i}(y\,;x)\hskip 2.84526pt\leftrightarrow\hskip 2.84526ptx=y_{j}\big{)}$
		$\displaystyle\hskip 28.45274pt\lor\,\forall y\,\forall x\,\big{(}T_{i}(y\,;x)% \hskip 2.84526pt\leftrightarrow\hskip 2.84526ptx=0\big{)}$
		$\displaystyle\hskip 28.45274pt\lor\,\forall y\,\forall x\,\big{(}T_{i}(y\,;x)% \hskip 2.84526pt\leftrightarrow\hskip 2.84526ptx=1\big{)}\big{)}$
		$\displaystyle\hskip 8.53581pt\land\forall x\,\big{(}R(x)\hskip 2.84526pt% \leftrightarrow\hskip 2.84526pt\exists y\,\big{(}\bigwedge_{i}T_{i}(y\,;x_{i})% \big{)}\big{)}\Big{)}$

$\blacktriangleright$ Remark 31.

Let $s\in\mathcal{T}^{m}_{n}$ be an $m$ -tuple of bipointed-set terms. There exist indices $i_{1}<i_{2}<\dotsb<i_{m}$ in $\{1,\dotsc,n\}$ and $s^{\prime}\in\mathcal{T}^{m}_{m}$ such that $s=s^{\prime}[x_{i_{1}}/x_{1},\dotsc,x_{i_{m}}/x_{m}]$ . In particular, for all $n\geq 0$ and $s\in\mathcal{T}^{m}_{n}$ , there exists $s^{\prime}\in\mathcal{T}^{m}_{m}$ such that $\operatorname{img}(s^{\prime\mathcal{A}})=\operatorname{img}(s^{\mathcal{A}})$ .

Proposition 32.

Let $m\geq 0$ . The formula $\chi_{m}$ in Definition 30 characterizes images of $b p$ term functions.

Corollary 33.

The decision problem $\mathrm{PCOFENT}_{\mathit{bp}}$ is $\mathrm{coNP}$ -complete.

4.4.2 Distributive lattices

For the theory of bounded distributive lattices, the signature will be $\sigma_{0}=\{0,1\}$ and $\sigma_{2}=\{\land,\lor\}$ . We take the generating algebra $\mathcal{A}$ to be $\{0,1\}$ with the constants interpreted as $0^{\mathcal{A}}=0$ and $1^{\mathcal{A}}=1$ , and with the basic operations defined as $\land^{\mathcal{A}}=\min$ and $\lor^{\mathcal{A}}=\max$ . When needed, we will annotate constructions associated to this algebra with $d l$ .

Lemma 34.

\{s^{\mathcal{A}}:\mathcal{A}^{n}\to\mathcal{A}\mid s\in\mathcal{T}_{n}\}% \hskip 5.69054pt\cong\hskip 5.69054pt\{f:\mathcal{A}^{n}\to\mathcal{A}\mid f% \text{ is monotone }\}

Proof.

Let $s\in\mathcal{T}_{n}$ . That $s^{\mathcal{A}}$ is monotone follows from the fact that the constant functions, the projections, $\min$ and $\max$ are all monotone.

Conversely, let $f$ be a monotone function. There are many ways to define $s\in\mathcal{T}_{n}$ so that $s^{\mathcal{A}}=f$ , and here is one way. Define $s$ by

s=\bigvee_{f(a)=1}\bigwedge_{a_{k}=1}x_{k}

Suppose $f(a)=1$ . Since $\big{(}\bigwedge_{a_{k}=1}x_{k}\big{)}^{\mathcal{A}}(a)=1$ , $s^{\mathcal{A}}(a)=1$ . Conversely, suppose that $s^{\mathcal{A}}(a)=1$ . Then there exists $a^{\prime}$ such that $f(a^{\prime})=1$ and $(\bigwedge_{a^{\prime}_{k}=1}x_{k})^{\mathcal{A}}(a)=1$ . Hence, $a^{\prime}\leq a$ . But $f$ is monotone, so $f(a)=1$ . $\hfill\blacktriangleleft$

Lemma 35.

Let $B\subseteq\mathcal{A}^{m}$ . Then $B$ contains $\min(B)$ and $\max(B)$ if and only if there exist $n\geq 0$ and $s\in\mathcal{T}^{m}_{n}$ such that $\operatorname{img}(s^{\mathcal{A}})=B$ .

Proof.

Let $\{b_{1},\dotsc,b_{n}\}$ be an enumeration of $B$ . Define the monotone function $f:\mathcal{A}^{n}\to\mathcal{A}^{m}$ by

f(a)=\begin{cases}\min(B)&a=0\\ b_{j}&a_{k}=1\text{ iff }j=k\\ \max(B)&\text{otherwise}\\ \end{cases}

By Lemma 34, there exists an $m$ -tuple of terms $s\in\mathcal{T}^{m}_{n}$ such that $s^{\mathcal{A}}=f$ .

For the converse, observe that $\min(\operatorname{img}(s^{\mathcal{A}}))=s^{\mathcal{A}}(0)$ and $\max(\operatorname{img}(s^{\mathcal{A}}))=s^{\mathcal{A}}(1)$ . $\hfill\blacktriangleleft$

Definition 36.

Let $m\geq 0$ . Define $\chi_{m}$ (for $d l$ terms) to be the formula

	$\displaystyle\exists x\,\big{(}R(x)\land\forall y\,\big{(}R(y)\to\textstyle{% \bigwedge_{i}}(x_{i}=x_{i}\land y_{i})\big{)}\big{)}$
	$\displaystyle\land\,\exists x\,\big{(}R(x)\land\forall y\,\big{(}R(y)\to% \textstyle{\bigwedge_{i}}(y_{i}=x_{i}\land y_{i})\big{)}\big{)}$

Proposition 37.

Let $m\geq 0$ . The formula $\chi_{m}$ in Definition 36 characterizes images for $d l$ term functions.

Corollary 38.

The decision problem $\mathrm{PCOFENT}_{\mathit{dl}}$ is $\mathrm{coNP}$ -complete.

4.4.3 Variable-constant fragments

We will now apply the second schema to show that irrespective of the choice of algebra $\mathcal{A}$ , $\mathrm{PCOFENTVC}$ belongs to $\mathrm{coNP}$ .

Lemma 39.

Let $m\geq 0$ . On the one hand, if $\mathcal{A}\subseteq\{c^{\mathcal{A}}\}$ , then $\forall x_{m+1}\,(x_{m+1}=c)$ is valid; and if not, $\forall x_{m+1}\,(x_{m+1}=c)$ is equivalent to $\bot$ . On the other hand, for $(x_{i}=c)\in L_{\mathit{cof},m}$ , $\forall x_{m+1}\,(x_{i}=c)$ is equivalent to $(x_{i}=c)$ .

$\blacktriangleright$ Remark 40.

Let $m\geq 0$ , and let $\phi\in L_{\mathit{cofvc},m}$ . By Corollaries 5 and 39, we may assume wlog that $\phi$ is, up to equivalence, either $\bot$ , $\top$ , or a disjunction of conjunctions of equations.

Proposition 41.

Let $\phi\in L_{\mathit{cofvc},m}$ . Then

\operatorname{X}^{m}\Vdash\phi\Rightarrow(x_{j}=c)\,(x)\hskip 11.38109pt\text{% iff}\hskip 11.38109pt\mathcal{A}\vDash\forall x\,\big{(}\phi\rightarrow x_{j}=% c\big{)}

Proof.

Induction on $\phi$ (in disjunctive form).

$\blacksquare$

Suppose $\phi=\bot$ or $\phi=\top$ . Immediate.
$\blacksquare$

Suppose that $\phi=\bigwedge_{i\in I}(x_{i}=c_{i})$ where $I\subseteq\{1,\dotsc,m\}$ .
- –
  
  Suppose that $j\in I$ and $c_{j}=c$ . Immediate.
- –
  
  Suppose that $j\notin I$ and $c_{j}=c$ . Suppose that $\operatorname{X}^{m}\Vdash\bigwedge_{i\in I}(x_{i}=c_{i})\Rightarrow(x_{j}=c)% \,(x)$ . In particular, $\operatorname{X}^{m}\Vdash(x_{j}=c)\,(s)$ when
  
  $s_{k}=\begin{cases}c&k\in I\\ x_{k}&\text{otherwise}\\ \end{cases}$
  
  Therefore, $\mathcal{A}=\{c^{\mathcal{A}}\}$ , and the conclusion follows trivially. The converse is analogous.
- –
  
  Suppose that $j\in I$ and $c_{j}\neq c$ . But $\operatorname{X}^{m}\nVdash\bigwedge_{i\in I}(x_{i}=c_{i})\Rightarrow(x_{j}=c)% \,(x)$ because $\operatorname{X}^{0}\Vdash(x_{j}=c_{j})\,(c_{j})$ while $\operatorname{X}^{0}\nVdash(x_{j}=c)\,(c_{j})$ . And likewise, $\mathcal{A}\nvDash\bigwedge_{i\in I}(x_{i}=c_{i})\rightarrow(x_{j}=c)\,(c_{j})$ .
$\blacksquare$

Suppose $\phi=\phi_{1}\lor\phi_{2}$ . Directly by induction.

$\hfill\blacktriangleleft$

Proposition 42.

Let $m\geq 0$ , and let $S_{1},S_{2}\in\Omega\operatorname{X}^{m}$ . Let $E$ be the sieve denoted by the equation $(x_{i}=c)\in L_{\mathit{cofvc},m}$ : that is,

E=\{s:\operatorname{X}^{n}\to\operatorname{X}^{m}\mid n\geq 0,\,s_{i}=c\}\in% \Omega\operatorname{X}^{m}

If $E\subseteq S_{1}\cup S_{2}$ , then either $E\subseteq S_{1}$ or $E\subseteq S_{2}$ .

Proof.

Observe that $E$ is principal: i.e., every morphism in $E$ factors through

s=(x_{1},\dotsc,x_{i-1},c,x_{i+1},\dotsc,x_{m})

So if $s\in S_{1}$ ( $s\in S_{2}$ ), then $E\subseteq S_{1}$ ( $E\subseteq S_{2}$ ). $\hfill\blacktriangleleft$

Corollary 43.

Equations in $L_{\mathit{cofvc}}$ are locally prime.

Lemma 44.

Let $m\geq 0$ . A formula $\rho\in L_{\mathit{cofvc},m}$ is locally prime if and only it is equivalent to a formula of the form

\rho\hskip 2.84526pt=\hskip 2.84526pt\bigwedge_{i\in I}(x_{i}=c_{i})\quad\text% {where }c_{1},\dotsc,c_{m}\in\sigma_{0}

for some non-empty $I\subseteq\{1,\dotsc,m\}$ .

Definition 45.

Let $m\geq 0$ . Define $\chi_{m}$ (for variable-constant fragments) to be the formula

	$\displaystyle\exists C_{1}\dotsc\exists C_{m}\,$	$\displaystyle\Big{(}\bigwedge_{i}\bigvee_{j}\big{(}C_{i}(c_{j})\lor(x_{i}=c_{j% })\big{)}$
		$\displaystyle\hskip 5.69054pt\land\,\bigwedge_{i}\bigwedge_{j}\bigwedge_{j<k}% \big{(}C_{i}(c_{j})\lor C_{i}(c_{k})\big{)}$
		$\displaystyle\hskip 5.69054pt\land\,\big{(}\bigvee_{i,j}\lnot C_{i}(c_{j})\big% {)}\Big{)}$

where $c_{1},\dotsc,c_{|\sigma_{0}|}$ is an enumeration of $\sigma_{0}$ .

Proposition 46.

Let $m\geq 0$ . The formula $\chi_{m}$ in Definition 45 defines the locally prime formulas in $L_{\mathit{cofvc}}$ .

Corollary 47.

If $\sigma_{0}$ has constants 0 and 1 denoting distinct elements of $\mathcal{A}$ , the decision problem $\mathrm{PCOFENTVC}$ is $\mathrm{coNP}$ -complete.

Proof.

By Propositions 8, 41, 46, and 21. $\hfill\blacktriangleleft$

4.4.4 De Morgan algebras

Lastly, we turn to the theory of De Morgan algebras and the term-constant fragment $L_{\mathit{coftc}}$ , which provide the cofibration layer of the cubical type theory in [3]. The strategy below is adapted from [3]: it amounts to reducing the term-constant variant of $\mathrm{COFENT}$ to the variable-constant variant.

The signature of De Morgan algebras will be $\sigma_{0}=\{0,1\}$ , $\sigma_{1}=\{\lnot\}$ , and $\sigma_{2}=\{\land,\lor\}$ . We take the generating algebra $\mathcal{A}$ to be $\{0,1\}^{2}$ with the constants interpreted as $0^{\mathcal{A}}=(0,0)$ and $1^{\mathcal{A}}=(1,1)$ , and with the basic binary operations defined as $\land^{\mathcal{A}}=\min$ and $\lor^{\mathcal{A}}=\max$ . The operation of De Morgan negation on $\{0,1\}^{2}$ is

\begin{array}[]{c|c}x&\lnot^{\mathcal{A}}(x)\\ \hline\cr(0,0)&(1,1)\\ \hline\cr(1,0)&(1,0)\\ \hline\cr(0,1)&(0,1)\\ \hline\cr(1,1)&(0,0)\\ \hline\cr\end{array}

Note that while Boolean negation swaps $(0,1)$ and $(1,0)$ as well as $(0,0)$ and $(1,1)$ , De Morgan negation fixes $(0,1)$ and $(1,0)$ , and swaps just $(0,0)$ and $(1,1)$ . When needed, we will annotate constructions associated to this algebra with $d m$ .

The following definition is adapted from [3]:

Definition 48.

Let $m\geq 0$ , and let $\phi\in L_{\mathit{coftc},m}$ .

	$\displaystyle\phi^{+}$	$\displaystyle=\begin{cases}\bot&\phi=\bot\text{ or }(c^{\prime}=c)\text{ with % }c^{\prime}\neq c\\ \top&\phi=\top\text{ or }(c=c)\\ (f=1)^{-}&\phi=(f=0)\\ (x_{i}=1)&\phi=(x_{i}=1)\\ (f=1)^{-}&\phi=(\lnot f=1)\\ (f_{1}=1)^{+}\land(f_{2}=1)^{+}&\phi=(f_{1}\land f_{2}=1)\\ (f_{1}=1)^{+}\lor(f_{2}=1)^{+}&\phi=(f_{1}\lor f_{2}=1)\\ \phi_{1}^{+}\land\phi_{2}^{+}&\phi=\phi_{1}\land\phi_{2}\\ \phi_{1}^{+}\lor\phi_{2}^{+}&\phi=\phi_{1}\lor\phi_{2}\\ \forall x_{m+1}\,\psi^{+}&\phi=\forall x_{m+1}\,\psi\end{cases}$
	$\displaystyle\phi^{-}$	$\displaystyle=\begin{cases}(f=1)^{+}&\phi=(f=0)\\ (x_{i}=0)&\phi=(x_{i}=1)\\ (f=1)^{+}&\phi=(\lnot f=1)\\ (f_{1}=1)^{-}\lor(f_{2}=1)^{-}&\phi=(f_{1}\land f_{2}=1)\\ (f_{1}=1)^{-}\land(f_{2}=1)^{-}&\phi=(f_{1}\lor f_{2}=1)\\ \end{cases}$

Proposition 49.

Let $m\geq 0$ , and let $\phi\in L_{\mathit{coftc},m}$ . The formula $\phi^{+}\in L_{\mathit{cofvc},m}$ is equivalent to $\phi$ and is proportional in length.

Corollary 50.

The decision problem $\mathrm{PCOFENTTC}_{\mathit{dm}}$ is $\mathrm{coNP}$ -complete.

5 Conclusion

In this paper, we have assembled a capable framework for studying the computational character of key fragments of the internal languages of cubical sets. We have also put it to use and obtained theoretical results with practical importance: not only have we determined the complexity of variants of $\mathrm{COFENT}$ , we have reasonable decision procedures. That said, this framework is capable of more:

$\blacksquare$

We plan to extend our results to simplicial sets. The cofibration language in [6] corresponds not to all presheaves on the cube category, but to sheaves for a specific Grothendieck topology which defines a topos equivalent to simplicial sets. Preliminary work indicates that our results, summarized above, on presheaves on cubical categories will extend to simplicial sets via this equivalence. This would provide the means to automate the cofibration language layer of a directed type theory based on simplicial sets. It would also provide the means to automate the dependently-typed internal language of simplicial sets.
$\blacksquare$

We plan to extend our results to full first-order cofibration languages. For certain finite algebras $\mathcal{A}$ , either or both schemas will apply: for the first schema, it needs to be shown that term-invariance holds for the more expressive fragment; and for the second schema, that the more expressive fragment has local factorization. Deciding validity in this context will give rise to fresh examples of $\mathrm{PSPACE}$ -complete problems.
$\blacksquare$

Finally, we conjecture that there are finite algebras for which the corresponding forcing relation (in presheaves) is undecidable. Our expectation is that counter-examples will help to explain the efficacy of the key properties already discovered: image invariance and local factorization.

References

[1] Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of cartesian cubical type theory. Mathematical Structures in Computer Science, 31(4):424–468, 2021. doi:10.1017/S0960129521000347.
[2] Ulrik Buchholtz and Edward Morehouse. Varieties of cubical sets. Lecture Notes in Computer Science, pages 77–92, 2017. doi:10.1007/978-3-319-57418-9_5.
[3] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom, 2016. arXiv:1611.02108.
[4] Leonid Libkin. Elements of Finite Model Theory. Springer Publishing Company, Incorporated, 1st edition, 2010.
[5] Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer New York, New York, NY, 1994.
[6] Emily Riehl and Michael Shulman. A type theory for synthetic $\infty$ -categories, 2017. arXiv:1705.07442.
[7] Matthew Z. Weaver and Daniel R. Licata. A constructive model of directed univalence in bicubical sets. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20, pages 915–928, New York, NY, USA, 2020. Association for Computing Machinery. doi:10.1145/3373718.3394794.

[bib.bib1] [1] Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of cartesian cubical type theory. Mathematical Structures in Computer Science, 31(4):424–468, 2021. doi:10.1017/S0960129521000347.

[bib.bib2] [2] Ulrik Buchholtz and Edward Morehouse. Varieties of cubical sets. Lecture Notes in Computer Science, pages 77–92, 2017. doi:10.1007/978-3-319-57418-9_5.

[bib.bib3] [3] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom, 2016. arXiv:1611.02108.

[bib.bib4] [4] Leonid Libkin. Elements of Finite Model Theory. Springer Publishing Company, Incorporated, 1st edition, 2010.

[bib.bib5] [5] Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer New York, New York, NY, 1994.

[bib.bib6] [6] Emily Riehl and Michael Shulman. A type theory for synthetic $\infty$ -categories, 2017. arXiv:1705.07442.

[bib.bib7] [7] Matthew Z. Weaver and Daniel R. Licata. A constructive model of directed univalence in bicubical sets. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20, pages 915–928, New York, NY, USA, 2020. Association for Computing Machinery. doi:10.1145/3373718.3394794.

Complexity of Cubical Cofibration Logics I: coNP-Complete Examples

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

1.1 Language fragments for cubical homotopy theory

1.2 Applications for cubical type theory

2 Motivating examples

2.1 Cube boundary inclusion

2.2 Simplex and pyramid

2.3 Example reduction

3 Decision problems

3.1 Formula languages

3.1.1 Types and terms

3.1.2 Parameterized first-order formulas

Definition 1.

3.2 Semantics

3.2.1 Forcing relation

Definition 2.

3.2.2 Presheaf semantics

Theorem 3.

▶ Remark 4.

Corollary 5.

3.3 Languages of representable types

3.4 Indexing category from a finite algebra

3.4.1 Generation by a finite algebra

3.4.2 Finite product theories

3.5 Cofibration formulas

Definition 6.

3.6 Entailment problems

Definition 7.

3.7 Problem characterization in terms of derivability

4 Results

4.1 Reduction from 𝐔𝐍𝐒𝐀𝐓

Proposition 8.

Proof.

Corollary 9.

4.2 Reduction to ∀SO

4.2.1 Translation of 𝑳𝒄𝒐𝒇 to second-order logic

Definition 10.

▶ Remark 11.

4.2.2 First schema

Lemma 12 (Term image invariance).

Proof.

Lemma 13.

Proof.

Corollary 14.

Definition 15.

Theorem 16.

Proof.

4.2.3 Second schema

Definition 17.

Lemma 18.

Proof.

Lemma 19.

Proof.

Definition 20.

Theorem 21.

Proof.

4.3 Parameter elimination

Proposition 22.

Proof.

4.3.1 Bivalent parameters

Lemma 23.

Proof.

Corollary 24.

Proof.

4.3.2 Formula lifting

Definition 25.

Proposition 26.

4.3.3 Grounding

Lemma 27.

Proof.

Complexity of Cubical Cofibration Logics I: $\mathrm{coNP}$ -Complete Examples

$\blacktriangleright$ Remark 4.

4.1 Reduction from $\mathrm{UNSAT}$

4.2 Reduction to $\forall$ SO

4.2.1 Translation of $L_{\mathit{cof}}$ to second-order logic

$\blacktriangleright$ Remark 11.

$\blacktriangleright$ Remark 31.

$\blacktriangleright$ Remark 40.