Structural Completeness and Superintuitionistic Inquisitive Logics

Abstract

In this paper, the notion of structural completeness is explored in the context of a generalized class of superintuitionistic logics involving also systems that are not closed under uniform substitution. We just require that each logic must be closed under D-substitutions assigning to atomic formulas only $\vee$-free formulas. For these systems we introduce four different notions of structural completeness and study how they are related. We focus on superintuitionistic inquisitive logics that validate a schema called Split and have the disjunction property. In these logics disjunction can be interpreted in the sense of inquisitive semantics as a question forming operator. It is shown that a logic is structurally complete with respect to D-substitutions if and only if it includes the weakest superintuitionistic inquisitive logic. Various consequences of this result are explored. For example, it is shown that every superintuitionistic inquisitive logic can be characterized by a Kripke model built up from D-substitutions. Additionally, we resolve a conjecture concerning superintuitionistic inquisitive logics due to Miglioli et al..

1 Introduction

The property of structural completeness of a logic $\varLambda$ is satisfied when every rule admissible in $\varLambda$ is also derivable in $\varLambda$. Since its introduction by Pogorzelski [25], the property has been studied in a number of contexts, e.g. in substructural logics in [24] or fuzzy logics in [8], but most exhaustively in the context of superintuitionistic (also known as intermediate) logics (e.g. in [9, 10]).

Research on structural completeness has largely assumed the requirement of closure under uniform substitutions. A notable exception to this requirement is found in inquisitive logic [6]. Inquisitive logic makes up a framework in which declarative propositions (asserting information) are distinguished from inquisitive propositions (in which a question is posed). In order to preserve the distinction, uniform substitution must be relaxed.

As [28] documents, there is an interesting class of superintuitionistic inquisitive logics that inhabit the space of theories extending intuitionistic logic but are not closed under all substitutions. Both [22] and [20] touch on properties concerning structural completeness relevant to inquisitive logics. [22] considers variants of structural completeness over a wide range of theories in which substitutivity might fail, emphasizing two particular inquisitive logics, while [20] considers the inquisitive logic $\textsf{InqB}$ among related systems of logics of dependency. While both studies have lessons for the structure of inquisitive logics, neither focuses on the whole class of these logics.

In what follows, we investigate structural completeness from the perspective of intuitionistic inquisitive logic and its extensions. Several interesting facts become clear from this standpoint, including the fact that all superintuitionistic inquisitive logics enjoy a property of hereditary structural completeness and that hereditary structural completeness coincides with structural completeness simpliciter in the space of extensions of intuitionistic inquisitive logic. We apply these results to expose a relationship with extensions of Gödel-Dummett logic $\textsf{LC}$ and to explore the features of Kripke models for inquisitive logics built from substitutions. Along the way, we resolve a two-part conjecture concerning inquisitive logics due to Miglioli et al. made in [22].

2 Intuitionistic Inquisitive Logic and Its Extensions

The standard inquisitive logic [2,3,4, 6] is based on an “information-based” semantics for classical logic that allows us to add to the language and characterize semantically some question forming operators, like inquisitive disjunction on the propositional level and an inquisitive existential quantifier on the first-order level. Since we will focus in this paper on the propositional level, we will be concerned only with inquisitive disjunction. This operator, when applied to statements $S_1, S_2$, forms the question whether $S_1$ or $S_2$, which can be contrasted with the statement that $S_1$ or $S_2$. Interestingly, this construction can be embedded under other operators, thus allowing one to form, for example, conjunctive questions and conditional questions. It is also possible to form disjunctive questions with more than two alternatives (whether $S_1$, $S_2$, or $S_3$, and so on), and polar (yes/no) questions as a special kind of disjunctive question (whether $S_1$ or not $S_1$).

Inquisitive disjunction has some constructive features and resembles intuitionistic disjunction, though, as we will see, it is not identical with it. Standard inquisitive logic can thus be viewed as classical logic extended with this constructive operator. It is possible to vary almost arbitrarily the background logic of declarative sentences, while keeping fixed the most characteristic features of inquisitive semantics. In this way we obtain non-classical inquisitive logics. A general semantic and syntactic theory of these logics is developed in [30]. An important example of such a logic is intuitionistic inquisitive logic [5, 28, 31]. It can be presented in two different ways. One can take the standard language of intuitionistic logic and add inquisitive disjunction to this language (as in [5, 29]). Alternatively, one can work just with the standard language involving only one disjunction, which is however interpreted in the inquisitive way (as in [2, 6, 31]). In this paper we will take the latter approach, which has the advantage that the axiomatization of the corresponding logic is much simpler and more elegant, and it can be compared directly with other logical systems in the same language that have been already studied in the literature on superintuitionistic logics. But the main reason for the decision to work with only one disjunction is that our main results concerning structural completeness hold only for this restricted language and they cease to be valid if the second disjunction is added. So, in this paper we will work with this basic language:

$$\begin{aligned} \varphi \,\,{:}{:}\!\!= p \mid \bot \mid \varphi \rightarrow \varphi \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \end{aligned}$$

where $\vee$ will be viewed as inquisitive disjunction. Negation, equivalence and a constant for validity are defined in the following usual way: $\lnot \varphi =_{def} \varphi \rightarrow \bot$, $\varphi \leftrightarrow \psi =_{def} (\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \varphi )$, $\top =_{def} \bot \rightarrow \bot$.

Fix any Hilbert style axiomatization of intuitionistic logic in this language, which has modus ponens as the only rule of inference. Let $\textsf{IL}$ denote the set of its derivable formulas. We write $\vdash _{\textsf{IL}} \varphi$ instead of $\varphi \in \textsf{IL}$, $\varphi \vdash _{\textsf{IL}} \psi$ instead of $\varphi \rightarrow \psi \in \textsf{IL}$, and $\varphi \equiv _{\textsf{IL}} \psi$ instead of $\varphi \leftrightarrow \psi \in \textsf{IL}$. (The same notation will be used also for other logics).

An axiomatization of intuitionistic inquisitive logic is obtained by extending the system for intuitionistic logic with the following schema called Split:

$$\begin{aligned} (\alpha \rightarrow (\psi \vee \chi )) \rightarrow ((\alpha \rightarrow \psi ) \vee (\alpha \rightarrow \chi )), \end{aligned}$$

where $\alpha$ ranges over $\vee$-free formulas.¹ The set of derivable formulas will be denoted as $\textsf{InqIL}$. The Split schema can be viewed as a piece that is missing in intuitionistic logic in order to prove inductively the following disjunctive form theorem, which is a cornerstone of propositional inquisitive logic that has been proved and used for many of its incarnations.

Theorem 1

For any formula $\varphi$ there are $\vee$-free formulas $\alpha _1, \ldots , \alpha _n$ such that

$$\begin{aligned} \varphi \equiv _{\textsf{InqIL}} \alpha _1 \vee \ldots \vee \alpha _n. \end{aligned}$$

Proof

One can proceed by induction. We show just the inductive step for implication. Assume that $\psi \equiv _{\textsf{InqIL}} \beta _1 \vee \ldots \vee \beta _m$ and $\chi \equiv _{\textsf{InqIL}} \gamma _1 \vee \ldots \vee \gamma _n$. Let $I=\{1, \ldots , m\}$ and $J=\{1, \ldots , n\}$. Then (using Split in the equivalence between the second and the third line):

$$\begin{array}{lll} \psi \rightarrow \chi &{} \equiv _{\textsf{InqIL}} &{} \bigvee \nolimits _{i \in I} \beta _i \rightarrow \bigvee \nolimits _{j \in J} \gamma _j \\[3pt] &{} \equiv _{\textsf{InqIL}} &{} \bigwedge \nolimits _{i \in I} (\beta _i \rightarrow \bigvee \nolimits _{j \in J} \gamma _j) \\[3pt] &{} \equiv _{\textsf{InqIL}} &{} \bigwedge \nolimits _{i \in I} \bigvee \nolimits _{j \in J} (\beta _i \rightarrow \gamma _j) \\[3pt] &{} \equiv _{\textsf{InqIL}} &{} \bigvee \nolimits _{f \in I \rightarrow J} \bigwedge \nolimits _{i \in I} (\beta _i \rightarrow \gamma _{f(i)}). \end{array} $$

   $\square$

The Split schema can be formulated in a stronger form, using the notion of a Harrop formula. A formula is called a Harrop formula if disjunction occurs in it only within antecedents of implications. So, the only allowed occurrences of disjunction are in the following context: $( \ldots ((\ldots \vee \ldots ) \rightarrow \ldots ) \ldots )$. It can be observed that for every Harrop formula $\varphi$ there is a $\vee$-free formula $\alpha$ such that $\varphi \equiv _{\textsf{InqIL}} \alpha$. To see this, assume that $\varphi$ contains a subformula $\psi \rightarrow \chi$. The antecedent $\psi$ may possibly involve a disjunction but all such disjunctions can be eliminated, since, according to Theorem 1, there are $\vee$-free formulas $\beta _1, \ldots , \beta _n$ such that $\psi \equiv _{\textsf{InqIL}} \beta _1 \vee \ldots \vee \beta _m$, and so $\psi \rightarrow \chi \equiv _{\textsf{InqIL}} \bigvee _i \beta _i \rightarrow \chi \equiv _{\textsf{InqIL}} \bigwedge _i (\beta _i \rightarrow \chi )$. As a consequence of this observation, $\textsf{InqIL}$ can be equivalently axiomatized by extending intuitionistic logic with the schema that we can call H-Split and which is like Split except that $\alpha$ ranges over arbitrary Harrop formulas.

Nevertheless, the restriction on the antecedents in Split (or H-Split) is important and cannot be completely avoided. Not all substitutional instances of Split hold in $\textsf{InqIL}$. For example, $((p \vee q) \rightarrow (p \vee q)) \rightarrow (((p \vee q) \rightarrow p) \vee ((p \vee q) \rightarrow q)) \notin \textsf{InqIL}$. In this respect, $\textsf{InqIL}$ is an unusual logic because it is not closed under uniform substitution. This fact is however well-motivated, given that the logic deals with two different categories of propositions, statements and questions. Questions are generated only by the inquisitive operator, and so every $\vee$-free formula represents a statement. It is not surprising that questions behave differently, and in some contexts cannot be substituted for statements.

In this paper, we want to explore $\textsf{InqIL}$ within the context of superintuitionistic logics. However, since superintuitionistic logics are required to be closed under uniform substitution, we need to introduce a more general notion, that will encompass also $\textsf{InqIL}$ (and other inquisitive logics). For this purpose, we use the following definitions.

Definition 1

A substitution is a function that assigns a formula to each atomic formula. An H-substitution is a substitution that assigns to each atomic formula a Harrop formula. A D-substitution is a substitution that assigns to each atomic formula a $\vee$-free formula.² If s is a substitution and $\varphi$ is a formula then $s(\varphi )$ denotes the formula that is obtained from $\varphi$ by replacing simultaneously every occurrence of each atomic formula p in $\varphi$ with the formula s(p).

Definition 2

A gsi-logic (generalized superintuitionistic logic) is any set of formulas which (a) contains all intuitionistically valid formulas; (b) does not contain $\bot$; (c) is closed under every D-substitution; (d) is closed under modus ponens.³ A gsi-logic is standard if it is closed under every substitution.

Note that the notion of a standard gsi-logic coincides with the standard notion of a superintuitionistic logic. Next we define, in accordance with [31], the notion of an inquisitive gsi-logic.

Definition 3

We say that a gsi-logic $\varLambda$ is inquisitive if it (a) contains all instances of Split, and (b) has the disjunction property, i.e. $\alpha \vee \beta \in \varLambda$ only if $\alpha \in \varLambda$ or $\beta \in \varLambda$. Instead of saying that a gsi-logic $\varLambda$ contains all instances of Split we will sometimes say that Split is valid in $\varLambda$.

It is clear that $\textsf{InqIL}$ is a gsi-logic, though not standard. Another example of a non-standard gsi-logic is the classical inquisitive logic, often called basic inquisitive logic and denoted as $\textsf{InqB}$ (see [3]), which can be obtained by adding to $\textsf{InqIL}$ the restricted double negation law DN: $\lnot \lnot \alpha \rightarrow \alpha$, where $\alpha$ ranges over $\vee$-free (or, equivalently, Harrop) formulas. Note that the $\vee$-free fragment of $\textsf{InqB}$ is identical with classical logic, while it can be shown that the $\vee$-free fragment of $\textsf{InqIL}$ is identical with (the $\vee$-free fragment of) intuitionistic logic.

It can also be shown that both $\textsf{InqIL}$ and $\textsf{InqB}$ have the disjunction property and thus are inquisitive also according to our general definition. In fact, $\textsf{InqIL}$ is the weakest and $\textsf{InqB}$ the strongest inquisitive gsi-logic. No inquisitive gsi-logic is standard. However, for any standard gsi-logic $\varLambda$ there is exactly one inquisitive gsi-logic that conservatively extends the $\vee$-free fragment of $\varLambda$. As a consequence, there are uncountably many inquisitive gsi-logics. For a justification of these claims, see [28], where inquisitive gsi-logics are called G-logics.

To the best of our knowledge, $\textsf{InqIL}$ and $\textsf{InqB}$ were both studied for the first time in [22], under the names $\mathsf {F_{int}}$ and $\mathsf {F_{cl}}$, where it was proved, for instance, that the schematic fragment of $\textsf{InqB}$ (called the standardization of $\mathsf {F_{cl}}$ in [22]), i.e. the set $S(\textsf{InqB})=\{\varphi \mid s(\varphi ) \in \textsf{InqB}, \text { for every substitution s} \}$, is identical with Medvedev’s logic of finite problems $\textsf{ML}$. Interestingly, the same was stated without proof also for $\textsf{InqIL}$. That this quite non-trivial claim is true follows from the main result of [17].

The system of $\textsf{InqB}$ was later rediscovered in [2, 6] and proved to be sound and complete with respect to the modern version of inquisitive semantics. This logic was applied to linguistic phenomena (see [4] for an overview) but also studied from algebraic and topological perspectives [1, 13, 34]. There is also an extensive literature on various modal extensions of $\textsf{InqB}$ [7, 14, 15, 27, 32].

A generalization of inquisitive semantics that corresponds to $\textsf{InqIL}$ was introduced in [28]. Intuitionistic inquisitive logic was further studied in [5, 29, 35], and from an algebraic perspective in [31, 33]. A slightly different approach to intuitionistic inquisitive logic was proposed in [18]. This approach is based on a more general framework that does not validate Split.

A recent interesting result also shows that the system of $\textsf{InqIL}$ provides a sound and complete axiomatization of proof-theoretic semantics [36]. This connection to proof-theoretic semantics nicely stresses the significance of this logic.

3 Structural Completeness

In this section, we show that the Split schema is quite intimately connected to the notion of structural completeness. Structural completeness is usually studied in relation to logics that are closed under arbitrary substitutions. For a more general notion of a logic we need a more flexible notion of structural completeness. In particular, we can consider various kinds of structural completeness defined in terms of some restricted classes of substitutions. Such notions were studied in depth in [22] and they were employed also in [20] where it was shown that $\textsf{InqB}$ and some related propositional dependence logics are structurally complete with respect to a suitably adapted sense of the term. In [22], the authors considered, besides other options, structural completeness defined in terms of H-substitutions and they called the corresponding notion H-smoothness. We will call it SH-completeness. Besides that we introduce three other notions of structural completeness.

Definition 4

Let $\varLambda$ be a gsi-logic. By $sub(\varLambda )$ we denote the set of all substitutions under which $\varLambda$ is closed, i.e., $s \in sub(\varLambda )$ iff $s(\varphi ) \in \varLambda$, for every $\varphi \in \varLambda$. We say that $\varLambda$ is SF-complete (structurally fully complete) if it holds:

• $\varphi \vdash _{\varLambda } \psi$ iff for any substitution s, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$.

We say that $\varLambda$ is SG-complete (structurally generally complete) if it holds:

• $\varphi \vdash _{\varLambda } \psi$ iff for any $s \in sub(\varLambda )$, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$.

We say that $\varLambda$ is SH-complete (structurally Harrop complete) if it holds:

• $\varphi \vdash _{\varLambda } \psi$ iff for any H-substitution s, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$.

We say that $\varLambda$ is SD-complete (structurally declaratively complete) if it holds:

• $\varphi \vdash _{\varLambda } \psi$ iff for any D-substitution s, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$.

We say that $\varLambda$ is hereditarily SF-complete (SG-complete, SH-complete, SD-complete) if every gsi-logic $\varLambda ' \supseteq \varLambda$ is SF-complete (SG-complete, SH-complete, SD-complete).

Note that the notions of SF-completeness and SG-completeness both generalize, in a clear sense, the standard notion of structural completeness. For standard gsi-logics both these notions are equivalent and coincide with the usual notion that is restricted to this field. Even though the notion of SF-completeness preserves the literal formulation of the usual definition and just applies it to a broader context, we think that SG-completeness provides a more natural generalization of structural completeness. This should be clear from the following observation that indicates that the notion of SF-completeness is reasonably applicable only to standard gsi-logics. We can also immediately observe that SD-completeness is also stronger than SG-completeness.

Proposition 1

Let $\varLambda$ be a gsi-logic. Then (a) if $\varLambda$ is SD-complete then it is SG-complete; (b) $\varLambda$ is SF-complete if and only if it is standard and SG-complete.

Proof

(a) Assume that $\varLambda$ is SD-complete. Obviously, if $\varphi \vdash _{\varLambda } \psi$ then for any $s \in sub(\varLambda )$, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$. For the opposite direction, assume that for any $s \in sub(\varLambda )$, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$. Then also for any D-substitution s, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$, and thus $\varphi \vdash _{\varLambda } \psi$.

(b) Assume that $\varLambda$ is SF-complete and $\vdash _{\varLambda } \varphi$. Then also $\vdash _{\varLambda } \top \rightarrow \varphi$. Take any substitution s. Since $\vdash _{\varLambda } s(\top )$, by SF-completeness we obtain $\vdash _{\varLambda } s(\varphi )$. We have shown that SF-complete gsi-logics are standard. The rest follows from the observation that for standard gsi-logics the notions of SF-completeness and SG-completeness coincide.    $\square$

Our aim in this section is to show that Split is closely related to SH-completeness and SD-completeness. Through this connection we will also be able to see that these two notions of structural completeness are in fact equivalent. First we can observe the following.

Proposition 2

Every gsi-logic in which Split is valid is closed under all H-substitutions.

Proof

Assume that $\varLambda$ is a gsi-logic in which Split is valid and take any H-substitution s. We have already observed that Split guarantees that every Harrop formula is equivalent to a $\vee$-free formula. In particular, for any p there is a $\vee$-free formula $\alpha _p$ such that $s(p) \equiv _{\varLambda } \alpha _p$. Now we can define a D-substitution $s^*$ fixing $s^*(p)=\alpha _p$, for each atomic p. If $\vdash _{\varLambda } \varphi$ then also $\vdash _{\varLambda } s^*(\varphi )$, since $\varLambda$ is closed under D-substitutions. It follows that also $\vdash _{\varLambda } s(\varphi )$.    $\square$

Let $\varLambda$ be a gsi-logic that validates Split. Proposition 2 says that if s is an H-substitution then $s \in sub(\varLambda )$. One can ask whether also the converse holds. If we formulate the converse directly, it is false for trivial reasons. If a substitution s assigns formulas that are not Harrop but are all equivalent to Harrop formulas then $\varLambda$ must be closed also under s. A more interesting question is whether $\varLambda$ may be closed also under substitutions that are not equivalent to any H-substitution. Let us formulate it more precisely. We say that two substitutions, s and t, are $\varLambda$-equivalent if $s(p) \equiv _{\varLambda } t(p)$, for every atomic formula p. Then the converse of Proposition 2 would state that if $s \in sub(\varLambda )$ then s is $\varLambda$-equivalent to an H-substitution. Interestingly, this is a property that distinguishes $\textsf{InqIL}$ and $\textsf{InqB}$.

Proposition 3

Every $s \in sub(\textsf{InqB})$ is $\textsf{InqB}$-equivalent to an H-substitution (and even D-substitution). In contrast, there is an $s \in sub(\textsf{InqIL})$ that is not $\textsf{InqIL}$-equivalent to any H-substitution.

Proof

For the first part, let s be a substitution under which $\textsf{InqB}$ is closed and let p be an arbitrary atomic formula. Then as $\textsf{InqB}$ proves $\lnot \lnot p\leftrightarrow p$, we obtain $\lnot \lnot s(p)\equiv _{\textsf{InqB}} s(p)$. Also, by Theorem 1, $s(p) \equiv _{\textsf{InqB}} \alpha _{1}\vee \ldots \vee \alpha _{n}$, where each $\alpha _{i}$ is $\vee$-free, whence $s(p) \equiv _{\textsf{InqB}}\lnot \lnot (\alpha _{1}\vee \ldots \vee \alpha _{n})$. But as $(\lnot \varphi \wedge \lnot \psi )\leftrightarrow \lnot (\varphi \vee \psi )$ holds intuitionistically, $s(p) \equiv _{\textsf{InqB}}\lnot (\lnot \alpha _{1}\wedge \ldots \wedge \lnot \alpha _{n})$, where $\lnot (\lnot \alpha _{1}\wedge \ldots \wedge \lnot \alpha _{n})$ is $\vee$-free and thus Harrop.

For the second part of the proposition, fix an atomic formula p and take the substitution s that assigns to every atomic formula the formula $p \vee \lnot p$. Assume, for the sake of contradiction, that $p \vee \lnot p \equiv _{\textsf{InqIL}} \alpha$, for some Harrop formula $\alpha$. Then, by Split and disjunction property, we would obtain $\vdash _{\textsf{InqIL}} \alpha \rightarrow p$ or $\vdash _{\textsf{InqIL}} \alpha \rightarrow \lnot p$, and thus $\vdash _{\textsf{InqIL}} (p \vee \lnot p) \rightarrow p$ or $\vdash _{\textsf{InqIL}} (p \vee \lnot p) \rightarrow \lnot p$. This leads to a contradiction because none of these formulas is valid in classical logic which extends $\textsf{InqIL}$. So, s is not $\textsf{InqIL}$-equivalent to any H-substitution.

It remains to be shown that $s \in sub(\textsf{InqIL})$. In order to show that a logic generated by modus ponens from a set of axioms is closed under a substitution s, it is sufficient to show that $s(\chi )$ is provable for every axiom $\chi$. So, we have to show $\vdash _{\textsf{InqIL}} s(\chi )$, for our specific s and every instance $\chi$ of Split. First, observe that for every formula $\chi$, $s(\chi )$ is intuitionistically equivalent to one of these formulas: $\bot , p \vee \lnot p, \top$. To see this, note that $\bot$ and $\top$ are generated from $p \vee \lnot p$ by negation and the set $\{\bot , p \vee \lnot p, \top \}$ is, up to intuitionistic equivalence, closed under the operations $\rightarrow , \wedge , \vee$. But then, if $s(\alpha ), s(\varphi ), s(\psi )$ are intuitionistically equivalent to any of the formulas $\bot , p \vee \lnot p, \top$, the formula

$$\begin{aligned} (s(\alpha ) \rightarrow (s(\varphi ) \vee s(\psi ))) \rightarrow ((s(\alpha ) \rightarrow s(\varphi )) \vee (s(\alpha ) \rightarrow s(\varphi ))) \end{aligned}$$

is intuitionistically valid. Hence, if we apply s to any instance of Split we always obtain a formula that is valid in $\textsf{InqIL}$.    $\square$

Proposition 3 shows that H-substitutions do not necessarily cover the space of all substitutions under which a logic validating Split is closed. Nevertheless, it will be clear from our main result, Theorem 2 below, that these substitutions play a special role in these logics.

We will rely heavily on a standard technique of proving structural completeness developed by Prucnal [26], or more precisely, on its refinement introduced later in [23]. Let $\alpha$ be a Harrop formula such that $\nvdash _{\textsf{IL}} \lnot \alpha$. Then there is a classical valuation v such that $v(\alpha )=1$. Following [23], we define, relative to $\alpha$ and v, the following H-substitution:

$$ s_{\alpha }^{v}(p) = {\left\{ \begin{array}{ll} \alpha \rightarrow p &{} \text {if }v(p)=1 \\ \lnot \lnot \alpha \wedge (\alpha \rightarrow p) &{} \text {otherwise} \end{array}\right. } $$

Note that if $\alpha$ is a $\vee$-free formula, then $s_{\alpha }^{v}$ is a D-substitution.

Lemma 1

Let $\varphi$ be any formula, $\alpha , \beta$ Harrop formulas, and v a classical valuation such that $v(\beta )=1$. Then (a) $s_{\alpha }^{v}(\varphi ) \vdash _{\textsf{IL}} \alpha \rightarrow \varphi$; (b) $s_{\alpha }^{v}(\beta ) \equiv _{\textsf{IL}} \alpha \rightarrow \beta$.

For a proof of this crucial result, see [23]. Note that, as a direct consequence of Lemma 1-b, it holds that if $\alpha$ is a Harrop formula, and $v(\alpha )=1$ then $\vdash _{\textsf{IL}} s_{\alpha }^{v}(\alpha )$. This lemma implies the following one that generalizes the main result of [23], which was originally formulated for standard gsi-logics.

Lemma 2

Let $\varLambda$ be a gsi-logic, $\psi , \chi$ any formulas, and $\alpha$ a Harrop formula. Then if $\alpha \rightarrow (\psi \vee \chi ) \in \varLambda$ then $(\alpha \rightarrow \psi ) \vee (\alpha \rightarrow \chi ) \in \varLambda$.

Proof

Assume $\alpha \rightarrow (\psi \vee \chi ) \in \varLambda$. We want to prove $(\alpha \rightarrow \psi ) \vee (\alpha \rightarrow \chi ) \in \varLambda$. If $\lnot \alpha \in \varLambda$ then the required conclusion is immediate. Assume $\lnot \alpha \notin \varLambda$. Then, due to Glivenko’s theorem, $\lnot \alpha$ is not classically valid and so there is a valuation v such that $v(\alpha )=1$. Then, by Lemma 1-b, $s_{\alpha }^{v}(\alpha ) \in \varLambda$. Since $\varLambda$ is closed under H-substitutions, $s_{\alpha }^{v}(\alpha ) \rightarrow (s_{\alpha }^{v}(\psi ) \vee s_{\alpha }^{v}(\chi )) \in \varLambda$, and hence also $s_{\alpha }^{v}(\psi ) \vee s_{\alpha }^{v}(\chi ) \in \varLambda$. Thus, by Lemma 1-a, $(\alpha \rightarrow \psi ) \vee (\alpha \rightarrow \chi ) \in \varLambda$.    $\square$

The previous lemma plays a crucial role in the proof of one part of the next theorem which is our main result relating Split with the notions of SH-completeness and SD-completeness.

Theorem 2

For every gsi-logic $\varLambda$ the following claims are equivalent: (a) $\varLambda$ is SH-complete; (b) $\varLambda$ is SD-complete; (c) Split is valid in $\varLambda$.

Proof

First, assume that $\varLambda$ is SH-complete. Let $\alpha$ be a $\vee$-free formula and $\varphi , \psi$ arbitrary formulas. By Lemma 2, for any H-substitution s, if $s(\alpha \rightarrow (\psi \vee \chi )) \in \varLambda$ then $s((\alpha \rightarrow \psi ) \vee (\alpha \rightarrow \chi )) \in \varLambda$. It follows from SH-completeness that Split is valid in $\varLambda$. In the same way, one can prove that SD-completeness implies the validity of Split.

Second, assume that Split is valid in $\varLambda$. We show that $\varphi \vdash _{\varLambda } \psi$ iff for any H-substitution s, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$. The left-to-right direction follows immediately from Proposition 2. We prove the right-to-left direction. Assume that

• (i) for any H-substitution s, if $\vdash _{\varLambda } s(\varphi )$ then $\vdash _{\varLambda } s(\psi )$.

We have to show that $\varphi \vdash _{\varLambda } \psi$. If $\vdash _{\varLambda } \lnot \varphi$, we are done, so we can assume that $\nvdash _{\varLambda } \lnot \varphi$. As Split is valid in $\varLambda$, we can take, due to the disjunctive form theorem, Harrop formulas $\alpha _1, \ldots , \alpha _n$ such that

• (ii) $\varphi \equiv _{\varLambda } \alpha _1 \vee \ldots \vee \alpha _n$.

Let us assume that the disjunction is minimal, i.e. $\varphi$ is not equivalent with the disjunction of any proper subset of $\{\alpha _1, \ldots , \alpha _n \}$. It follows that for every $\alpha _i$ ($1\le i \le n$), $\nvdash _{\textsf{IL}} \lnot \alpha _i$ (otherwise the disjunction in (ii) would not be minimal). Thus, due to Glivenko’s theorem, for each $1\le i \le n$, $\nvdash _{\textsf{CL}} \lnot \alpha _i$, and so there is a classical valuation $v_i$ such that $v_i(\alpha _i)=1$. Then the following holds:

• 1. $\vdash _{\varLambda } s^{v_i}_{\alpha _{i}} (\alpha _i)$ (by Lemma 1-b),

• 2. $\vdash _{\varLambda } s^{v_i}_{\alpha _{i}} (\alpha _i) \rightarrow s^{v_i}_{\alpha _{i}} (\varphi )$ (since $\varLambda$ is closed under H-substitutions),

• 3. $\vdash _{\varLambda } s^{v_i}_{\alpha _{i}} (\varphi )$ (from 1. and 2.),

• 4. $\vdash _{\varLambda } s^{v_i}_{\alpha _{i}} (\psi )$ (from 3. and the assumption (i)),

• 5. $s^{v_i}_{\alpha _{i}} (\psi ) \vdash _{\varLambda } \alpha _i \rightarrow \psi$ (by Lemma 1-a),

• 6. $\alpha _i \vdash _{\varLambda } \psi$ (from 4. and 5.).

Since the last point holds for any $1\le i \le n$ we obtain $\varphi \vdash _{\varLambda } \psi$ as required. In the same way, one can prove that the validity of Split implies that the logic is SD-complete.   $\square$

In the rest of this paper, we will explore some consequences of this result. The first one is immediate and it shows an interesting difference between SF-completeness/SG-completeness (on the one hand) and SH-completeness/SD-completeness (on the other).

Corollary 1

Every SH-complete (SD-complete) gsi-logic is hereditarily SH-complete (SD-complete).

In contrast to this corollary, there are examples of gsi-logics that are SF- and SG-complete but neither hereditarily SF-complete nor hereditarily SG-complete. For instance, the logic of finite problems $\textsf{ML}$ has this property (see [9, 12]). The next corollary is based on the observation that SD-completeness is a stronger property than SG-completeness.

Corollary 2

$\textsf{InqIL}$ is hereditarily SG-complete.

In other words, every gsi-logic that validates Split is SG-complete. The converse does not hold. $\textsf{ML}$ does not validate Split but it is SG-complete.

The relations between different kinds of structural completeness are summarized in the following picture:

$\textsf{ML}$ is a counterexample to $SF \Longrightarrow SD(H)$ and $SG \Longrightarrow SD(H)$, and any inquisitive gsi-logic is a counterexample to $SD(H) \Longrightarrow SF$ and $SG \Longrightarrow SF$.

4 Schematic Closures of Inquisitive Gsi-Logics

In this section we discuss some issues concerning SF-completeness and for this purpose we employ the following notation. If $\varLambda$ is a gsi-logic and $\varDelta$ a set of formulas then $\varLambda \oplus \varDelta$ will denote the set of formulas derivable from $\varLambda \cup \varDelta$ by modus ponens. More precisely,

$$\begin{aligned} \varLambda \oplus \varDelta = \{ \varphi \mid \psi \wedge \chi _1 \wedge \ldots \wedge \chi _n \vdash _{\textsf{IL}} \varphi \text { for some } \psi \in \varLambda \text { and } \chi _1, \ldots , \chi _n \in \varDelta \}. \end{aligned}$$

Note that if $\varDelta$ is closed under D-substitutions then so is $\varLambda \oplus \varDelta$, and if, moreover, $\varLambda \cup \varDelta$ is consistent, i.e. $\bot \notin \varLambda \oplus \varDelta$, then $\varLambda \oplus \varDelta$ is the smallest gsi-logic including $\varLambda \cup \varDelta$.

Let us recall that $\textsf{LC}$ is the Gödel-Dummett fuzzy logic [11, 16]. It is often presented as an extension of intuitionistic logic by the prelinearity schema:

$$\begin{aligned} (\varphi \rightarrow \psi ) \vee (\psi \rightarrow \varphi ). \end{aligned}$$

Let us denote the set of all instances of this schema as PreLin and let FullSplit denote the set of instances of the schema (where $\chi$ is not restricted)

$$\begin{aligned} (\chi \rightarrow (\varphi \vee \psi )) \rightarrow ((\chi \rightarrow \varphi ) \vee (\chi \rightarrow \psi )). \end{aligned}$$

An obvious connection of $\textsf{LC}$ to the logics we are focused on in this paper is given by the following observation made in [11].

Proposition 4

$\textsf{LC}=\textsf{IL} \oplus PreLin = \textsf{IL} \oplus FullSplit$.

So, $\textsf{LC}$ is a standard extension of $\textsf{InqIL}$ ($=\textsf{IL} \oplus Split$). It is well-known that the logic $\textsf{LC}$ is hereditarily structurally complete in the class of standard gsi-logics (shown in [12]). This result can also be obtained as a direct consequence of our Corollary 2, if we recall that SG-completeness generalizes the usual structural completeness. A natural question arises whether $\textsf{LC}$ is also hereditarily SF-complete over the space of gsi-logics in general.

When one considers results over the case of standard gsi-logics, there is reason to be cautious before importing them to our general setting. That a logic is hereditarily structurally complete over the standard gsi-logics does not a priori entail hereditary SF-completeness over the broader space of gsi-logics. To see that $\textsf{LC}$ is indeed hereditarily SF-complete, we need to use the following observation that is due to Dummett [11].

Lemma 3

$\varphi \vee \psi \equiv _{\textsf{LC}} ((\varphi \rightarrow \psi ) \rightarrow \psi ) \wedge ((\psi \rightarrow \varphi ) \rightarrow \varphi )$.

This result shows that disjunction is definable in $\textsf{LC}$. In fact, as pointed out in [23], every (standard) gsi-logic in which disjunction is definable includes $\textsf{LC}$. The previous lemma implies the following one.

Lemma 4

Every gsi-logic that includes $\textsf{LC}$ is standard.

Proof

Take any gsi-logic $\varLambda$ that includes $\textsf{LC}$, any $\varphi \in \varLambda$ and any substitution s. It follows from Lemma 3 that for every formula $\psi$ there is a $\vee$-free formula $\alpha _{\psi }$ such that $\psi \equiv _{\varLambda } \alpha _{\psi }$. We define a D-substitution $s^*$ fixing $s^*(p)=\alpha _{s(p)}$, for every atom p. Note that $s^*$ is $\varLambda$-equivalent to s. Since $s^*(\varphi ) \in \varLambda$, we also have $s(\varphi ) \in \varLambda$. Hence, $\varLambda$ is standard.   $\square$

Using this Lemma we can prove the following result.

Theorem 3

$\textsf{LC}$ is hereditarily SF-complete over all gsi-logics.

We can even strengthen this result in the following way.

Theorem 4

Let $\varLambda$ be a gsi-logic including $\textsf{InqIL}$. Then the following claims are equivalent: (a) $\varLambda$ is hereditarily SF-complete; (b) $\varLambda$ is SF-complete; (c) $\varLambda$ is standard; (d) $\varLambda$ includes all instances of FullSplit; (e) if $\vdash _{\varLambda }\varphi \rightarrow (\psi \vee \chi )$ then $\vdash _{\varLambda }(\varphi \rightarrow \psi )\vee (\varphi \rightarrow \chi )$; (f) $\textsf{LC} \subseteq \varLambda$.

Proof

$(a)\Rightarrow (b)$ is immediate by definition. $(b)\Rightarrow (c)$ is from Proposition 1. $(c)\Rightarrow (d)$: As a standard extension of $\textsf{InqIL}$, $\varLambda$ must contain all instances of FullSplit. $(d)\Rightarrow (e)$ is immediate. $(e)\Rightarrow (f)$: As an extension of $\textsf{IL}$, $\varLambda$ includes all instances of $(\varphi \vee \psi )\rightarrow (\varphi \vee \psi )$. By the assumption (e), we obtain $((\varphi \vee \psi )\rightarrow \varphi )\vee ((\varphi \vee \psi )\rightarrow \psi ) \in \varLambda$. Since $\psi \rightarrow (\varphi \vee \psi ), \varphi \rightarrow (\varphi \vee \psi )$ are theorems, we obtain $(\varphi \rightarrow \psi )\vee (\psi \rightarrow \varphi ) \in \varLambda$. By Proposition 4, $\textsf{LC} \subseteq \varLambda$. $(f)\Rightarrow (a)$: By Theorem 3, $\textsf{LC}$ is hereditarily SF-complete, whence in virtue of the inclusion of $\textsf{LC}$ in $\varLambda$, $\varLambda$ is hereditarily SF-complete.   $\square$

It is clear that the logic $\textsf{LC}$ is what we obtain if we close $\textsf{InqIL}$ under all substitutions. Let us consider this operation of schematic closure from a more general perspective. We have already indicated that any gsi-logic $\varLambda$ determines its schematic fragment $S(\varLambda )=\{ \varphi \mid s(\varphi ) \in \varLambda , \text{ for } \text{ every } \text{ substitution } s \}$, which is a standard gsi-logic. All inquisitive gsi-logics have the same schematic fragment, namely $\textsf{ML}$. The operation of schematic closure that we denote as C can be generally defined as follows: $\varphi \in C(\varLambda )$ iff $s_1(\psi _1) \wedge \ldots \wedge s_n (\psi _n) \vdash _{\textsf{IL}} \varphi$, for some substitutions $s_1, \ldots , s_n$ and some $\psi _1, \ldots , \psi _n \in \varLambda$. Note that $C(\varLambda )$ is indeed a standard gsi-logic. In general, it holds that $S(\varLambda ) \subseteq \varLambda \subseteq C(\varLambda )$. $S(\varLambda )$ is the greatest standard gsi-logic below $\varLambda$, and $C(\varLambda )$ is the smallest standard gsi-logic above $\varLambda$. So, if $\varLambda$ is itself standard, we obtain $S(\varLambda ) = \varLambda = C(\varLambda )$. In the rest of this section we explore the schematic closures of inquisitive gsi-logics.

It is clear that $C(\textsf{InqIL})=\textsf{LC}$ and $C(\textsf{InqB})=\textsf{CL}$. What do the schematic closures of the other inquisitive gsi-logics look like? The standard gsi-logics that include $\textsf{LC}$ form a chain consisting of the multivalued logics $\textsf{G}_n$, $n \ge 3$, plus the classical logic $\textsf{CL}$ on the top. If we denote classical logic as $\textsf{G}_2$ and the logic $\textsf{LC}$ as $\textsf{G}_{\omega }$ then we have (see [16]):

$$\begin{aligned} \textsf{G}_{\omega } \subseteq \ldots \subseteq \textsf{G}_5 \subseteq \textsf{G}_4 \subseteq \textsf{G}_3 \subseteq \textsf{G}_2. \end{aligned}$$

The schematic closure of every gsi-logic extending $\textsf{InqIL}$ will be one of the $\textsf{G}$-logics. For those gsi-logics which include $\textsf{InqIL}$ and have the disjunction property, i.e. for the inquisitive gsi-logics, we can characterize the schematic closures in an elegant and systematic way.

For any set of formulas $\varDelta$, let $\varDelta ^{df}$ denote the $\vee$-free fragment of $\varDelta$, i.e. $\varDelta ^{df}=\{\varphi \in \varDelta \mid \varphi \text { is } \vee \!\text {-free} \}$. The disjunction property of inquisitive logics is crucial for the proof of the following lemma.

Lemma 5

Let $\varLambda$ be any inquisitive gsi-logic and $\textsf{G}_n$, where $n \in \{2, 3, 4, \ldots , \omega \}$, any gsi-logic including $\textsf{LC}$. Then (a) $\varLambda = \textsf{InqIL} \oplus \varLambda ^{df}$; (b) $\textsf{G}_n = \textsf{LC} \oplus \textsf{G}_n^{df}$.

Proof

(a) Let $\varLambda$ be any inquisitive gsi-logic. Clearly, it holds that $\textsf{InqIL} \oplus \varLambda ^{df} \subseteq \varLambda$. Assume $\varphi \in \varLambda$. Let $\varphi \equiv _{\textsf{InqIL}} \alpha _1 \vee \ldots \vee \alpha _n$, where each $\alpha _i$ is $\vee$-free. By the disjunction property, for some i, $\alpha _i \in \varLambda$ and thus $\alpha _i \in \varLambda ^{df}$. Hence, $\varphi \in \textsf{InqIL} \oplus \varLambda ^{df}$. (b) Clearly, $\textsf{LC} \oplus \textsf{G}_n^{df} \subseteq \mathsf {G_n}$. Assume $\varphi \in \textsf{G}_n$. Then, by Lemma 3, there is $\vee$-free $\alpha$ such that $\varphi \equiv _{\textsf{LC}} \alpha$. Then $\alpha \in \textsf{G}_n^{df}$ and thus $\varphi \in \textsf{LC} \oplus \textsf{G}_n^{df}$.

With the help of this lemma we can characterize the schematic closures of inquisitive gsi-logics in the following way.

Theorem 5

Let $\varLambda$ be an inquisitive gsi-logic. Then

$$\begin{aligned} C(\varLambda )=\textsf{LC} \oplus \varLambda ^{df} = \textsf{G}_{n}, \text { for } n=\max \lbrace m\mid \varLambda ^{df}\subseteq \textsf{G}^{df}_{m}\rbrace . \end{aligned}$$

Proof

Assume that $\varLambda$ is an inquisitive gsi-logic. Clearly, it holds that $\textsf{LC} \oplus \varLambda ^{df} \subseteq C(\varLambda )$. By Lemma 5-a, $\varLambda = \textsf{InqIL} \oplus \varLambda ^{df}$ and thus $\varLambda \subseteq \textsf{LC} \oplus \varLambda ^{df}$. By Lemma 4, $\textsf{LC} \oplus \varLambda ^{df}$ is standard and since $C(\varLambda )$ is the smallest standard gsi-logic extending $\varLambda$, we obtain $C(\varLambda ) \subseteq \textsf{LC} \oplus \varLambda ^{df}$. So, we have proved that $C(\varLambda ) = \textsf{LC} \oplus \varLambda ^{df}$.

Clearly, $C(\varLambda )=\textsf{G}_{n}$, for some n. Then it must hold $\varLambda ^{df}\subseteq \textsf{G}^{df}_{n}$. Assume, for the sake of contradiction, that $n \ne \omega$ and $\varLambda ^{df}\subseteq \textsf{G}^{df}_{n+1}$. Then, using Lemma 5-b, we obtain $C(\varLambda )=\textsf{LC} \oplus \varLambda ^{df}\subseteq \textsf{LC} \oplus \textsf{G}^{df}_{n+1}=\textsf{G}_{n+1}$. But $C(\varLambda ) \subseteq \textsf{G}_{n+1}$ is in contradiction with the assumption $C(\varLambda )=\textsf{G}_{n}$. Thus $n=\max \lbrace m\mid \varLambda ^{df}\subseteq \textsf{G}^{df}_{m}\rbrace$.

   $\square$

So, while $\varLambda = \textsf{InqIL} \oplus \varLambda ^{df}$, $C(\varLambda )=\textsf{LC} \oplus \varLambda ^{df}$. This result shows that the schematic closure operation collapses the uncountable space of inquisitive gsi-logics to a countable linear order of standard gsi-logics. Moreover, this mapping to $\textsf{G}_{n}$-logics is surjective. In particular, each $\textsf{InqIL} \oplus \textsf{G}^{df}_{n}$ is inquisitive and $C(\textsf{InqIL} \oplus \textsf{G}^{df}_{n})=\textsf{G}_{n}$.

5 Kripke Models

Structural completeness is an important property of classical logic that intuitionistic logic lacks. On the other hand, the disjunction property is an important property of intuitionistic logic that classical logic violates. An interesting question is whether there are logics that have both these properties.

Definition 5

A gsi-logic is optimal if it is SG-complete and has the disjunction property.

The only standard gsi-logic that is known to be optimal is $\textsf{ML}$ (see [37]). As another direct consequence of Theorem 2 we obtain the following result showing that among non-standard gsi-logics there are uncountably many optimal logics.

Theorem 6

Every inquisitive gsi-logic is optimal.

Let us point out that at the end of [22] a conjecture is formulated which, when translated in our terminology, says that (a) $\textsf{InqIL}$ is optimal, and (b) $\textsf{InqIL}$ and $\textsf{InqB}$ are the only optimal gsi-logics. Theorem 6 thus serves to prove the first half of the conjecture and refutes the latter half.

In this section, we show that Theorem 6 is related to the possibility of an interesting canonical model construction for inquisitive gsi-logics. For any gsi-logic one can construct, in the usual way, a canonical Kripke model built out of prime theories. A peculiar feature of inquisitive gsi-logics is that they can also be characterized by a Kripke model built directly out of consistent $\vee$-free formulas.⁴ We will briefly formulate this construction and compare it with another unusual canonical model construction that we obtain as an application of our main results. For the rest of this section, let us fix an inquisitive gsi-logic $\varLambda$. Moreover, let us say that $\alpha$ is consistent if $\nvdash _{\varLambda } \lnot \alpha$.

Now we introduce the Kripke semantics for intuitionistic logic. A Kripke frame is a pair $\langle S, \le \rangle$ where $\le$ is a preorder, i.e. a reflexive and transitive relation on S. A Kripke model is a Kripke frame equipped with a valuation V, i.e. a function that assigns to each atomic formula an upward closed subset of S (that is, if $w \in V(p)$ and $w \le v$ then $v \in V(p)$). Given any Kripke model the relation $\Vdash$ between states of the model and formulas is defined in the usual recursive way. For the atomic formulas, we set $w \Vdash p$ iff $w \in V(p)$. For the constant $\bot$ and complex formulas, the relation is determined as follows:

• (a) $w \nVdash \bot$,

• (b) $w \Vdash \varphi \rightarrow \psi$ iff for any $v \ge w$, if $v \Vdash \varphi$ then $v \Vdash \psi$,

• (c) $w \Vdash \varphi \wedge \psi$ iff $w \Vdash \varphi$ and $w \Vdash \psi$,

• (d) $w \Vdash \varphi \vee \psi$ iff $w \Vdash \varphi$ or $w \Vdash \psi$.

The relation is persistent: if $w \Vdash \varphi$ and $w \le v$ then $v \Vdash \varphi$. We say that $\varphi$ is valid in a model $\langle S, \le , V \rangle$ if $w \Vdash \varphi$ holds in that model for every $w \in S$. It is well-known that a formula is intuitionistically valid iff it is valid in all Kripke models [21]. The recursive clauses for $\Vdash$ actually mirror some characteristic properties of $\vdash$ in inquisitive gsi-logics, as is shown in the following proposition.

Proposition 5

Let $\alpha$ be a consistent $\vee$-free formula and $\varphi , \psi$ arbitrary formulas. Then

• (a) $\alpha \nvdash _{\varLambda } \bot$,

• (b) $\alpha \vdash _{\varLambda } \varphi \rightarrow \psi$ iff for any consistent $\vee$-free $\beta$ s.t. $\beta \vdash _{\varLambda } \alpha$ if $\beta \vdash _{\varLambda } \varphi$ then $\beta \vdash _{\varLambda } \psi$,⁵

• (c) $\alpha \vdash _{\varLambda } \varphi \wedge \psi$ iff $\alpha \vdash _{\varLambda } \varphi$ and $\alpha \vdash _{\varLambda } \psi$,

• (d) $\alpha \vdash _{\varLambda } \varphi \vee \psi$ iff $\alpha \vdash _{\varLambda } \varphi$ or $\alpha \vdash _{\varLambda } \psi$.

Proof

(a) and (c) are immediate. Due to Lemma 2, (d) holds for every gsi-logic which has the disjunction property. Let us prove (b). The left-to-right direction is immediate. For the right-to-left direction assume that for any consistent $\vee$-free $\beta \vdash _{\varLambda } \alpha$, if $\beta \vdash _{\varLambda } \varphi$ then $\beta \vdash _{\varLambda } \psi$. Obviously, $\beta \vdash _{\varLambda } \psi$ holds also in the case that $\beta$ is not consistent. Assume that $\varphi \equiv _{\varLambda } \gamma _1 \vee \ldots \vee \gamma _n$, where $\gamma _1, \ldots , \gamma _n$ are $\vee$-free. Then $\gamma _i \wedge \alpha \vdash _{\varLambda } \alpha$ and $\gamma _i \wedge \alpha \vdash _{\varLambda } \varphi$. Our assumption implies that $\gamma _i \wedge \alpha \vdash _{\varLambda } \psi$. So, for all i, $\gamma _i \vdash _{\varLambda } \alpha \rightarrow \psi$, and thus $\varphi \vdash _{\varLambda } \alpha \rightarrow \psi$. It follows that $\alpha \vdash _{\varLambda } \varphi \rightarrow \psi$.   $\square$

This observation motivates the construction of a canonical Kripke model $\mathcal {M}_{\varLambda }=\langle S_{\varLambda }, \le _{\varLambda }, V_{\varLambda } \rangle$, where $S_{\varLambda }=\{ \alpha \mid \alpha \text { is } \vee \!\text {-free and consistent} \}$, $\alpha \le _{\varLambda } \beta$ iff $\beta \vdash _{\varLambda } \alpha$, and $\alpha \in V_{\varLambda }(p)$ iff $\alpha \vdash _{\varLambda } p$. Then Proposition 5 directly implies that $\Vdash$ in $\mathcal {M}_{\varLambda }$ coincides with $\vdash _{\varLambda }$.

Theorem 7

For each $\varphi$ and each consistent $\vee$-free $\alpha$, $\alpha \Vdash \varphi$ in $\mathcal {M}_{\varLambda }$ if and only if $\alpha \vdash _{\varLambda } \varphi$. As a consequence, $\varphi \in \varLambda$ if and only if $\varphi$ is valid in $\mathcal {M}_{\varLambda }$.

There is also a remarkable correspondence between the semantic clauses of Kripke semantics and the behaviour of D-substitutions in inquisitive gsi-logics. This correspondence is based on Theorem 6. To make it more visible, let us write $s \succ \varphi$ instead of $\vdash _{\varLambda } s(\varphi )$ and let us define for any D-substitutions s, t that $s \le t$ iff there is a D-substitution u such that $t = u \circ s$ (where $\circ$ is the composition of substitutions).

Proposition 6

Let s be a D-substitution and $\varphi , \psi$ arbitrary formulas. Then

• (a) $s \nsucc \bot$,

• (b) $s \succ \varphi \rightarrow \psi$ iff for any D-substitution $t \ge s$, if $t \succ \varphi$ then $t \succ \psi$,

• (c) $s \succ \varphi \wedge \psi$ iff $s \succ \varphi$ and $s \succ \psi$,

• (d) $s \succ \varphi \vee \psi$ iff $s \succ \varphi$ or $s \succ \psi$.

Proof

All cases are straightforward. We will just comment on the case (b). This case can be reformulated in this way: $s(\varphi ) \vdash s(\psi )$ iff for any D-substitution t, if $\vdash t(s(\varphi ))$ then $\vdash t(s(\psi ))$. But this is exactly SD-completeness applied to the implication $s(\varphi ) \rightarrow s(\psi )$.   $\square$

Using this observation we can build from D-substitutions a particular canonical Kripke model $\mathcal {M}^{\varLambda }=\langle S^{\varLambda }, \le ^{\varLambda }, V^{\varLambda } \rangle$, where $S^{\varLambda }$ is the set of all D-substitutions, $s \le ^{\varLambda } t$ iff there is a D-substitution u such that $t = u \circ s$, $s \in V^{\varLambda }(p)$ iff $s \succ p$.⁶

Let id be the identity function on atomic formulas. Then id is a D-substitution and $id \le ^{\varLambda } s$, for every D-substitution s. So, $\varphi$ is valid in $\mathcal {M}^{\varLambda }$ iff $id \Vdash \varphi$ in $\mathcal {M}^{\varLambda }$. Proposition 6 implies the following result.

Theorem 8

For each $\varphi$ and each D-substitution s, $s \Vdash \varphi$ in $\mathcal {M}^{\varLambda }$ if and only if $s \succ \varphi$. As a consequence, $\varphi \in \varLambda$ if and only if $\varphi$ is valid in $\mathcal {M}^{\varLambda }$.

6 Conclusion

Let us summarize the main results of this paper. We have studied four notions of structural completeness (SF-, SG-, SH- and SD-completeness) in a class of generalized superintuitionistic logics that are not required to be closed under all substitutions but only under substitutions assigning disjunction free formulas. We have shown a connection between these notions and the schema Split that axiomatizes intuitionistic inquisitive logic $\textsf{InqIL}$. A characteristic feature of Split is that it allows one to transform every formula to a disjunctive normal form (Theorem 1).

Our main result (Theorem 2) shows that SH-completeness is equivalent to SD-completeness and these properties hold exactly for those logics that validate Split. As a consequence, SH(D)-completeness is hereditary (Corollary 1). We have also shown that $\textsf{InqIL}$ is hereditarily SG-complete (Corollary 2) and its closure under substitutions, i.e. the Gödel-Dummett logic $\textsf{LC}$, remains hereditarily SF-complete (Theorem 3 and its extension Theorem 4).

We have further studied inquisitive logics, i.e. those logics that include $\textsf{InqIL}$ and have the disjunction property. We have proved that the operation that closes every such logic under substitutions maps the uncountably large class of inquisitive logics onto the countably infinite chain of those logics that include $\textsf{LC}$ (Theorem 5). It follows directly from our main result that inquisitive logics are optimal, i.e. they are structurally complete and have disjunction property (Theorem 6). They can be characterized by a canonical Kripke model built from consistent disjunction free formulas (Theorem 7). Interestingly, their optimality means that they can be alternatively characterized by a canonical Kripke model built from substitutions assigning disjunction free formulas (Theorem 8).

In future work, we would like to study structural completeness in the more general context of substructural inquisitive logics [30]. We also plan to explore the notion of structural completeness for these logics in the setting of multi-conclusion consequence relation [19].