ATIME AP ND TQBF MC ¯MC

# Complexity of the Model Checking problem for inquisitive propositional and
modal logic

Gianluca Grilletti  Munich Center for Mathematical Philosophy  Ivano Ciardelli
University of Padua

††Gefördert durch die Deutsche Forschungsgemeinschaft (DFG), Projektnummer
446711878. Funded by the German Research Foundation (DFG), project number
446711878.

##  1 Introduction

The aim of this paper is to study the complexity of the _model checking
problem_ $\MC$ for _inquisitive propositional logic_ $\mathsf{InqB}$ and for
_inquisitive modal logic_ $\mathsf{InqM}$, that is, the problem of deciding
whether a given finite structure for the logic satisfies a given formula.111In
the terminology introduced by Vardi in [8], this is the so-called _combined
complexity_ for the model checking problem. In particular, we prove that both
problems are $\APclass$-complete.

_Inquisitive logics_ are a family of formalisms that extend classical and non-
classical logic to encompass _questions_. Traditionally, logic is concerned
with _statements_ , that is, expressions completely determined by their
_truth-conditions_. The standard approaches to semantics are based on this
assumption and are usually formulated in terms of truth-assignment (e.g.,
_Boolean valuations_ in propositional logic). However, this semantical
approach does not allow us to study expressions whose meaning is _not_
determined in terms of truth-conditions, such as _questions_.

In order to interpret questions, which are not true or false, the semantics of
_Inquisitive logic_ is based on a relation called _support_ between and
_information states_ and a sentence. This allows to give a uniform semantic
account for statement and questions alike: an information state _supports_ a
statement if it _implies_ the statement; and it _supports_ a question if it
_resolves_ the question.

The particular instances of inquisitive logic we consider in this paper are
$\mathsf{InqB}$ and $\mathsf{InqM}$, extending propositional logic and modal
logic respectively with the question-forming operators. In these systems
information states are formalized as _sets of truth-assignments_ , which gives
us a much richer semantical structure than in the classical setting. The main
question we tackle in this paper is: how hard is it to _decide if a formula of
$\mathsf{InqB}$ (resp., $\mathsf{InqM}$) is supported by an information state
in a given model_?

The problem of deciding whether a formula $\phi$ of a logic $L$ is satisfied
by a model $\mathcal{M}$ is referred to as the _model checking problem for
$L$_ (in symbols $\MC(L)$). The computational complexity of this problem is
known for several logics (see, e.g., [4] for an overview of the classical
results). In recent years, the problem has been addressed also for a class of
logics called _team logics_ which, like our inquisitive systems, are
interpreted relative to sets of assignments (see, e.g., [5, 6] and [9, Ch.
7]).

Although there is a close connection between these logics and inquisitive
logics, it was still an open question what are the complexities of
$\MC(\mathsf{InqB})$ and $\MC(\mathsf{InqM})$.222Both model checking problems
have been investigated in [10] (unpublished), building up on previous work by
Yang [6]. In this paper we give a reduction of the $\PSPACE$-complete problem
_true quantified Boolean formulas_ $\TQBF$ (see, e.g., [7, Ch. 8]) to
$\MC(\mathsf{InqB})$, thus settling that both $\MC(\mathsf{InqB})$ and
$\MC(\mathsf{InqM})$ are _$\PSPACE$ -complete_.

The paper is structured as follows: In Section 2 we present the basic notions
of inquisitive logic used throughout the paper. In Section 3 we introduce
suitable encodings of $\mathsf{InqB}$ and $\mathsf{InqM}$ structures and
formalize the model checking problems $\MC(\mathsf{InqB})$ and
$\MC(\mathsf{InqM})$. Moreover, in the same section we present an algorithm
for _alternating Turing machines_ to solve $\MC(\mathsf{InqM})$ and use it to
show that $\MC(\mathsf{InqM})$—and a fortiori also $\MC(\mathsf{InqBQ})$—is in
the class $\PSPACE$. In Section 4 we present and study a polynomial-space
reduction of the $\TQBF$ problem to the $\MC(\mathsf{InqB})$, thus showing
that the problem is also $\PSPACE$-hard, and we thus infer that
$\MC(\mathsf{InqB})$ and $\MC(\mathsf{InqM})$ are both $\PSPACE$-complete. We
conclude in Section 5 with some remarks and directions for future work.

##  2 Preliminaries

In this section we recall some basic notions of inquisitive logic that we use
throughout the paper. As an extended introduction on the topic of inquisitive
logic we suggest [1]. As for computational complexity, we assume the reader to
be already familiar with the basic notions on the topic (we refer to [7] for
an introduction) and we limit ourselves to recall the main results used in the
paper.

###  2.1 Inquisitive propositional and modal logic

Henceforth, we indicate with $\mathrm{AP}$ a fixed set of atomic propositions.

######  Definition 1 (Syntax of $\mathsf{InqB}$ and $\mathsf{InqM}$).

The set of formulas of $\mathsf{InqM}$—also called _inquisitive modal
formulas_ —is defined by the following grammar:

$\phi\;::=\;\bot\;|\;p\;|\;\phi\land\phi\;|\;\phi\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\phi\;|\;\phi\to\phi\;|\;\Box\phi\;|\;\boxplus\phi$

where $p\in\mathrm{AP}$. The set of _inquisitive (propositional) formulas_
$\mathsf{InqB}$ is the set of $\mathsf{InqM}$ formulas not containing the
symbols $\Box$ and $\boxplus$.

So the language of inquisitive logic is the standard language of modal logic
extended with
$\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}$ and
$\boxplus$. The operator
$\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}$ is
called _inquisitive disjunction_ , while $\boxplus$ is the _window modality_.
Additionally, we introduce the following standard shorthands:

$\neg\phi:=\phi\to\bot\hskip
50.00008pt\phi\vee\psi:=\neg(\neg\phi\land\neg\psi)$

The role of
$\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}$ is to
enhance the language of modal logic with _alternative questions_. For example,
the formula
$p\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg p$
stands for the _natural language question_ “does $p$ hold (or not)?”. Instead,
the derived operator $\vee$ corresponds to the usual disjunction from
propositional logic: for example, the expression $p\vee\neg p$ is intuitively
interpreted as the _sentence_ “$p$ holds or $p$ does not hold”. We will show
the formal difference in the interpretation of these two formulas after
introducing the semantics of the logic.

The operator $\boxplus$ plays the role of an _inquisitive modality_ ,
sensitive to the inquisitive structures of the models. For example, in the
context of epistemic logic (see, e.g., [3]) where the operator $\Box$ is
interpreted as _knowledge_ of an abstract agent (e.g., $\Box p$ usually stands
for “the agent knows that $p$”), the operator $\boxplus$ is roughly
interpreted as a _wondering_ operator, encoding what the agent wonders about
(e.g., $\boxplus?p$ stands for “the agent wonders whether $p$ is the case”).

As pointed out in Section 1, the presence of questions requires to move from a
semantics based on _truth-assignments_ to one based on _information states_.
To formalize this intuition, the logic employs special semantic structures,
called _information models_.

######  Definition 2 (Information models).

An _information model for $\mathsf{InqB}$_ is a tuple of the form
$\mathcal{M}=\left\langle W,V\right\rangle$ where $W$ is a non-empty set (the
_worlds_ of the model) and $V:\mathrm{AP}\to\mathcal{P}(W)$ is a function
called the _valuation_ of the model.

An _information model for $\mathsf{InqM}$_ is a tuple of the form
$\mathcal{M}=\left\langle W,V,\Sigma\right\rangle$ where $W$ and $V$ are as
before, and $\Sigma:W\to\mathcal{P}(\mathcal{P}(W))$ is a function called an
_inquisitive state map_ , satisfying the following conditions for every $w\in
W$:

  1. 1.

$\Sigma(w)\neq\emptyset$;

  2. 2.

If $s\in\Sigma(w)$ and $t\subseteq s$, then $t\in\Sigma$.

We refer to the second condition as _downward closure of $\Sigma(w)$_.

$V$$p_{0}$$p_{1}$$w_{0}$$w_{1}$$w_{2}$$\Sigma(w_{0})$$w_{0}$$w_{1}$$w_{2}$$\Sigma(w_{1})$$w_{0}$$w_{1}$$w_{2}$$\Sigma(w_{2})$$w_{0}$$w_{1}$$w_{2}$
Figure 1: A graphical representation of an information model for
$\mathsf{InqM}$ over the set of atoms $\mathrm{AP}=\\{p_{0},p_{1}\\}$ and with
set of worlds $W=\\{w_{0},w_{1},w_{2}\\}$. The valuation function $V$ is
represented by the colored rectangles in the first image:
$V(p_{0})=\\{w_{0},w_{2}\\}$ (the red rectangle) and
$V(p_{1})=\\{w_{0},w_{1}\\}$ (the blue rectangle). The map $\Sigma$ is
represented in the other images by depicting the maximal states of each
$\Sigma(w)$ for $w\in W$. So for example
$\Sigma(w_{2})=\\{\,\\{w_{0},w_{1}\\},\,\\{w_{0},w_{2}\\}\,\\}$, as depicted
in the last image. Notice that to obtain a graphical representation of an
information model for $\mathsf{InqB}$, we require only the first image of the
sequence, that is, a representation of the valuation function $V$.

An example of information model for $\mathsf{InqM}$ is depicted in Figure 1.
Each world $w\in W$ is naturally associated with a _Boolean valuation_ over
$\mathrm{AP}$, defined as

$V_{w}(p)=\left\\{\begin{array}[]{ll}1&\text{if }w\in V(p)\\\
0&\text{otherwise}\end{array}\right.$

So we can think of each world as providing a _complete description_ of the
current _state of affairs_. Under this interpretation, we can represent an
information state as a _set of worlds_ , that is, all the worlds _compatible_
with the information state considered. So for example, the information that
“$p$ holds” can be represented as the set of worlds $w$ that assign truth
value $1$ to $p$: $\\{\,w\in W\,|\,V_{w}(p)=1\,\\}=V(p)$. In line with this
intuition, henceforth we refer to a subset $s\subseteq W$ as an _information
state_ of the model. The semantics of the logic is then defined relative to a
model _and_ an information state.

######  Definition 3 (Semantics of $\mathsf{InqM}$).

Let $\mathcal{M}$ be an information and $s$ an information state of the model.
We define the semantic relation $\vDash$ of $\mathsf{InqM}$ by the following
inductive clauses:

$\begin{array}[]{lll}\mathcal{M},s\vDash\bot&\iff&s=\emptyset\\\
\mathcal{M},s\vDash p&\iff&s\subseteq V(p)\;\;\iff\;\;\forall w\in
s.\;V_{w}(p)=1\\\
\mathcal{M},s\vDash\phi\land\psi&\iff&\mathcal{M},s\vDash\phi\text{ and
}\mathcal{M},s\vDash\psi\\\
\mathcal{M},s\vDash\phi\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\psi&\iff&\mathcal{M},s\vDash\phi\text{
or }\mathcal{M},s\vDash\psi\\\ \mathcal{M},s\vDash\phi\to\psi&\iff&\text{For
all $t\subseteq s$, if }\mathcal{M},t\vDash\phi\text{ then
}\mathcal{M},t\vDash\psi\\\ \mathcal{M},s\vDash\Box\phi&\iff&\text{For all
$w\in s$, }\mathcal{M},\bigcup\Sigma(w)\vDash\phi\\\
\mathcal{M},s\vDash\boxplus\phi&\iff&\text{For all $t\in\Sigma[s]$,
}\mathcal{M},t\vDash\phi\end{array}$

If $\mathcal{M},s\vDash\phi$ we say that $s$ _supports_ $\phi$.

Intuitively, an information state $s$ supports a formula $\phi$ if the
information represented by $s$ _implies the statement represented by $\phi$_
or _resolves the question represented by $\phi$_. For example, consider the
formula
$p\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg p$
representing the question “Does $p$ hold?”. The support conditions for this
formula are:

$\begin{array}[]{ll}\mathcal{M},s\vDash
p\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
p&\iff\mathcal{M},s\vDash p\;\text{or}\;\mathcal{M},s\vDash\neg p\\\
&\iff\left(\forall w\in s.\;V_{w}(p)=1\right)\;\text{or}\;\left(\forall w\in
s.\;V_{w}(p)=0\right)\end{array}$

So a state $s$ supports the formula
$p\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg p$
if _either_ all the worlds in $s$ agree on $p$ being true _or_ all the worlds
in $s$ agree on $p$ being false. That is, if we have enough information to
_either_ affirm that $p$ holds _or_ affirm that $p$ does not hold.

We conclude the Section with a proposition, exhibiting two fundamental
properties of the semantics.

######  Proposition 4.

Let $\phi$ be a formula of the language and $\mathcal{M}$ be a model.

(Empty state)

$\mathcal{M},\emptyset\vDash\phi$.

(Persistency)

For every $s\subseteq t\subseteq W$, if $\mathcal{M},s\vDash\phi$ then
$\mathcal{M},t\vDash\phi$.

##  3 Encoding and model checking algorithm

Henceforth, we limit ourselves to work with finite sets of atomic propositions
and with finite models (i.e., with models with finitely many worlds).
Throughout the section, we will use the following ad-hoc notations for ease of
presentation:

  * •

The vocabulary consists of the atomic propositions
$\mathrm{AP}=\\{p_{0},\dots,p_{l-1}\\}$, thus $l$ is the number of atomic
propositions;

  * •

The set of worlds is $W=\\{w_{0},\dots,w_{n-1}\\}$, thus $n$ is the number of
worlds in the model;

  * •

The state map is $\Sigma(w_{i})=\\{S_{0}^{i},\dots,S_{k_{i}-1}^{i}\\}$ for
every $w_{i}\in W$;

  * •

We define $m$ as the “size” of the function $\Sigma$, that is, the value

$m\;=\;|\Sigma(w_{0})|+\dots+|\Sigma(w_{n-1})|\;=\;k_{0}+\dots+k_{n-1}$

Consider an information model. We define a natural way to encode this model by
storing the propositional valuation in $n+1$ binary strings as follows:

  * •

The first string is $\delta$ of length $nl$. The $(li+j)^{\text{th}}$ bit of
the string is $\delta_{li+j}=V_{w_{i}}(p_{j})$. This representation allows to
check conditions of the form $w_{i}\in V(p_{j})$ in time linear in $nl$.

  * •

The other strings are $\epsilon_{0},\dots,\epsilon_{n-1}$. The string
$\epsilon_{k}$ has length $(n+1)k_{i}+1$ and contains in order a digit
$\mathtt{0}$, a binary representation of length $n$ of $S^{i}_{0}$, a digit
$\mathtt{0}$, a binary representation of length $n$ of $S^{i}_{1}$…and ends
with a digit $\mathtt{1}$. This representation allows to check conditions of
the form $w_{i}\in\bigcup\Sigma[s]$ in time linear in $mn$.

An example of encoding is given in Figure 2. Notice that to encode an
information model for $\mathsf{InqB}$ we do not need to store the strings
$\epsilon_{0},\dots,\epsilon_{n-1}$, but just the string $\delta$.

$\begin{array}[]{c}\delta\hskip
10.00002pt\underbrace{\begin{array}[]{ccc}\mathtt{1}&\mathtt{1}&\mathtt{0}\\\
p_{0}&p_{1}&p_{2}\end{array}}_{w_{0}}\underbrace{\begin{array}[]{ccc}\mathtt{0}&\mathtt{1}&\mathtt{0}\\\
p_{0}&p_{1}&p_{2}\end{array}}_{w_{1}}\underbrace{\begin{array}[]{ccc}\mathtt{1}&\mathtt{0}&\mathtt{0}\\\
p_{0}&p_{1}&p_{2}\end{array}}_{w_{2}}\\\\[30.00005pt] \epsilon_{0}\hskip
10.00002pt\mathtt{0}\;\underbrace{\mathtt{0}\mathtt{0}\mathtt{1}}_{\\{w_{2}\\}}\;\mathtt{1}\hskip
30.00005pt\epsilon_{1}\hskip
10.00002pt\mathtt{0}\;\underbrace{\mathtt{1}\mathtt{0}\mathtt{0}}_{\\{w_{0}\\}}\;\,\mathtt{0}\underbrace{\mathtt{0}\mathtt{1}\mathtt{1}}_{\\{w_{1},w_{2}\\}}\mathtt{1}\hskip
30.00005pt\epsilon_{2}\hskip
10.00002pt\mathtt{0}\underbrace{\mathtt{1}\mathtt{1}\mathtt{0}}_{\\{w_{0},w_{1}\\}}\mathtt{0}\underbrace{\mathtt{1}\mathtt{0}\mathtt{1}}_{\\{w_{0},w_{2}\\}}\mathtt{1}\end{array}$
Figure 2: The encoding of the information model depicted in Figure 1. Each bit
of the encoding correspond to the valuation of a propositional atom at a
certain world. For example, the bit $\mathtt{1}$ at position $0$ indicates
that $w_{0}\in V(p_{0})$, while the bit $\mathtt{0}$ at position $2$ indicates
that $w_{0}\notin V(p_{2})$.

We use a similar representation for _information states_ , encoded as strings
of length $n$—where a $1$ in position $i$ indicates that the world $w_{i}$ is
part of the state. So, for example, the state $\\{w_{0},w_{2}\\}$ in a model
with worlds $\\{w_{0},w_{1},w_{2}\\}$ is encoded by the binary string
$\mathtt{101}$. Given these encodings, conditions of the form
$\mathcal{M},s\vDash p_{j}$, $w\in\bigcup\Sigma[s]$ and $t\in\Sigma[s]$ can be
checked in time $\mathcal{O}((n(l+m))^{2})$.333This and others bounds we
indicate in this section are far from optimal, but this will not affect our
analysis of the complexity of the model checking problem.

With a slight abuse of notation, we use the symbols $\mathcal{M}$, $s$ and
$\phi$ to indicate both the formal objects introduced and their binary
encodings. We define the _model checking problem for $\mathsf{InqM}$_ as the
decision problem

$\MC(\mathsf{InqM})\;:=\;\\{\;\left\langle\mathcal{M},s,\phi\right\rangle\;|\;\text{$\mathcal{M}$
is a model for $\mathsf{InqM}$ and }\mathcal{M},s\vDash\phi\;\\}$

We also introduce the corresponding anti-satisfaction problem

$\MCanti(\mathsf{InqM})\;:=\;\\{\;\left\langle\mathcal{M},s,\phi\right\rangle\;|\;\text{$\mathcal{M}$
is a model for $\mathsf{InqM}$ and }\mathcal{M},s\nvDash\phi\;\\}$

Similarly, we introduce the corresponding problems for $\mathsf{InqB}$.

$\displaystyle\MC(\mathsf{InqB})\;:=\;\\{\;\left\langle\mathcal{M},s,\phi\right\rangle\;|\;\text{$\mathcal{M}$
is a model for $\mathsf{InqB}$ and }\mathcal{M},s\vDash\phi\;\\}$
$\displaystyle\MCanti(\mathsf{InqB})\;:=\;\\{\;\left\langle\mathcal{M},s,\phi\right\rangle\;|\;\text{$\mathcal{M}$
is a model for $\mathsf{InqB}$ and }\mathcal{M},s\nvDash\phi\;\\}$

We are interested in studying the complexity of these decision problems, and
in particular we claim that all the problems have complexity $\PSPACE$. Notice
that the problem $\MC(\mathsf{InqM})$ (resp., $\MCanti(\mathsf{InqM})$) is
strictly more complex than the problem $\MC(\mathsf{InqB})$ (resp.,
$\MCanti(\mathsf{InqB})$), so for our claim we just need to prove that the
former is a $\PSPACE$ problem and the latter is a $\PSPACE$-hard problem.

Firstly, we present two mutually recursive algorithms for alternating Turing
machines (ATMs) (see, e.g., [7, Ch. 10]) to solve $\MC(\mathsf{InqM})$ and
$\MCanti(\mathsf{InqM})$: $\mathtt{PosSem}$, which checks the condition
$\mathcal{M},s\vDash\phi$, and $\mathtt{NegSem}$, which checks the condition
$\mathcal{M},s\nvDash\phi$. These algorithms are a variation of the algorithms
presented in [9, Ch. 7] and [10].

For brevity we will present the algorithms in pseudo-code. We make use of the
following expressions:

  * •

As usual, we indicate with true, false the Boolean values, and with and, or,
neg the standard Boolean operators.

  * •

Given a state $s$, we indicate with $\forall t\subseteq s$ that we are
employing the universal states of the ATM to choose a subset $t\subseteq s$.
In particular, the result yielded by the algorithm (relative to this non-
deterministic branch of the computation) is true iff for all possible choices
of $t$ the algorithm yields true.

  * •

Given a state $s$, we indicate with $\exists t\subseteq s$ that we are
employing the existential states of the ATM to choose a subset $t\subseteq s$.
In particular, the result yielded by the algorithm (relative to this non-
deterministic branch of the computation) is true iff for at least one choice
of $t$ the algorithm yields true.

Both operations can be implemented in an ATM by choosing non-deterministically
the bits of the representation of $t$. This amounts to $|s|$ non-deterministic
choices, thus both operations have complexity in $\mathcal{O}(n)$.

⬇

1Algorithm PosSem

2Input: $\mathcal{M}$,$s$,$\phi$.

3Output: true if $[\mathcal{M},s\vDash\phi]$, false otherwise.

4

5Match $\phi$ with

6 $\phi=p_{j}$:

7 define result := true

8 foreach i in {0,...,n-1}:

9 if $w_{i}\in s$ and $V_{w_{i}}(p_{j})=0$ then result := false

10 return result

11 $\phi=\psi\land\chi$:

12 define result := PosSem($\mathcal{M}$,$s$,$\psi$) and
PosSem($\mathcal{M}$,$s$,$\chi$)

13 return result

14
$\phi=\psi\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\chi$:

15 define result := PosSem($\mathcal{M}$,$s$,$\psi$) or
PosSem($\mathcal{M}$,$s$,$\chi$)

16 return result

17 $\phi=\psi\to\chi$:

18 $\forall t\subseteq s$

19 define result := NegSem($\mathcal{M}$,$t$,$\psi$) or
PosSem($\mathcal{M}$,$t$,$\chi$)

20 return result

21 $\phi=\Box\psi$:

22 define result := true

23 foreach i in {0,...,n-1}:

24 if $w_{i}\in s$ then:

25 define $t$ := $\bigcup\Sigma(w_{i})$

26 if NegSem($\mathcal{M}$,$t$,$\psi$) then result := false

27 return result

28 $\phi=\boxplus\psi$:

29 define result := true

30 foreach i in {0,...,n-1}:

31 if $w_{i}\in s$ then foreach $t\in\Sigma(w)$:

32 if NegSem($\mathcal{M}$,$t$,$\psi$) then result := false

33 return result

⬇

1Algorithm NegSem

2Input: $\mathcal{M}$,$s$,$\phi$.

3Output: true if $[\mathcal{M},s\nvDash\phi]$, true otherwise.

4

5Match $\phi$ with

6 $\phi=p_{j}$:

7 return neg(PosSem($\mathcal{M},s,p_{j}$))

8 $\phi=\psi\land\chi$:

9 define result := NegSem($\mathcal{M}$,$s$,$\psi$) or
NegSem($\mathcal{M}$,$s$,$\chi$)

10 return result

11
$\phi=\psi\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\chi$:

12 define result := NegSem($\mathcal{M}$,$s$,$\psi$) and
NegSem($\mathcal{M}$,$s$,$\chi$)

13 return result

14 $\phi=\psi\to\chi$:

15 $\exists t\subseteq s$

16 define result := PosSem($\mathcal{M}$,$t$,$\psi$) and
NegSem($\mathcal{M}$,$t$,$\chi$)

17 return result

18 $\phi=\Box\psi$:

19 define result := false

20 foreach i in {0,...,n-1}:

21 if $w_{i}\in s$ then:

22 define $t$ := $\bigcup\Sigma(w_{i})$

23 if NegSem($\mathcal{M}$,$t$,$\psi$) then result := true

24 return result

25 $\phi=\boxplus\psi$:

26 define result := false

27 foreach i in {0,...,n-1}:

28 if $w_{i}\in s$ then foreach $t\in\Sigma(w)$:

29 if NegSem($\mathcal{M}$,$t$,$\psi$) then result := true

30 return result

Both algorithms work as intended, as proved in the following proposition.

######  Proposition 5.

Let $\mathcal{M}$ be an information model, $s$ an information state of
$\mathcal{M}$ and $\phi$ an inquisitive formula.

  * •

$\mathtt{PosSem}$ with inputs $\mathcal{M},s,\phi$ returns as output true iff
$\mathcal{M},s\vDash\phi$.

  * •

$\mathtt{NegSem}$ with inputs $\mathcal{M},s,\phi$ returns as output true iff
$\mathcal{M},s\nvDash\phi$.

###### Proof.

The proof proceeds by induction on the structure of the formula $\phi$. The
cases for conjunction and disjunction are a direct translation of the semantic
clauses (or their contrapositive conditions), so we comment only the cases for
atomic proposition, implication and modalities.

  * •

Case $\phi=p_{j}$ in $\mathtt{PosSem}$: The pseudo-code for this case consists
of the following lines:

⬇

7define result := true

8foreach i in {0,...,n-1}:

9 if $w_{i}\in s$ and $V_{w_{i}}(p_{j})=0$ then result := false

10return result

The variable result (the output of this portion of code) is initially assigned
value true (line 7) and this value may be updated to false in the foreach-loop
(lines 8-9).

Firstly assume that $\mathcal{M},s\vDash p_{j}$, i.e., for every $w_{i}\in s$
we have $V_{w_{i}}(p_{j})=1$. In this case, the condition of the if-then
expression at line 17 (if $w_{i}\in s$ and $V_{w_{i}}(p_{j})=0$) is never
satisfied, thus the variable result maintains the value true, and the
algorithm returns the correct value true (line 10).

Secondly assume that $\mathcal{M},s\nvDash p_{j}$, i.e., there exists
$w_{i}\in s$ for which $V_{w_{i}}(p_{j})=0$. In this case, the condition of
the if-then expression at line 17 is satisfied for $w_{i}$, thus the variable
result is assigned value false, and the algorithm returns the correct value
false (line 10).

  * •

Case $\phi=p_{j}$ in $\mathtt{NegSem}$: The pseudo-code for this case consists
of the following lines:

⬇

7return neg(PosSem($\mathcal{M},s,p_{j}$))

In this case the algorithm returns the Boolean negation of the output of
$\mathtt{\mathtt{PosSem}(}\mathcal{M},s,p_{j}\mathtt{)}$. That is, the
algorithm returns true if $\mathcal{M},s\nvDash p_{j}$ and it returns false if
$\mathcal{M},s\vDash p_{j}$, which is the expected behavior.

  * •

Case $\phi=\psi\to\chi$ in $\mathtt{PosSem}$: The pseudo-code for this case
consists of the following lines:

⬇

15$\forall t\subseteq s$

16define result := NegSem($\mathcal{M}$,$t$,$\psi$) or
PosSem($\mathcal{M}$,$t$,$\chi$)

17return result

Translating the algorithm in mathematical expressions and applying the
inductive hypothesis, this piece of code returns the Boolean value
corresponding to the following expression:

$\forall t\subseteq
s.\;\left[\;\mathcal{M},t\nvDash\psi\;\text{or}\;\mathcal{M},t\vDash\chi\;\right],$

which is exactly the semantic clause for $\mathcal{M},s\vDash\psi\to\chi$.

  * •

Case $\phi=\psi\to\chi$ in $\mathtt{NegSem}$: The pseudo-code for this case
consists of the following lines:

⬇

15$\exists t\subseteq s$

16define result := PosSem($\mathcal{M}$,$t$,$\psi$) and
NegSem($\mathcal{M}$,$t$,$\chi$)

17return result

Translating the algorithm in mathematical expressions and applying the
inductive hypothesis, this piece of code returns the Boolean value
corresponding to the following expression:

$\exists t\subseteq
s.\;\left[\;\mathcal{M},t\vDash\psi\;\text{and}\;\mathcal{M},t\nvDash\chi\;\right]$

which is equivalent to the following expression, that is, the semantic
condition corresponding to $\mathcal{M},s\nvDash\psi\to\chi$:

$\neg\big{(}\;\;\forall t\subseteq
s.\;\left[\;\mathcal{M},t\nvDash\psi\;\text{or}\;\mathcal{M},t\vDash\chi\;\right]\;\;\big{)}$

  * •

Case $\phi=\Box\psi$ in $\mathtt{PosSem}$: The pseudo-code for this case
consists of the following lines:

⬇

22define result := true

23foreach i in {0,...,n-1}:

24 if $w_{i}\in s$ then:

25 define $t$ := $\bigcup\Sigma(w_{i})$

26 if NegSem($\mathcal{M}$,$t$,$\psi$) then result := false

27return result

The variable $\mathtt{result}$ (the output of this portion of code) is
initially assigned value $\mathtt{true}$ (line 22) and the value is updated to
$\mathtt{false}$ in the $\mathtt{foreach}$-loop only if there exists $w_{i}\in
s$ such that
$\mathtt{NegSem(}\mathcal{M}\mathtt{,}\bigcup\Sigma(w_{i})\mathtt{,}\psi\mathtt{)}$
(lines 23-26). Applying the inductive hypothesis, the piece of code returns
the Boolean value corresponding to the following expression:

$\forall w_{i}\in s.\;\mathcal{M},\bigcup\Sigma(w_{i})\vDash\psi$

which is the semantic condition corresponding to
$\mathcal{M},s\vDash\Box\psi$.

  * •

Case $\phi=\Box\psi$ in $\mathtt{NegSem}$: The pseudo-code for this case
consists of the following lines:

⬇

19define result := true

20foreach i in {0,...,n-1}:

21 if $w_{i}\in s$ then:

22 define $t$ := $\bigcup\Sigma(w_{i})$

23 if NegSem($\mathcal{M}$,$t$,$\psi$) then result := false

24return result

This portion of code is exactly the same as the portion for $\Box\psi$ in the
algorithm $\mathtt{PosSem}$ (lines 22-27), but with the values assigned to the
variable $\mathtt{result}$ reversed. Thus applying an analogous reasoning as
in the previous point, the piece of code returns the Boolean value
corresponding to the following expression:

$\exists w_{i}\in s.\;\mathcal{M},\bigcup\Sigma(w_{i})\nvDash\psi$

which is the semantic condition corresponding to
$\mathcal{M},s\nvDash\Box\psi$.

  * •

Case $\phi=\boxplus\psi$ in $\mathtt{PosSem}$: The pseudo-code for this case
consists of the following lines:

⬇

29define result := true

30foreach i in {0,...,n-1}:

31 if $w_{i}\in s$ then foreach $t\in\Sigma(w)$:

32 if NegSem($\mathcal{M}$,$t$,$\psi$) then result := false

33return result

The variable result (the output of this portion of code) is initially assigned
value true (line 29) and this value may be updated to false in the foreach-
loop in case $\mathtt{NegSem(}\mathcal{M}\mathtt{,}t\mathtt{,}\psi\mathtt{)}$
holds for some $t\in\bigcup\Sigma[s]$ (lines 30-32). Translating this
condition in mathematical formulas, this corresponds to the following
expression:

$\forall t\in\Sigma[s].\;\mathcal{M},t\vDash\psi$

which is the semantic condition corresponding to
$\mathcal{M},s\vDash\boxplus\psi$.

  * •

Case $\phi=\boxplus\psi$ in $\mathtt{NegSem}$: The pseudo-code for this case
consists of the following lines:

⬇

26define result := true

27foreach i in {0,...,n-1}:

28 if $w_{i}\in s$ then:

29 define $t$ := $\bigcup\Sigma(w_{i})$

30 if NegSem($\mathcal{M}$,$t$,$\psi$) then result := false

31return result

This portion of code is exactly the same as the portion for $\boxplus\psi$ in
the algorithm $\mathtt{PosSem}$ (lines 29-33), but with the values assigned to
the variable $\mathtt{result}$ reversed. Thus applying an analogous reasoning
as in the previous point, the piece of code returns the Boolean value
corresponding to the following expression:

$\exists t\in\Sigma[s].\;\mathcal{M},t\nvDash\psi$

which is the semantic condition corresponding to
$\mathcal{M},s\nvDash\boxplus\psi$.

∎

We leave to the eager reader the task to show that both algorithms have
complexity $\mathcal{O}((n(l+m))^{2}\cdot\left|\phi\right|)$, where
$\left|\phi\right|$ denotes the size of the encoding of the formula $\phi$.
Since the input consists of an encoding of the model together with an encoding
of the formula (plus overhead), the size of the input is linear in
$t=n(l+m)+\left|\phi\right|$. So the previous analysis shows that the problems
$\MC(\mathsf{InqM})$ and $\MCanti(\mathsf{InqM})$ both lie in
$\ATIME(t^{3})\subseteq\PSPACE$.444Recall that
$\PSPACE=\AP:=\bigcup_{i\in\mathbb{N}}\ATIME(t^{i})$ (see [7, Th. 10.21]).

######  Theorem 6.

The problems $\MC(\mathsf{InqM})$ and $\MCanti(\mathsf{InqM})$ are in
$\PSPACE$.

##  4 Complexity of Model Checking for $\mathsf{InqB}$

In this section we provide a polynomial reduction of the $\PSPACE$-complete
problem $\TQBF$ (the set of _true quantified Boolean formulas_) to
$\MC(\mathsf{InqB})$. Combined with the results from the previous section,
this shows that $\MC(\mathsf{InqB})$ and $\MC(\mathsf{InqM})$ are
$\PSPACE$-complete problems. Moreover, since the problem $\MC(\mathsf{InqB})$
trivially reduces to $\MCanti(\mathsf{InqB})$, this suffices to show that also
$\MCanti(\mathsf{InqB})$ and $\MCanti(\mathsf{InqM})$ are also
$\PSPACE$-complete. Since we are working with the logic $\mathsf{InqB}$, we
will work only with models for $\mathsf{InqB}$ (recall that we introduced the
graphical representation of these models in Figure 1).

The section is divided in several parts. Firstly we introduce the family of
_switching models_ and show how to use them to encode Boolean valuations.555We
remark here that we the terminology _Boolean valuations_ to indicate functions
with codomain $\\{0,1\\}$, not to be confused with the valuation of an
information model. Secondly, we introduce some special formulas, later used to
encode an instance of the $\TQBF$ problem (i.e., a quantified Boolean
sentence) into an instance of $\MC(\mathsf{InqB})$. These formulas allow to
simulate the steps of a non-deterministic search to solve the $\TQBF$ problem.
Thirdly, we employ the formulas previously defined to define the encoding and
show that it is a reduction of the $\TQBF$ problem into the
$\MC(\mathsf{InqB})$ problem. Finally, we show that the encoding proposed is
polinomially bounded in size, thus proving that it preserves
$\PSPACE$-hardness.

###  4.1 Switching models

We introduce _switching models_ , a family of inquisitive models. These models
allows us to encode Boolean valuations as information states. These models
were originally employed in [5] and later in [9, Ch. 7] to study the model
checking problem for different team semantics.

######  Definition 7 (Switching model).

Given $l\in\mathbb{N}$ a positive natural number, we define the model
$\mathcal{S}_{l}=\left\langle W_{l},V_{l}\right\rangle$ over the set of
propositional atoms $\\{p_{0},\dots,p_{l-1},q_{0},\dots,q_{l-1}\\}$ by the
following clauses:

  * •

$W_{l}=\\{w_{0}^{+},w_{0}^{-},w_{1}^{+},w_{1}^{-},\dots,w_{l-1}^{+},w_{l-1}^{-}\\}$;

  * •

$V_{l}(p_{i})=\\{w_{i}^{+}\\}$;

  * •

$V_{l}(q_{i})=\\{w_{i}^{+},w_{i}^{-}\\}$.

$p_{1}$$p_{2}$$p_{3}$$q_{1}$$q_{2}$$q_{3}$$w_{1}^{+}$$w_{1}^{-}$$w_{2}^{+}$$w_{2}^{-}$$\cdots$$w_{l}^{+}$$w_{l}^{-}$
Figure 3: The switching model $\mathcal{S}_{l}$. The circles represent the
worlds of the model ($w_{1}^{+},w_{1}^{-},\dots$). The extension of the atomic
propositions is depicted by the colored rectangles (in green the atoms
$p_{i}$, in blue the atoms $q_{i}$). For example, the set
$V_{l}(p_{2})=\\{w_{2}^{+}\\}$ corresponds to the second (from the left) green
rectangle.

A representation of a switching model is depicted in Figure 3. For a fixed
switching model $\mathcal{S}_{l}$, we define special states to encode Boolean
valuations over the set of atoms $\mathrm{AP}_{k}:=\\{x_{0},\dots,x_{k-1}\\}$
for $k\leq l$: we will call these states _$k$ -switchings_.666Notice that we
are using two distinct families of propositional atoms: the $p_{i}$s and
$q_{i}$s are the atoms evaluated on the switching model, while the $x_{i}$s
(the elements of $\mathrm{AP}_{k}$) are the atoms used to define the Boolean
valuations encode by information states.

######  Definition 8.

Consider a number $k\leq l$. A _$k$ -switching_ of $\mathcal{S}_{l}$ is an
information state $s$ with the following two properties:

  * •

For every $i<k$, $s$ contains exactly one world among $w_{i}^{+}$ and
$w_{i}^{-}$;

  * •

For every $i$ with $k\leq i<l$, $s$ contains both $w_{i}^{+}$ and $w_{i}^{-}$.

Two examples of switchings are depicted in Figure 4. Notice that there exists
only one $0$-switching, that is, the info state $W_{l}$. There is a natural
correspondence between $k$-switchings of $\mathcal{S}_{l}$ and Boolean
valuations over $\mathrm{AP}_{k}$. Given a _Boolean valuation_
$\sigma:\mathrm{AP}_{k}\to\\{0,1\\}$, we define the corresponding
$k$-switching $s_{\sigma}$ by the following clauses (for $i<k$):

$\begin{array}[]{lcl}w_{i}^{+}\in s_{\sigma}&\quad\iff&\sigma(x_{i})=1\\\
w_{i}^{-}\in s_{\sigma}&\quad\iff&\sigma(x_{i})=0\end{array}$

This correspondence also holds for the particular case of $k=0$: the set
$\mathrm{AP}_{0}$ is empty, so there is only one valuation over this set (the
empty function); and the only $0$-switching of $\mathcal{S}_{l}$ is $W_{l}$,
the set of all worlds of the model.

Let us also highlight the following properties, which will come in handy to
later define the encoding of a quantified Boolean formula. For $i\leq k$ we
have:

$\begin{array}[]{lcl}\sigma(x_{i})=1&\quad\iff&s_{\sigma}\vDash q_{i}\to
p_{i}\\\ \sigma(x_{i})=0&\quad\iff&s_{\sigma}\vDash q_{i}\to\neg
p_{i}\end{array}$

This map from Boolean valuations $\sigma$ to $k$-switchings $s_{\sigma}$ is
bijective. Its inverse $s\mapsto\sigma_{s}$ is defined by the following two
equivalent conditions:

$\begin{array}[]{lcl}\sigma_{s}(x_{i})=1&\quad\iff&w_{i}^{+}\in s\\\
\sigma_{s}(x_{i})=0&\quad\iff&w_{i}^{-}\in s\end{array}$

$w_{0}^{+}$$w_{0}^{-}$$w_{1}^{+}$$w_{1}^{-}$$w_{2}^{+}$$w_{2}^{-}$$w_{3}^{+}$$w_{3}^{-}$

$w_{0}^{+}$$w_{0}^{-}$$w_{1}^{+}$$w_{1}^{-}$$w_{2}^{+}$$w_{2}^{-}$$w_{3}^{+}$$w_{3}^{-}$

Figure 4: A $4$-switching $s$ (on the left) and a $2$-switching $t$ (on the
right) over the model $\mathcal{S}_{4}$. $s$ corresponds to the Boolean
valuation $\sigma:\mathrm{AP}_{4}\to\\{0,1\\}$ defined as $\sigma(x_{0})=1$,
$\sigma(x_{1})=0$, $\sigma(x_{2})=1$ and $\sigma(x_{3})=1$. $t$ corresponds to
the Boolean valuation $\tau:\mathrm{AP}_{2}\to\\{0,1\\}$ defined as
$\tau(x_{0})=1$ and $\tau(x_{1})=0$.

###  4.2 Some special formulas

We now introduce several formulas that will help us in our endeavors. Each of
these formulas has a characteristic semantics when interpreted on the
switching model $\mathcal{S}_{l}$.

$C_{k}^{+}:=q_{k}\land p_{k}\quad\text{and}\quad C_{k}^{-}:=q_{k}\land\neg
p_{k}\qquad\text{for $0\leq k<l$}$ (1)

These two formulas characterize the singleton states $\\{w_{k}^{+}\\}$ and
$\\{w_{k}^{-}\\}$ respectively. A depiction of their semantics is given in
Figure 5.

$C_{0}^{+}$$C_{0}^{-}$$C_{1}^{+}$$C_{1}^{-}$$C_{2}^{+}$$C_{2}^{-}$$C_{3}^{+}$$C_{3}^{-}$$w_{0}^{+}$$w_{0}^{-}$$w_{1}^{+}$$w_{1}^{-}$$w_{2}^{+}$$w_{2}^{-}$$w_{3}^{+}$$w_{3}^{-}$
Figure 5: Semantics of $C_{k}^{+}$ and $C_{k}^{-}$.

$D_{k}:=q_{k}\to{\,?p_{k}}\qquad\text{for $0\leq k<l$}$ (2)

The maximal states satisfying $D_{k}$ are depicted in Figure 6. We give a
short proof that this is indeed their semantics.

######  Lemma 9.

Let $s$ be a state of $\mathcal{S}_{l}$. Then the maximal substates of $s$
satisfying $D_{k}$ are $t^{+}=s_{\sigma}\setminus\\{w_{k}^{-}\\}$ and
$t^{-}=s_{\sigma}\setminus\\{w_{k}^{+}\\}$.

###### Proof.

The only state of $\mathcal{S}_{l}$ satisfying $q_{k}$ and not satisfying
$?p_{k}$ is $\\{w^{+}_{k},w^{-}_{k}\\}$. So by definition of $D_{k}$ for every
$t\subseteq s$ we have that $\mathcal{S}_{l},t\vDash D_{k}$ iff
$\\{w^{+}_{k},w^{-}_{k}\\}\nsubseteq t$. In particular, $t^{+}$ and $t^{-}$
are the maximal substates of $s$ with these property. ∎

$w_{0}^{+}$$w_{0}^{-}$$w_{1}^{+}$$w_{1}^{-}$$w_{2}^{+}$$w_{2}^{-}$$w_{3}^{+}$$w_{3}^{-}$

$w_{0}^{+}$$w_{0}^{-}$$w_{1}^{+}$$w_{1}^{-}$$w_{2}^{+}$$w_{2}^{-}$$w_{3}^{+}$$w_{3}^{-}$

Figure 6: The two maximal states satisfying $D_{1}$ in the model
$\mathcal{S}_{4}$.

$\displaystyle S_{0}$
$\displaystyle:=\operatorname*{{\boldsymbol{\raisebox{-0.85pt}{\rotatebox{-2.0}{\scalebox{1.375}{$\backslash$}}}}\mkern-13.0mu\bigvee}}_{i=0}^{l-1}\left(\neg
C_{i}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{i}^{-}\right)$ (3) $\displaystyle S_{k}$
$\displaystyle:=\operatorname*{{\boldsymbol{\raisebox{-0.85pt}{\rotatebox{-2.0}{\scalebox{1.375}{$\backslash$}}}}\mkern-13.0mu\bigvee}}_{i=0}^{k-1}\left(\neg
C_{i}^{+}\land\neg
C_{i}^{-}\right)\;\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\;\operatorname*{{\boldsymbol{\raisebox{-0.85pt}{\rotatebox{-2.0}{\scalebox{1.375}{$\backslash$}}}}\mkern-13.0mu\bigvee}}_{i=k}^{l-1}\left(\neg
C_{i}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{i}^{-}\right)\quad\text{for $0<k<l$}$ (4) $\displaystyle S_{l}$
$\displaystyle:=\operatorname*{{\boldsymbol{\raisebox{-0.85pt}{\rotatebox{-2.0}{\scalebox{1.375}{$\backslash$}}}}\mkern-13.0mu\bigvee}}_{i=0}^{l-1}\left(\neg
C_{i}^{+}\land\neg C_{i}^{-}\right)$ (5)

The semantics of the formulas $S_{k}$ is more complex to describe, but we omit
a thorough analysis since we only need the following technical lemma.

######  Lemma 10.

Let $s$ be a $k$-switching of the model $\mathcal{S}_{l}$. Then
$\mathcal{S}_{l},s\nvDash S_{k}$, but for every proper subset $t\subsetneq s$
it holds $\mathcal{S}_{l},t\vDash S_{k}$.

###### Proof.

Firstly, let us show that $s\nvDash S_{k}$ (for ease of read, in the rest of
the proof we will omit the model $\mathcal{S}_{l}$). Since $S_{k}$ is a
disjunction, we just need to check that each disjunct is not satisfied at $s$.

  * •

For $i<k$, by Definition 8 $s$ contains exactly one world among $w_{i}^{+}$
and $w_{i}^{-}$. This means that $s\vDash C_{i}^{+}$ or $s\vDash C_{i}^{-}$.
In either case we have $s\nvDash\neg C_{i}^{+}\land\neg C_{i}^{-}$.

  * •

For $i\geq k$, by Definition 8 $s$ contains both worlds $w_{i}^{+}$ and
$w_{i}^{-}$. This means that $s\nvDash\neg C_{i}^{+}$ (since it contains
$w_{i}^{+}$) and $s\nvDash\neg C_{i}^{-}$ (since it contains $w_{i}^{-}$). So
we have $s\nvDash\neg
C_{i}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{i}^{-}$.

Since these are all the disjuncts of $S_{k}$, the formula is not satisfied at
$s$.

Secondly, let us show that every $t\subsetneq s$ satisfies $S_{k}$. Since
$S_{k}$ is a disjunction, we just need to find a disjunct satisfied by $t$.
And since the containment $t\subsetneq s$ is strict, there exists a world in
$w_{i}^{e}$ in $s$ and not in $t$. We consider two cases, depending whether
$i<k$ or $i\geq k$.

  * •

If $i<k$, by Definition 8 $t$ does not contain $w_{i}^{+}$ nor $w_{i}^{-}$
(one of them was already missing from $s$). So $t\vDash\neg
C_{i}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{i}^{-}$, which is a disjunct of $S_{k}$, thus $t\vDash S_{k}$.

  * •

If $i\geq k$, by Definition 8 $t$ contains exactly one among $w_{i}^{+}$ and
$w_{i}^{-}$ ($s$ being a $k$-switching contains both of them). This means that
either $t\vDash\neg C_{i}^{+}$ (if $w_{i}^{+}\notin t$) or $t\vDash\neg
C_{i}^{-}$ (if $w_{i}^{-}\notin t$). In both cases we have $t\vDash\neg
C_{i}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{i}^{-}$, which is a disjunt of $S_{k}$, thus $t\vDash S_{k}$.

So it follows that $t\vDash S_{k}$, as desired. ∎

###  4.3 The translation

We have all the elements to define our encoding of an instance of $\TQBF$ into
an instance of $\MC(\mathsf{InqB})$, that is, an information model, a state
and an _inquisitive formula_. We firstly focus on the most complex part:
defining the inquisitive formula.

For ease of read, we use the symbols $\zeta,\xi,\eta$ to indicate
propositional formulas (without quantifiers, so that an arbitrary QBF is of
the form $Q_{0}x_{0}\dots Q_{l-1}x_{l-1}\zeta$) and the symbols
$\phi,\psi,\chi$ to indicate inquisitive formulas. Moreover, we assume that
propositional formulas contain only propositional variables from the set
$\mathrm{AP}_{l}=\\{x_{0},\dots,x_{l-1}\\}$. Finally, we assume that all
propositional formulas are in _negation normal form_ , that is, for negations
only appear in front of atomic propositions.777Translating a formula in
negation normal form is an operation linear in time, thus this assumption does
not affect our complexity analysis.

We give the translation in two steps: firstly, we define by recursion _two_
translations of _propositional formulas_ into inquisitive formulas with an
associated polarity, a _positive translation_ $\zeta^{p}$ and a _negative
translation_ $\zeta^{n}$. Then we provide, again by mutual recursion, two
translations for quantified Boolean formulas with an associated polarity,
$(Q_{0}x_{0}\dots Q_{l-1}x_{l-1}\zeta)^{P}$ and $(Q_{0}x_{0}\dots
Q_{l-1}x_{l-1}\zeta)^{N}$.

The translations $\zeta^{p}$ and $\zeta^{n}$ are defined by the following
clauses:

<EMAIL_ADDRESS>@{\hspace{4em}}
l@{\hspace{.2em}}l}(x_{i})^{p}\hfil\hskip 1.99997pt&:=q_{i}\to
p_{i}\hfil\hskip 40.00006pt&(x_{i})^{n}\hfil\hskip 1.99997pt&:=q_{i}\to\neg
p_{i}\\\ (\neg x_{i})^{p}\hfil\hskip 1.99997pt&:=q_{i}\to\neg p_{i}\hfil\hskip
40.00006pt&(\neg x_{i})^{n}\hfil\hskip 1.99997pt&:=q_{i}\to p_{i}\\\
(\zeta\land\xi)^{p}\hfil\hskip 1.99997pt&:=\zeta^{p}\land\xi^{p}\hfil\hskip
40.00006pt&(\zeta\land\xi)^{n}\hfil\hskip
1.99997pt&:=\zeta^{n}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\xi^{n}\\\
(\zeta\vee\xi)^{p}\hfil\hskip
1.99997pt&:=\zeta^{p}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\xi^{p}\hfil\hskip
40.00006pt&(\zeta\vee\xi)^{n}\hfil\hskip
1.99997pt&:=\zeta^{n}\land\xi^{n}\end{array}$

This translation allows us to encode the semantics of $\zeta$ in terms of
switching states instead of Boolean valuations. In particular, the formula
$\zeta$ is satisfied under a certain Boolean valuation $\sigma$ iff
$\zeta^{p}$ is supported by the corresponding switching $s_{\sigma}$ (recall
Definition 8).

######  Lemma 11.

Let $\sigma:\mathrm{AP}_{l}\to\\{0,1\\}$ be a Boolean valuation and let
$s_{\sigma}$ be the corresponding switching of $\mathcal{S}_{l}$. Then for
every propositional formula $\zeta$ we have that:

$\begin{array}[]{l @{\qquad\text{iff}\qquad} l @{\qquad\text{iff}\qquad}
l}\sigma(\zeta)=1&s_{\sigma}\vDash\zeta^{p}&s_{\sigma}\nvDash\zeta^{n}\\\
\sigma(\zeta)=0&s_{\sigma}\vDash\zeta^{n}&s_{\sigma}\nvDash\zeta^{p}\end{array}$

###### Proof.

We proceed by induction on the structure of the formula $\zeta$. We firstly
prove that $\sigma(\zeta)=1\iff s_{\sigma}\vDash\zeta^{p}$ and
$\sigma(\zeta)=0\iff s_{\sigma}\vDash\zeta^{n}$.

  * •

If $\zeta=x_{i}$, we have

$\begin{array}[]{l@{\;\iff\;}l @{\hspace{4em}}
l@{\;\iff\;}l}\sigma(x_{i})=1&s_{\sigma}\vDash r_{i}\to p_{i}\hfil\hskip
40.00006pt&\sigma(x_{i})=0&s_{\sigma}\vDash r_{i}\to\neg p_{i}\\\
&s_{\sigma}\vDash(x_{i})^{p}\hfil\hskip
40.00006pt&&s_{\sigma}\vDash(x_{i})^{n}\end{array}$

  * •

If $\zeta=\neg x_{i}$, we have

$\begin{array}[]{l@{\;\iff\;}l @{\hspace{4em}} l@{\;\iff\;}l}\sigma(\neg
x_{i})=1&\sigma(x_{i})=0\hfil\hskip 40.00006pt&\sigma(\neg
x_{i})=0&\sigma(x_{i})=1\\\ &s_{\sigma}\vDash r_{i}\to\neg p_{i}\hfil\hskip
40.00006pt&&s_{\sigma}\vDash r_{i}\to p_{i}\\\ &s_{\sigma}\vDash(\neg
x_{i})^{p}\hfil\hskip 40.00006pt&&s_{\sigma}\vDash(\neg x_{i})^{n}\end{array}$

  * •

If $\zeta=\eta\land\xi$, we have

$\begin{array}[]{l@{}l @{\hspace{4em}}
l@{}l}&\sigma(\eta\land\xi)=1\hfil\hskip 40.00006pt&&\sigma(\eta\land\xi)=0\\\
&\;\iff\;\sigma(\eta)=\sigma(\xi)=1\hfil\hskip
40.00006pt&&\;\iff\;\sigma(\eta)=0\;\text{or}\;\sigma(\xi)=0\\\
&\;\iff\;s_{\sigma}\vDash\eta^{p}\land\xi^{p}\hfil\hskip
40.00006pt&&\;\iff\;s_{\sigma}\vDash\eta^{n}\;\text{or}\;s_{\sigma}\vDash\xi^{n}\\\
&\;\iff\;s_{\sigma}\vDash(\eta\land\xi)^{p}\hfil\hskip
40.00006pt&&\;\iff\;s_{\sigma}\vDash(\eta\land\xi)^{n}\end{array}$

  * •

If $\zeta=\eta\vee\xi$, we have

$\begin{array}[]{l@{}l @{\hspace{4em}} l@{}l}&\sigma(\eta\vee\xi)=1\hfil\hskip
40.00006pt&&\sigma(\eta\vee\xi)=0\\\
&\;\iff\;\sigma(\eta)=1\;\text{or}\;\sigma(\xi)=1\hfil\hskip
40.00006pt&&\;\iff\;\sigma(\eta)=\sigma(\xi)=0\\\
&\;\iff\;s_{\sigma}\vDash\eta^{p}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\xi^{p}\hfil\hskip
40.00006pt&&\;\iff\;s_{\sigma}\vDash\eta^{n}\land\xi^{n}\\\
&\;\iff\;s_{\sigma}\vDash(\eta\vee\xi)^{p}\hfil\hskip
40.00006pt&&\;\iff\;s_{\sigma}\vDash(\eta\vee\xi)^{n}\end{array}$

Secondly, we notice that:

$\displaystyle
s_{\sigma}\vDash\zeta^{p}\;\iff\;\sigma(\zeta)=1\;\iff\;\sigma(\zeta)\neq
0\;\iff\;s_{\sigma}\nvDash\zeta^{n}$ $\displaystyle
s_{\sigma}\vDash\zeta^{n}\;\iff\;\sigma(\zeta)=0\;\iff\;\sigma(\zeta)\neq
1\;\iff\;s_{\sigma}\nvDash\zeta^{p}$

This concludes the proof.

∎

Now we shift our attention to quantified Boolean formulas, and in particular
to the formulas $\theta_{k}:=Q_{k}x_{k}\dots Q_{l-1}x_{l-1}\zeta$. Notice that
the lower the value $k$, the more quantifiers appear in the formula
$\theta_{k}$, with the limit case being $\theta_{l}:=\zeta$.

As for propositional formulas we define two translations by mutual recursion.
The two translations are indicated with $\theta_{k}^{P}$ and $\theta_{k}^{N}$.
These translations involve the formulas $D_{i}$ and $S_{i}$ introduced in
Subsection 4.2.

$\begin{array}[]{lll}\zeta^{P}&=&\zeta^{p}\\\
\zeta^{N}&=&\zeta^{n}\\\\[1.99997pt]
\theta_{k-1}^{P}&=&\left\\{\begin{array}[]{ll}D_{k-1}\to\theta_{k}^{P}&\text{if}\;Q_{k-1}=\forall\\\
\left(D_{k-1}\to\theta_{k}^{N}\right)\to
S_{k}&\text{if}\;Q_{k-1}=\exists\end{array}\right.\\\\[10.00002pt]
\theta_{k-1}^{N}&=&\left\\{\begin{array}[]{ll}(D_{k-1}\to\theta_{k}^{P})\to
S_{k}&\text{if}\;Q_{k-1}=\forall\\\
D_{k-1}\to\theta_{k}^{N}&\text{if}\;Q_{k-1}=\exists\end{array}\right.\end{array}$

Similarly to the translations $\zeta^{p}$ and $\zeta^{n}$, we can prove a
preservation result for these translations.

######  Lemma 12.

Consider the quantified Boolean formula $\theta_{k}=Q_{k}x_{k}\dots
Q_{l-1}x_{l-1}\zeta$ with variables in $\mathrm{AP}_{l}$. Let
$\sigma:\mathrm{AP}_{k}\to\\{0,1\\}$ be a Boolean valuation and $s_{\sigma}$
the corresponding $k$-switching of $\mathcal{S}_{l}$. We have that:

$\begin{array}[]{l c
l}\sigma(\theta_{k})=1&\text{iff}&\mathcal{S}_{l},s_{\sigma}\vDash(\theta_{k})^{P}\\\
\sigma(\theta_{k})=0&\text{iff}&\mathcal{S}_{l},s_{\sigma}\vDash(\theta_{k})^{N}\end{array}$
(6)

###### Proof.

We prove the result by induction on the number of quantifiers preceding
$\zeta$. The base case is

$\begin{array}[]{l c
l}\sigma(\zeta)=1&\text{iff}&\mathcal{S}_{l},s_{\sigma}\vDash(\zeta)^{P}\\\
\sigma(\zeta)=0&\text{iff}&\mathcal{S}_{l},s_{\sigma}\vDash(\zeta)^{N}\end{array}$

and this is the statement of Lemma 11.

As for the inductive step, suppose the equivalences to hold for formulas with
$l-k-1$ quantifiers. We want to show that the equivalences hold also for
formulas with $l-k$ quantifiers. So consider the formula
$\theta_{k-1}=Q_{k-1}x_{k-1}\dots Q_{l-1}x_{l-1}\zeta$. As a useful shorthand,
we will write $Q_{k-1}x_{k-1}\theta_{k}$ for the formula $\theta_{k-1}$,
making explicit reference to the relation between the two formulas.

Let $\sigma:\mathrm{AP}_{k-1}\to\\{0,1\\}$ and $s_{\sigma}$ be as in the
statement of the lemma. We have two cases two consider, depending on whether
$Q_{k-1}=\forall$ or $Q_{k-1}=\exists$.

  * •

Suppose $Q_{k-1}=\forall$ and let us firstly focus on the first equivalence of
6. We have:

$\begin{array}[]{ll}&\mathcal{S}_{l},s_{\sigma}\vDash(\forall
x_{k-1}\theta_{k})^{P}\\\ \iff&\mathcal{S}_{l},s_{\sigma}\vDash
D_{k-1}\to\theta_{k}^{P}\\\ \iff&\text{For every $t\subseteq s_{\sigma}$, if
}\mathcal{S}_{l},t\vDash D_{k-1}\text{ then
}\mathcal{S}_{l},t\vDash\theta_{k}^{P}\end{array}$

By persistency of the logic (Proposition 4), we just need to check the
condition for the _maximal_ substates of $s_{\sigma}$ satisfying $D_{k-1}$. By
Lemma 9 these maximal substates are
$t^{+}=s_{\sigma}\setminus\\{w_{k-1}^{-}\\}$ and
$t^{-}=s_{\sigma}\setminus\\{w_{k-1}^{+}\\}$, which are both $k$-switchings
and substates of $s_{\sigma}$. These switchings correspond respectively to the
Boolean valuations $\tau^{+},\tau^{-}:\mathrm{AP}_{k}\to\\{0,1\\}$ defined as

$\begin{array}[]{ll}\tau^{+}(x_{i})=\left\\{\begin{array}[]{ll}\sigma(x_{i})&\text{if
}i<k\\\ 1&\text{if }i=k\end{array}\right.\\\\[10.00002pt]
\tau^{-}(x_{i})=\left\\{\begin{array}[]{ll}\sigma(x_{i})&\text{if }i<k\\\
0&\text{if }i=k\end{array}\right.\end{array}$

By inductive hypothesis, we have

$\begin{array}[]{l l
l}\mathcal{S}_{l},t^{+}\vDash\theta_{k}^{P}&\iff&\tau^{+}(\theta_{k})=1\\\
\mathcal{S}_{l},t^{-}\vDash\theta_{k}^{P}&\iff&\tau^{-}(\theta_{k})=1\end{array}$

So in conclusion we have

$\begin{array}[]{ll}&\mathcal{S}_{l},s_{\sigma}\vDash(\forall
x_{k-1}\theta_{k})^{P}\\\ \iff&\tau^{+}(\theta_{k})=\tau^{-}(\theta_{k})=1\\\
\iff&\sigma(\forall x_{k-1}\theta_{k})=\sigma(\theta_{k-1})=1\end{array}$

As for the second equivalence of 6, we have:

$\begin{array}[]{ll}&\mathcal{S}_{l},s_{\sigma}\vDash(\forall
x_{k-1}\theta_{k})^{N}\\\
\iff&\mathcal{S}_{l},s_{\sigma}\vDash(D_{k-1}\to\theta_{k}^{P})\to S_{k}\\\
\iff&\text{For every $t\subseteq s_{\sigma}$, if }\mathcal{S}_{l},t\vDash
D_{k-1}\to\theta_{k}^{P}\text{ then }\mathcal{S}_{l},t\vDash S_{k}\end{array}$

By Lemma 10, the only substate of $s_{\sigma}$ not satisfying $S_{k}$ is
$s_{\sigma}$ itself. So the chain of equivalences above can be extended as
follows:

$\begin{array}[]{ll}&\mathcal{S}_{l},s_{\sigma}\vDash(\forall
x_{k-1}\theta_{k})^{N}\\\ \iff&\mathcal{S}_{l},s_{\sigma}\nvDash
D_{k-1}\to\theta_{k}^{P}\\\ \iff&\text{For some $t\subseteq s_{\sigma}$,
}\mathcal{S}_{l},t\vDash D_{k-1}\text{ and
}\mathcal{S}_{l},t\nvDash\theta_{k}^{P}\\\
\stackrel{{\scriptstyle\ast}}{{\iff}}&\mathcal{S}_{l},t^{+}\nvDash\theta_{k}^{P}\text{
or }\mathcal{S}_{l},t^{-}\nvDash\theta_{k}^{P}\\\
\stackrel{{\scriptstyle\ast\ast}}{{\iff}}&\tau^{+}(\theta_{k})=0\text{ or
}\tau^{-}(\theta_{k})=0\\\ \iff&\sigma(\forall
x_{k-1}\theta_{k})=\sigma(\theta_{k-1})=0\end{array}$

where the equivalence $(\ast)$ follows by persistency and the equivalence
$(\ast\ast)$ follows by two applications of the inductive hypothesis applied
to the $k$-switchings $t^{+}$ and $t^{-}$ respectively.

  * •

Suppose $Q_{k}=\exists$. Most of the arguments and passages follow closely the
structure of the previous case, so we will omit comments to most of them.

Let us firstly focus on the first equivalence of 6. We have:

$\begin{array}[]{ll}&\mathcal{S}_{l},s_{\sigma}\vDash(\exists
x_{k-1}\theta_{k})^{P}\\\
\iff&\mathcal{S}_{l},s_{\sigma}\vDash(D_{k-1}\to\theta_{k}^{N})\to S_{k}\\\
\iff&\text{For every $t\subseteq s_{\sigma}$, if }\mathcal{S}_{l},t\vDash
D_{k-1}\to\theta_{k}^{N}\text{ then }\mathcal{S}_{l},t\vDash S_{k}\\\
\iff&\mathcal{S}_{l},s_{\sigma}\nvDash D_{k-1}\to\theta_{k}^{N}\\\
\iff&\text{For some $t\subseteq s_{\sigma}$, }\mathcal{S}_{l},t\vDash
D_{k-1}\text{ and }\mathcal{S}_{l},t\nvDash\theta_{k}^{N}\\\
\iff&\mathcal{S}_{l},t^{+}\nvDash\theta_{k}^{N}\text{ or
}\mathcal{S}_{l},t^{-}\nvDash\theta_{k}^{N}\\\
\stackrel{{\scriptstyle\ast}}{{\iff}}&\tau^{+}(\theta_{k})=1\text{ or
}\tau^{-}(\theta_{k})=1\\\ \iff&\sigma(\exists
x_{k-1}\theta_{k})=\sigma(\theta_{k-1})=1\end{array}$

where the equivalence $(\ast)$ follows by inductive hypothesis.

As for the second equivalence of 6, we have:

$\begin{array}[]{ll}&\mathcal{S}_{l},s_{\sigma}\vDash(\exists
x_{k-1}\theta_{k})^{N}\\\ \iff&\mathcal{S}_{l},s_{\sigma}\vDash
D_{k-1}\to\theta_{k}^{N}\\\ \iff&\text{For every $t\subseteq s_{\sigma}$, if
}\mathcal{S}_{l},t\vDash D_{k-1}\text{ then
}\mathcal{S}_{l},t\vDash\theta_{k}^{N}\\\
\iff&\mathcal{S}_{l},t^{+}\vDash\theta_{k}^{N}\text{ and
}\mathcal{S}_{l},t^{-}\vDash\theta_{k}^{N}\\\
\stackrel{{\scriptstyle\ast}}{{\iff}}&\tau^{+}(\theta_{k})=\tau^{-}(\theta_{k})=0\\\
\iff&\sigma(\exists x_{k-1}\theta_{k})=\sigma(\theta_{k-1})=0\end{array}$

where the equivalence $(\ast)$ follows from inductive hypothesis.

And this concludes the proof of the inductive step. Thus the result follows by
induction.

∎

As a direct corollary of the previous lemma we obtain the desired result: we
can reduce an instance of $\TQBF$ to an instance of $\MC(\mathsf{InqB})$.

######  Corollary 13.

Let $\theta:=Q_{0}x_{0}\dots Q_{l-1}x_{l-1}\zeta$ be a closed quantified
Boolean formula. Then $\theta$ is valid iff
$\mathcal{S}_{l},W_{l}\vDash\theta^{P}$. In other terms:

$\theta\in\TQBF\quad\text{iff}\quad\left\langle\mathcal{S}_{l},W_{l},\theta^{P}\right\rangle\in\MC(\mathsf{InqB})$

###### Proof.

Recall that the set $W_{l}$ of all the worlds of $\mathcal{S}_{l}$ is a
$0$-switching, and that the corresponding valuation is the empty function. By
Lemma 12 (applied for $k=0$) we have that $\theta$ is valid (i.e., satisfied
by the empty function) iff $\mathcal{S}_{l},W_{l}\vDash\theta^{P}$. ∎

###  4.4 Complexity

It remains to show that the reduction of $\TQBF$ to $\MC(\mathsf{InqB})$
presented in Corollary 13 is polynomially bounded in size. This entails that
$\MC(\mathsf{InqB})$ is a $\PSPACE$-hard problem, since so is $\TQBF$.

Let $\theta$ be the formula $Q_{0}x_{0}\dots Q_{l-1}x_{l-1}\zeta$ with
$\left|\zeta\right|=h$, and thus $\left|\theta\right|=\Theta(l+h)$. Using the
encoding of information models presented in Section 3, the size of
$\mathcal{S}_{l}$ is
$\left|\\{p_{0},\dots,p_{l-1},q_{0},\dots,q_{l-1}\\}\right|\cdot\left|W_{l}\right|=2l^{2}$,
which is indeed polynomially bounded by $l+h$. And the same goes for the
encoding of the information state $W_{l}$, which is of size $2l$.

As for the size of $\theta^{P}$, the computations are slightly more involved,
so we proceed one step at a time. Since there are several summations and an
inductive proof involved, the $\mathcal{O}$ notation may easily lead to
errors. For this reason, we firstly present a semi-formal analysis of the
complexity involving $\mathcal{O}$s in the current section, and we give a more
thorough analysis in Appendix A.

Firstly, we find bounds for the size of the special formulas presented in
Subsection 4.2. Recall that we indicate with $\left|\phi\right|$ the size of
the encoding of a formula $\phi$.

  * •

$\left|C^{+}_{k}\right|=\left|\;q_{k}\land
p_{k}\;\right|=\mathcal{O}(\log(l))$ and
$\left|C^{-}_{k}\right|=\left|\;q_{k}\land\neg
p_{k}\;\right|=\mathcal{O}(\log(l))$.

  * •

$\left|\neg C_{k}^{+}\land\neg C_{k}^{-}\right|=\left|\neg
C_{k}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{k}^{-}\right|=\mathcal{O}(\log(l))$.

  * •

$\left|S_{0}\right|=\mathcal{O}(l)+\sum_{i=0}^{l-1}\left|\neg
C^{+}_{i}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C^{-}_{i}\right|=\mathcal{O}(l)+\mathcal{O}(l\log(l))=\mathcal{O}(l\log(l))$.

  * •

For $k>0$ we have
$\left|S_{k}\right|=\mathcal{O}(l)+\sum_{i=0}^{k-1}\left|\neg
C_{i}^{+}\land\neg C_{i}^{-}\right|+\sum_{i=k}^{l-1}\left|\neg
C_{i}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{i}^{-}\right|=\mathcal{O}(l)+\mathcal{O}(k\log(l))+\mathcal{O}((l-k)\log(l))=\mathcal{O}(l\log(l))$.

  * •

$\left|D_{k}\right|=\left|\;q_{k}\to(p_{k}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
p_{k})\;\right|=\mathcal{O}(\log(l))$.

  * •

A straightforward inductive argument on the construction of $\zeta^{P}$
(resp., $\zeta^{N}$) shows that $\left|\zeta^{P}\right|=\mathcal{O}(h)$
(resp., $\left|\zeta^{N}\right|=\mathcal{O}(h)$).

And now we prove by (descending) induction on $k$ that
$\left|\theta_{k}^{P}\right|$ and $\left|\theta_{k}^{N}\right|$ are both in
$\mathcal{O}((l-k-1)l\log(l)+h)$. The base step of the induction $k=l$ (i.e.,
when there are no quantifiers involved and the formulas are $\zeta^{P}$ and
$\zeta^{N}$ respectively) was already considered. So assume that
$\left|\theta_{k}^{P}\right|$ and $\left|\theta_{k}^{N}\right|$ are both in
$\mathcal{O}((l-k-1)l\log(l)+h)$. We prove only that
$\left|\theta_{k-1}^{P}\right|$ is in $\mathcal{O}((l-k)l\log(l)+h)$, since
the other inequality follows similar computations. We consider two separate
cases, depending on whether $Q_{k-1}=\forall$ or $Q_{k-1}=\exists$.

$\begin{array}[]{ll}\left|(\forall
x_{k-1}\theta_{k})^{P}\right|&=\left|D_{k-1}\to\theta_{k}^{P}\right|\\\
&=\mathcal{O}(\log(l))+\mathcal{O}((l-k-1)l\log(l)+h)\\\
&=\mathcal{O}((l-k)l\log(l)+h)\end{array}$ $\begin{array}[]{ll}\left|(\exists
x_{k-1}\theta_{k})^{P}\right|&=\left|(D_{k-1}\to\theta_{k}^{N})\to
S_{k}\right|\\\
&=\mathcal{O}(l\log(l))+\mathcal{O}((l-k-1)l\log(l)+h)+\mathcal{O}(l\log(l))\\\
&=\mathcal{O}((l-k)l\log(l)+h)\end{array}$

And this concludes the inductive proof. The salient results we thus obtain are
the following.

######  Theorem 14.

For $\theta=Q_{0}x_{0}\dots Q_{l-1}x_{l-1}\zeta$ a closed quantified Boolean
formula, the size of $\theta^{P}$ is in
$\mathcal{O}(l^{2}\log(l)+\left|\zeta\right|)$. In particular, the size of the
translation is polynomially bounded by the size of the original formula.

######  Corollary 15.

The problem $\MC(\mathsf{InqB})$ is $\PSPACE$-hard.

As anticipated, this was the last ingredient needed to show that the four
problems considered are $\PSPACE$-complete.

######  Theorem 16.

The problems $\MC(\mathsf{InqB})$, $\MCanti(\mathsf{InqB})$,
$\MC(\mathsf{InqM})$ and $\MCanti(\mathsf{InqM})$ are $\PSPACE$-complete.

##  5 Conclusions

In this paper we formalized and studied the model checking problems
$\MC(\mathsf{InqB})$ and $\MC(\mathsf{InqM})$ for inquisitive propositional
logic and inquisitive modal logic, and studied their complexity. In Section 3
we provided an algorithm to solve the problem $\MC(\mathsf{InqM})$ and proved
its correctness. This allowed us to show that the complexity of the problem is
in the class $\PSPACE$. In Section 4 we provided a polynomial-space reduction
of the _true quantified Boolean formula_ problem to $\MC(\mathsf{InqB})$, thus
showing that the problem is also $\PSPACE$-hard. Putting these results
together, we inferred that both problems are $\PSPACE$-complete.

This paper is the first investigation of computational complexity issues for
inquisitive logics. A venue for further investigation is whether the proof
presented adapts to other inquisitive logics, such as _inquisitive epistemic
logic_ [1, Ch. 7], _inquisitive intuitionistic logic_ [2] or first-order
versions of the system such as $\mathsf{InqBQ}$ [1, Ch. 4].

## References

  * [1] Ivano Ciardelli.  Questions in logic.  PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, 2016.
  * [2] Ivano Ciardelli, Rosalie Iemhoff, and Fan Yang.  Questions and dependency in intuitionistic logic.  Notre Dame Journal of Formal Logic, 61(1):75–115, 2020.
  * [3] Ivano Ciardelli and Floris Roelofsen.  Inquisitive dynamic epistemic logic.  Synthese, 192(6):1643–1687, 2015.
  * [4] Edmund M. Clarke and Bernd-Holger Schlingloff.  Chapter 24 - model checking.  In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, Handbook of Automated Reasoning, pages 1635–1790. North-Holland, Amsterdam, 2001.
  * [5] Johannes Ebbing and Peter Lohmann.  Complexity of model checking for modal dependence logic.  In Mária Bieliková, Gerhard Friedrich, Georg Gottlob, Stefan Katzenbeisser, and György Turán, editors, SOFSEM 2012: Theory and Practice of Computer Science, pages 226–237, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
  * [6] Johannes Ebbing, Peter Lohmann, and Fan Yang.  Model checking for modal intuitionistic dependence logic.  In Guram Bezhanishvili, Sebastian Löbner, Vincenzo Marra, and Frank Richter, editors, Logic, Language, and Computation, pages 231–256, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.
  * [7] Michael Sipser.  Introduction to the Theory of Computation.  Course Technology, Boston, MA, third edition, 2013.
  * [8] Moshe Y. Vardi.  The complexity of relational query languages (extended abstract).  In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC ’82, pages 137–146, New York, NY, USA, 1982. Association for Computing Machinery.
  * [9] Fan Yang.  On extensions and variants of dependence logic: A study of intuitionistic connectives in the team semantics setting.  PhD thesis, University of Helsinki, 2014.
  * [10] Max Zeuner.  Model checking for inquisitive logic.  Master Thesis, Ludwig Maximilian University, 2020.

##  Appendix A Explicit analysis

In this appendix we give an explicit analysis of the computations presented at
the end of Section 4, leading to Theorem 14. Throughout this appendix, we
indicate with $c_{i}$ constants dependent only on the encoding used for
formulas, chosen opportunely to satisfy the inequalities involved.

Firstly, we give an explicit analysis of the sizes of the formulas presented
in Subsection 4.2.

  * •

$\left|C^{+}_{k}\right|=\left|\;q_{k}\land p_{k}\;\right|\leq c_{1}\log(l)$
and $\left|C^{-}_{k}\right|=\left|\;q_{k}\land\neg p_{k}\;\right|\leq
c_{1}\log(l)$.

  * •

$\left|\neg C_{i}^{+}\land\neg C_{i}^{-}\right|=\left|\neg
C_{i}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{i}^{-}\right|\leq c_{2}+\left|C_{i}^{+}\right|+\left|C_{i}^{-}\right|\leq
c_{3}\log(l)$.

  * •

$\left|S_{0}\right|\leq c_{4}l+\sum_{i=0}^{l-1}\left|\neg
C^{+}_{i}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C^{-}_{i}\right|\leq c_{4}l+l\cdot c_{2}\log(l)\leq c_{5}l\log(l)$.

  * •

For $k>0$ we have $\left|S_{k}\right|=c_{6}l+\sum_{i=0}^{k-1}\left|\neg
C_{i}^{+}\land\neg C_{i}^{-}\right|+\sum_{i=k}^{l-1}\left|\neg
C_{i}^{+}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
C_{i}^{-}\right|\leq c_{6}l+k\cdot c_{3}\log(l)+(l-k)\cdot c_{3}\log(l)\leq
c_{7}l\log(l)$.

  * •

To make computations less tedious, we define $c_{8}=\max(c_{5},c_{7})$, so
that $\left|S_{k}\right|\leq c_{8}l\log(l)$ independently from the value of
$k$.

  * •

$\left|D_{k}\right|=\left|\;q_{k}\to(p_{k}\operatorname*{\mathrel{\rotatebox[origin={c}]{270.0}{$\geqslant$}}}\neg
p_{k})\;\right|\leq c_{9}\log(l)$.

  * •

A straightforward inductive argument on the construction of $\zeta^{P}$
(resp., $\zeta^{N}$) shows that $\left|\zeta^{P}\right|=\mathcal{O}(h)$
(resp., $\left|\zeta^{N}\right|=\mathcal{O}(h)$).

Secondly, we provide an explicit analysis of the size of
$\left|(Q_{k}x_{k}\dots Q_{l-1}x_{l-1}\zeta)^{P}\right|$ and
$\left|(Q_{k}x_{k}\dots Q_{l-1}x_{l-1}\zeta)^{N}\right|$. As in Subsection 4.3
we use the shorthand $\theta_{k}:=Q_{k}x_{k}\dots Q_{l-1}x_{l-1}\zeta$, and
indicate with $Q_{k-1}x_{k-1}\theta_{k}$ the formula $\theta_{k-1}$ to make
the relation between the formulas $\theta_{k}$ and $\theta_{k-1}$ explicit. We
show by downward induction on $k$ that both quantities are bounded by
$c((l-k-1)l\log(l)+h)$ for an opportune choice of the constant $c$. The base
step of the induction ($k=l$, i.e., when no quantifiers are involved and the
the formulas considered are $\zeta^{P}$ and $\zeta^{N}$) has already been
taken care of. So assume that $\left|\theta_{k}^{P}\right|\leq
c((l-k)l\log(l)+h)$ and $\left|\theta_{k}^{N}\right|\leq c((l-k)l\log(l)+h)$.

As for the inductive step, we firstly prove the inequality
$\left|\theta_{k-1}^{P}\right|\leq c((l-(k-1))l\log(l)+h)$. We consider two
separate cases, depending on whether $Q_{k-1}=\forall$ or $Q_{k-1}=\exists$.

$\begin{array}[]{lll}\left|(\forall
x_{k-1}\theta_{k})^{P}\right|&=\left|D_{k-1}\to\theta_{k}^{P}\right|\\\ &\leq
c_{10}\log(l)+c((l-k)l\log(l)+h)\\\ &\leq c\log(l)+c(l-k)l\log(l)+ch&\text{(if
$c\geq c_{10}$)}\\\ &\leq c(\;(l-(k-1))l\log(l)+h\;)\end{array}$
$\begin{array}[]{lll}\left|(\exists
x_{k-1}\theta_{k})^{P}\right|&=\left|(D_{k-1}\to\theta_{k}^{N})\to
S_{k}\right|\\\ &\leq c_{11}l\log(l)+c((l-k)l\log(l)+h)\\\ &\leq
cl\log(l)+c(l-k)l\log(l)+ch&\text{(if $c\geq c_{11}$)}\\\ &\leq
c(\;(l-(k-1))l\log(l)+h\;)\end{array}$

Secondly we prove the inequality $\left|\theta_{k-1}^{N}\right|\leq
c((l-(k-1))l\log(l)+h)$. Also in this case we distinguish the cases
$Q_{k-1}=\forall$ and $Q_{k-1}=\exists$.

$\begin{array}[]{lll}\left|(\forall
x_{k-1}\theta_{k})^{N}\right|&=\left|(D_{k}\to\theta_{k}^{P})\to
S_{k}\right|\\\ &\leq c_{12}l\log(l)+c((l-k)l\log(l)+h)\\\ &\leq
cl\log(l)+c(l-k)l\log(l)+ch&\text{(if $c\geq c_{12}$)}\\\ &\leq
c(\;(l-(k-1))l\log(l)+h\;)\end{array}$ $\begin{array}[]{lll}\left|(\exists
x_{k-1}\theta_{k})^{N}\right|&=\left|D_{k}\to\theta_{k}^{N}\right|\\\ &\leq
c_{13}\log(l)+c((l-k)l\log(l)+h)\\\ &\leq c\log(l)+c(l-k)l\log(l)+ch&\text{(if
$c\geq c_{13}$)}\\\ &\leq c(\;(l-(k-1))l\log(l)+h\;)\end{array}$

So by choosing $c:=\max(c_{10},c_{11},c_{12},c_{13})$ we meet all the
conditions necessary for the inequality to hold. This concludes our inductive
proof, and shows that both $\left|\theta_{k}^{P}\right|$ and
$\left|\theta_{k}^{N}\right|$ are in $\mathcal{O}(((l-k)l\log(l)+h))$, as
desired.