2. Intuitionistic Inquisitive Logic and Its Extensions

The standard inquisitive logic (Ciardelli, Reference Ciardelli2009, Reference Ciardelli2016; Ciardelli and Roelofsen, Reference Ciardelli and Roelofsen2011; Ciardelli et al., Reference Ciardelli, Groenendijk and Roelofsen2019) uses 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 nonclassical inquisitive logics. A general semantic and syntactic theory of these logics is developed in Punčochář (Reference Punčochář2019). An important example of such a logic is intuitionistic inquisitive logic (Ciardelli et al., Reference Ciardelli, Iemhoff and Yang2020; Punčochář, Reference Punčochář2016, Reference Punčochář2021). 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 an extra operator, as in Punčochář (Reference Punčochář2017) and Ciardelli et al. (Reference Ciardelli, Iemhoff and Yang2020). Alternatively, one can work just with the standard language involving only one disjunction, which is however interpreted in the inquisitive way, as in Ciardelli (Reference Ciardelli2009), Ciardelli and Roelofsen (Reference Ciardelli and Roelofsen2011), and Punčochář (Reference Punčochář2021). 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.

However, 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. A precise formulation of this fact would require a lot of extra space because we would need to fully describe the system with the two disjunctions. Nevertheless, we can provide some explanation without going into the details by pointing out that intuitionistic logic is not structurally complete, and if we add intuitionistic declarative disjunction to the language, structural completeness fails for the same reasons for which it fails in the standard language of intuitionistic logic. For example, the Harrop rule with declarative disjunction, which is often used as a counterexample to structural completeness in intuitionistic logic, would be admissible but not derivable in the system.

Note that this is not in conflict with the results in Iemhoff and Yang (Reference Iemhoff and Yang2016), which show structural completeness for dependence logic considering languages that involve inquisitive as well as declarative disjunction (called tensor in this context). Dependence logic is based on classical logic, which is structurally complete, and so the presence of the second disjunction does not cause any problems. Our main results point to an interesting discrepancy between intuitionistic and inquisitve disjunction. While inquisitive disjunction preserves the constructive features of intuitionistic disjunction, its addition does not, unlike the addition of intuitionistic disjunction, lead to a violation of structural completeness.

In this paper, we will work with this basic language:

\begin{equation*} \varphi ::= p \mid \bot \mid \varphi \rightarrow \varphi \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \end{equation*}

where $\vee$ will be viewed as an inquisitive disjunction. Negation, equivalence, and a constant for validity are defined in the following usual way:

\begin{equation*} \neg \varphi ={}_{\!def}\; \varphi \rightarrow \bot, \varphi \leftrightarrow \psi ={}_{\!def}\; (\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \varphi ), \top ={}_{\!def}\; \bot \rightarrow \bot.\end{equation*}

Fix any Hilbert-style axiomatization of intuitionistic logic in this language, which has modus ponens as the only rule of inference. Let $\mathsf{IL}$ denote the set of its derivable formulas. We write $\vdash _{\mathsf{IL}} \varphi$ instead of $\varphi \in \mathsf{IL}$ , $\varphi \vdash _{\mathsf{IL}} \psi$ instead of $\varphi \rightarrow \psi \in \mathsf{IL}$ , and $\varphi \equiv _{\mathsf{IL}} \psi$ instead of $\varphi \leftrightarrow \psi \in \mathsf{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{equation*} (\alpha \rightarrow (\psi \vee \chi )) \rightarrow ((\alpha \rightarrow \psi ) \vee (\alpha \rightarrow \chi )), \end{equation*}

where $\alpha$ ranges over $\vee$ -free formulas.Footnote ¹ The set of derivable formulas will be denoted as $\mathsf{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{equation*} \varphi \equiv _{\mathsf{InqIL}} \alpha _1 \vee \ldots \vee \alpha _n. \end{equation*}

Proof. One can proceed by induction. We show just the inductive step for implication. Assume that $\psi \equiv _{\mathsf{InqIL}} \beta _1 \vee \ldots \vee \beta _m$ and $\chi \equiv _{\mathsf{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{equation*} \begin{array}{lll} \psi \rightarrow \chi & \equiv _{\mathsf{InqIL}} & \bigvee _{i \in I} \beta _i \rightarrow \bigvee _{j \in J} \gamma _j \\[3pt] & \equiv _{\mathsf{InqIL}} & \bigwedge _{i \in I} (\beta _i \rightarrow \bigvee _{j \in J} \gamma _j) \\[3pt] & \equiv _{\mathsf{InqIL}} & \bigwedge _{i \in I} \bigvee _{j \in J} (\beta _i \rightarrow \gamma _j) \\[3pt] & \equiv _{\mathsf{InqIL}} & \bigvee _{f{:}\, I \rightarrow J} \bigwedge _{i \in I} (\beta _i \rightarrow \gamma _{f(i)}). \end{array} \end{equation*}

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 _{\mathsf{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 Theorem1, there are $\vee$ -free formulas $\beta _1, \ldots, \beta _n$ such that $\psi \equiv _{\mathsf{InqIL}} \beta _1 \vee \ldots \vee \beta _m$ , and so $\psi \rightarrow \chi \equiv _{\mathsf{InqIL}} \bigvee _i \beta _i \rightarrow \chi \equiv _{\mathsf{InqIL}} \bigwedge _i (\beta _i \rightarrow \chi )$ . As a consequence of this observation, $\mathsf{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 $\mathsf{InqIL}$ . For example:

\begin{equation*}((p \vee q) \rightarrow (p \vee q)) \rightarrow (((p \vee q) \rightarrow p) \vee ((p \vee q) \rightarrow q)) \notin \mathsf{InqIL}.\end{equation*}

In this respect, $\mathsf{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 $\mathsf{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 $\mathsf{InqIL}$ (and other inquisitive logics). For this purpose, we use the following definitions.

Note that the notion of a standard gsi-logic coincides with the standard notion of a superintuitionistic (also called intermediate) logic. It is clear that $\mathsf{InqIL}$ is a gsi-logic, though not standard. Another example of a nonstandard gsi-logic is the classical inquisitive logic, often called basic inquisitive logic and denoted as $\mathsf{InqB}$ (see Ciardelli (Reference Ciardelli2016)), which can be obtained by adding to $\mathsf{InqIL}$ the restricted double negation law DN: $\neg \neg \alpha \rightarrow \alpha$ , where $\alpha$ ranges over $\vee$ -free (or, equivalently, Harrop) formulas. Note that the $\vee$ -free fragment of $\mathsf{InqB}$ is identical with classical logic, while it can be shown that the $\vee$ -free fragment of $\mathsf{InqIL}$ is identical with (the $\vee$ -free fragment of) intuitionistic logic.

Next we define, in accordance with Punčochář (Reference Punčochář2021), the general notion of an inquisitive gsi-logic.

The notion of an inquisitive gsi-logic coincides with the notion of a G-logic introduced in Punčochář (Reference Punčochář2016). It can be shown that both $\mathsf{InqIL}$ and $\mathsf{InqB}$ have the disjunction property and thus are indeed inquisitive in the sense of our general definition. In fact, $\mathsf{InqIL}$ is the weakest, and $\mathsf{InqB}$ is the strongest inquisitive gsi-logic. Every inquisitive gsi-logic is regular, but no inquisitive gsi-logic is an intermediate logic in the usual sense; that is, in our terminology, no inquisitive gsi-logic is standard. However, for any standard gsi-logic $\Lambda$ , there is exactly one inquisitive gsi-logic that conservatively extends the $\vee$ -free fragment of $\Lambda$ . As a consequence, there are uncountably many inquisitive gsi-logics. For a justification of these claims, see Punčochář (Reference Punčochář2016).

To the best of our knowledge, $\mathsf{InqIL}$ and $\mathsf{InqB}$ were both studied for the first time in Miglioli et al. (Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti1989), under the names $\mathsf{F_{int}}$ and $\mathsf{F_{cl}}$ , where it was proved, for instance, that the schematic fragment of $\mathsf{InqB}$ (called the standardization of $\mathsf{F_{cl}}$ in Miglioli et al., (Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti1989)), that is, the set $S(\mathsf{InqB})=\{\varphi \mid s(\varphi ) \in \mathsf{InqB}, \text{for every substitution}\, s \}$ , is identical with Medvedev’s logic of finite problems $\mathsf{ML}$ . Interestingly, the same was stated without proof also for $\mathsf{InqIL}$ . That this quite nontrivial claim is true follows from the main result of Grilletti (Reference Grilletti, Fernández-Duque, Palmigiano and Pinchinat2022).

The system of $\mathsf{InqB}$ was later rediscovered in Ciardelli (Reference Ciardelli2009) and Ciardelli and Roelofsen (Reference Ciardelli and Roelofsen2011) and proved to be sound and complete with respect to the modern version of inquisitive semantics. This logic was applied to linguistic phenomena (see Ciardelli et al. (Reference Ciardelli, Groenendijk and Roelofsen2019) for an overview) but also studied from algebraic and topological perspectives (Roelofsen, Reference Roelofsen2013; Frittella et al., Reference Frittella, Greco, Palmigiano, Yang, Väänänen, Hirvonen and de Queiroz2016; Bezhanishvili et al., Reference Bezhanishvili, Grilletti, Holliday, Iemhoff, Moortgat and de Queiroz2019). There is also an extensive literature on various modal extensions of $\mathsf{InqB}$ (Ciardelli and Roelofsen, Reference Ciardelli and Roelofsen2015; van Gessel, Reference van Gessel2020, Reference van Gessel2022; Punčochář, Reference Punčochář2015; Punčochář and Sedlár, Reference Punčochář and Sedlár2021).

A generalization of inquisitive semantics that corresponds to $\mathsf{InqIL}$ was introduced in Punčochář (Reference Punčochář2016). Intuitionistic inquisitive logic was further studied in Ciardelli et al. (Reference Ciardelli, Iemhoff and Yang2020), Punčochář (Reference Punčochář2017), Sano (Reference Sano, Fernández-Duque, Palmigiano and Pinchinat2022), and Punčochář and Pezlar (Reference Punčochář, Pezlar, Ciabattoni, Gabelaia and Sedlár2024) and from an algebraic perspective in Punčochář (Reference Punčochář2021) and Quadrellaro (Reference Quadrellaro2022). A slightly different approach to intuitionistic inquisitive logic was proposed in Holliday (Reference Holliday, Fernández-Duque, Palmigiano and Pinchinat2022). This approach is based on a more general framework that does not validate Split.

A recent interesting result also shows that the system of $\mathsf{InqIL}$ provides a sound and complete axiomatization of proof-theoretic semantics (Stafford, Reference Stafford2021). 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 Miglioli et al. (Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti1989), and they were employed also in Iemhoff and Yang (Reference Iemhoff and Yang2016), where it was shown that $\mathsf{InqB}$ and some related propositional dependence logics are structurally complete with respect to a suitably adapted sense of the term. In Miglioli et al. (Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti1989), 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.

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 (i.e., intermediate logics in the usual sense), both these notions are equivalent and coincide with the usual definition. 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 stronger than $SG$ -completeness.

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.

Let $\Lambda$ be a gsi-logic that validates Split. Proposition6 says that if $s$ is an $H$ -substitution, then $s \in sub(\Lambda )$ . One can ask whether the converse also 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 $\Lambda$ must also be closed under $s$ . A more interesting question is whether $\Lambda$ may also be closed 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 $\Lambda$ -equivalent if $s(p) \equiv _{\Lambda } t(p)$ , for every atomic formula $p$ . Then the converse of Proposition6 would state that if $s \in sub(\Lambda )$ , then $s$ is $\Lambda$ -equivalent to an $H$ -substitution. Interestingly, this is a property that distinguishes $\mathsf{InqIL}$ from $\mathsf{InqB}$ .

Proof. For the first part, let $s$ be a substitution under which $\mathsf{InqB}$ is closed, and let $p$ be an arbitrary atomic formula. Then, as $\mathsf{InqB}$ proves $\neg \neg p\leftrightarrow p$ , we obtain $\neg \neg s(p)\equiv _{\mathsf{InqB}} s(p)$ . By Theorem1, $s(p) \equiv _{\mathsf{InqB}} \alpha _{1}\vee \ldots \vee \alpha _{n}$ , where each $\alpha _{i}$ is $\vee$ -free, whence $s(p) \equiv _{\mathsf{InqB}}\neg \neg (\alpha _{1}\vee \ldots \vee \alpha _{n})$ . But as $(\neg \varphi \wedge \neg \psi )\leftrightarrow \neg (\varphi \vee \psi )$ holds intuitionistically, $s(p) \equiv _{\mathsf{InqB}}\neg (\neg \alpha _{1}\wedge \ldots \wedge \neg \alpha _{n})$ , where $\neg (\neg \alpha _{1}\wedge \ldots \wedge \neg \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 \neg p$ . Assume, for the sake of contradiction, that $p \vee \neg p \equiv _{\mathsf{InqIL}} \alpha$ , for some Harrop formula $\alpha$ . Then, by Split and disjunction property, we would obtain $\vdash _{\mathsf{InqIL}} \alpha \rightarrow p$ or $\vdash _{\mathsf{InqIL}} \alpha \rightarrow \neg p$ , and thus $\vdash _{\mathsf{InqIL}} (p \vee \neg p) \rightarrow p$ or $\vdash _{\mathsf{InqIL}} (p \vee \neg p) \rightarrow \neg p$ . This leads to a contradiction because none of these formulas is valid in classical logic, which extends $\mathsf{InqIL}$ . So, $s$ is not $\mathsf{InqIL}$ -equivalent to any $H$ -substitution.

It remains to be shown that $s \in sub(\mathsf{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 _{\mathsf{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 \neg p, \top$ . To see this, note that $\bot$ and $\top$ are generated from $p \vee \neg p$ by negation and the set $\{\bot, p \vee \neg 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 \neg p, \top$ , the formula

\begin{equation*}(s(\alpha ) \rightarrow (s(\varphi ) \vee s(\psi ))) \rightarrow ((s(\alpha ) \rightarrow s(\varphi )) \vee (s(\alpha ) \rightarrow s(\varphi )))\end{equation*}

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

We are not sure how to interpret philosophically the previous rather surprising result. What does it mean in terms of the inquistive interpretation of the system that associates formulas equivalent to $\vee$ -free formulas with statements and other formulas with questions? We do not have a clear explanation. Technically speaking, Proposition7 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, Theorem2 below, that these substitutions play a special role in these logics.

We will rely heavily on a standard technique for proving structural completeness developed by Prucnal (Reference Prucnal1973), or more precisely, on its refinement introduced later by Minari and Wroński (Reference Minari and Wroński1988). Let $\alpha$ be a Harrop formula and $v$ a classical valuation (i.e., a function assigning to each formula $0$ or $1$ in accordance with the semantics of classical logic). Following Minari and Wroński (Reference Minari and Wroński1988), we define, relative to $\alpha$ and $v$ , the following $H$ -substitution:

\begin{equation*} s_{\alpha }^{v}(p) = \begin{cases} \alpha \rightarrow p & \text{if}\, v(p)=1 \\ \neg \neg \alpha \wedge (\alpha \rightarrow p) & \text{otherwise} \end{cases} \end{equation*}

Note that if $\alpha$ is a $\vee$ -free formula, then $s_{\alpha }^{v}$ is a $D$ -substitution. We need the following two features of this substitution.

Proof. The claim (a) follows from Lemma 1 in Minari and Wroński (Reference Minari and Wroński1988), which can be proved by induction and which states that for any formula $\varphi$ :

\begin{equation*} \alpha \vdash _{\mathsf{IL}} \varphi \leftrightarrow s_{\alpha }^{v} (\varphi ).\end{equation*}

The claim (b) follows from Lemma 3 in Minari and Wroński (Reference Minari and Wroński1988) that states that the property by which $s_{\alpha }^{v}$ was defined is preserved by every Harrop formula $\beta$ in this sense:

\begin{equation*} s_{\alpha }^{v}(\beta ) \equiv _{\mathsf{IL}} \begin{cases} \alpha \rightarrow \beta & \text{if} \,v(\beta )=1 \\ \neg \neg \alpha \wedge (\alpha \rightarrow \beta ) & \text{otherwise} \end{cases} \end{equation*}

This lemma implies the following one that generalizes the main result of Minari and Wroński (Reference Minari and Wroński1988), which was originally formulated only for the usual intermediate logics, that is, in our terminology, standard gsi-logics.

Lemma 9. Let $\Lambda$ be a gsi-logic and $\alpha$ a Harrop formula. If $\Lambda$ is regular or $\alpha$ is $\vee$ -free, then for all formulas $\psi, \chi$ :

\begin{equation*}\text{if}\, \alpha \rightarrow (\psi \vee \chi ) \in \Lambda \text{ then}\, (\alpha \rightarrow \psi ) \vee (\alpha \rightarrow \chi ) \in \Lambda .\end{equation*}

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.

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).

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 $\mathsf{ML}$ has this property (see Citkin (Reference Citkin1978); Dzik and Wroński (Reference Dzik and Wroński1973)). The next corollary is based on the observation that $SD$ -completeness is a stronger property than $SG$ -completeness.

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

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

$\mathsf{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$ .

We will conclude this section by another observation related to our main result, Theorem2. In its proof, we relied heavily on the result from Minari and Wroński (Reference Minari and Wroński1988) that states that for every standard gsi-logic $\Lambda$ , for every Harrop formula $\alpha$ , and for all formulas $\psi, \chi$ :

\begin{equation*} \text{if}\, \alpha \rightarrow (\psi \vee \chi )\in \Lambda\, \text{then}\, (\alpha \rightarrow \psi )\vee (\alpha \rightarrow \chi )\in \Lambda .\end{equation*}

In Lemma9, we had to formulate this claim more generally, which gave us two implications in the equivalences of Theorem2 (i.e., (a) $\Rightarrow$ (c) and (b) $\Rightarrow$ (c)). Minari and Wroński (Reference Minari and Wroński1988) concluded their paper by an open problem asking whether their result is best possible in the sense that the following two conditions are equivalent for every formula $\varphi$ :

1. (a) for every standard gsi-logic $\Lambda$ and for all formulas $\psi, \chi$ , it holds that if $\varphi \rightarrow (\psi \vee \chi )\in \Lambda$ , then $(\varphi \rightarrow \psi )\vee (\varphi \rightarrow \chi )\in \Lambda$ .

2. (b) $\varphi \equiv _{\mathsf{IL}} \alpha$ , for some Harrop formula $\alpha$ .

Minari and Wroński’s result is the implication from (b) to (a), and the question they posed is the implication from (a) to (b). This question is resolved negatively by Wojtylak (Reference Wojtylak2004), who formulated a class of sentences satisfying (a) but not generally (b).

It is clear that not every Wojtylak sentence is intuitionistically equivalent to a Harrop formula, the most simple example being $p \leftrightarrow (q \vee r)$ . Nevertheless, Wojtylak (Reference Wojtylak2004) proved the following theorem.

This provides a remarkable feature distinguishing the usual intermediate logics, that is, standard gsi-logics, from inquisitive gsi-logics. One can show that no inquisitive gsi-logic has the property expressed in Theorem3. Indeed, for every inquisitive gsi-logic $\Lambda$ , we have (due to Split and the laws of intuitionistic logic):

\begin{equation*}(p \leftrightarrow (q \vee r)) \rightarrow ((p \rightarrow q) \vee (p \rightarrow r)) \in \Lambda .\end{equation*}

However,

\begin{equation*}((p \leftrightarrow (q \vee r)) \rightarrow (p \rightarrow q)) \vee ((p \leftrightarrow (q \vee r)) \rightarrow (p \rightarrow r)) \notin \Lambda . \end{equation*}

To see this, assume for contradiction that the disjunction is in $\Lambda$ . Then, by the disjunction property of $\Lambda$ , at least one of its disjuncts would be in $\Lambda$ . But none of the disjuncts is valid in classical logic and thus cannot be valid in $\Lambda$ .

Interestingly, we can resolve Minari and Wroński’s open question positively if we do not restrict ourselves to the standard gsi-logics and instead expand the claim to all regular gsi-logics.

We can formulate an analogous result related to the class of all gsi-logics.

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 $\Lambda$ is a gsi-logic and $\Delta$ a set of formulas, then $\Lambda \oplus \Delta$ will denote the set of formulas derivable from $\Lambda \cup \Delta$ by modus ponens. More precisely,

\begin{equation*} \Lambda \oplus \Delta = \{ \varphi \mid \psi \wedge \chi _1 \wedge \ldots \wedge \chi _n \vdash _{\mathsf{IL}} \varphi \text{ for some $\psi \in \Lambda $ and $\chi _1, \ldots, \chi _n \in \Delta $} \}. \end{equation*}

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

Let us recall that $\mathsf{LC}$ is the Gödel–Dummett fuzzy logic (Gödel, Reference Gödel1932; Dummett, Reference Dummett1959). It is often presented as an extension of intuitionistic logic by the prelinearity schema:

\begin{equation*} (\varphi \rightarrow \psi ) \vee (\psi \rightarrow \varphi ). \end{equation*}

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 $\varphi$ is not restricted)

\begin{equation*} (\varphi \rightarrow (\psi \vee \chi )) \rightarrow ((\varphi \rightarrow \psi ) \vee (\varphi \rightarrow \chi )). \end{equation*}

An obvious connection of $\mathsf{LC}$ to the logics we are focused on in this paper is given by the following observation made in Dummett (Reference Dummett1959).

So, $\mathsf{LC}$ is a standard extension of $\mathsf{InqIL}$ ( $=\mathsf{IL} \oplus Split$ ). It is well-known that the logic $\mathsf{LC}$ is hereditarily structurally complete in the class of standard gsi-logics (shown in Dzik and Wroński (Reference Dzik and Wroński1973)). This result can also be obtained as a direct consequence of our Corollary11, if we recall that $SG$ -completeness generalizes the usual structural completeness. A natural question arises whether $\mathsf{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 $\mathsf{LC}$ is indeed hereditarily $SF$ -complete, we need to use the following observation that is due to Dummett (Reference Dummett1959).

This result shows that disjunction is definable in $\mathsf{LC}$ . In fact, as pointed out in Minari and Wroński (Reference Minari and Wroński1988), every (standard) gsi-logic in which disjunction is definable includes $\mathsf{LC}$ . The previous lemma implies the following one.

Using this lemma, we can prove the following result.

We can even strengthen this result in the following way.

It is clear that the logic $\mathsf{LC}$ is what we obtain if we close $\mathsf{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 $\Lambda$ determines its schematic fragment:

\begin{equation*}S(\Lambda )=\{ \varphi \mid s(\varphi ) \in \Lambda, \text{for every substitution}\, s \},\end{equation*}

which is a standard gsi-logic. It is a rather surprising fact that all inquisitive gsi-logics have the same schematic fragment, namely, $\mathsf{ML}$ . This follows from a combination of results in Ciardelli and Roelofsen (Reference Ciardelli and Roelofsen2011), showing that $\mathsf{ML}$ is the schematic fragment of the strongest inquisitive gsi-logic $\mathsf{InqB}$ and the main result of Grilletti (Reference Grilletti, Fernández-Duque, Palmigiano and Pinchinat2022), which implies that $\mathsf{ML}$ is also the schematic fragment of the weakest inquisitive gsi-logic $\mathsf{InqIL}$ .

The operation of schematic closure that we denote as $C$ can be generally defined as follows: $\varphi \in C(\Lambda )$ iff $s_1(\psi _1) \wedge \ldots \wedge s_n (\psi _n) \vdash _{\mathsf{IL}} \varphi$ , for some substitutions $s_1, \ldots, s_n$ and some $\psi _1, \ldots, \psi _n \in \Lambda$ .

Note that $C(\Lambda )$ is indeed a standard gsi-logic. In general, it holds that $S(\Lambda ) \subseteq \Lambda \subseteq C(\Lambda )$ . In fact, $S(\Lambda )$ is the greatest standard gsi-logic below $\Lambda$ , and $C(\Lambda )$ is the smallest standard gsi-logic above $\Lambda$ . So, if $\Lambda$ is itself standard, we obtain $S(\Lambda ) = \Lambda = C(\Lambda )$ . In the rest of this section, we explore the schematic closures of inquisitive gsi-logics.

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

\begin{equation*} \mathsf{G}_{\omega } \subseteq \ldots \subseteq \mathsf{G}_5 \subseteq \mathsf{G}_4 \subseteq \mathsf{G}_3 \subseteq \mathsf{G}_2. \end{equation*}

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

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

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

Theorem 8. Let $\Lambda$ be an inquisitive gsi-logic. Then

\begin{equation*} C(\Lambda )=\mathsf{LC} \oplus \Lambda ^{df} = \mathsf{G}_{n}, \text{ for } n=\max \lbrace m\mid \Lambda ^{df}\subseteq \mathsf{G}^{df}_{m}\rbrace . \end{equation*}

So, while $\Lambda = \mathsf{InqIL} \oplus \Lambda ^{df}$ , $C(\Lambda )=\mathsf{LC} \oplus \Lambda ^{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 of order type $1+\omega ^{\ast }$ . Moreover, this mapping to $\mathsf{G}_{n}$ -logics is surjective as the following proposition shows.

5. Characteristic Kripke Models Built from Substitutions

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.

The only standard gsi-logic that is known to be optimal is $\mathsf{ML}$ (see Wojtylak (Reference Wojtylak2004)). As another direct consequence of Theorem2, we obtain the following result showing that among nonstandard gsi-logics, there are uncountably many optimal logics.

We can also consider alternative notions of optimality involving the other kinds of structural completeness. For instance, we can say that a gsi-logic is $H$ -optimal if it is $SH$ -complete and has the disjunction property. It follows from our previous observations that every $H$ -optimal gsi-logic is optimal. However, the inverse implication does not hold. The logic $\mathsf{ML}$ is not $H$ -optimal because it does not validate Split and thus is not $SH$ -complete. Theorem2 immediately implies that inquisitive gsi-logics are exactly those gsi-logics that are $H$ -optimal.

Let us point out that at the end of Miglioli et al. (Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti1989) a conjecture is formulated, which, when translated in our terminology, says that (a) $\mathsf{InqIL}$ is $H$ -optimal, and (b) $\mathsf{InqIL}$ and $\mathsf{InqB}$ are the only $H$ -optimal gsi-logics.Footnote ⁴ Our results verify the first half of the conjecture but falsify the latter half.

In this section, we show that Theorem9 is related to the possibility of an interesting construction of characteristic models 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.Footnote ⁵ We will briefly formulate this construction and compare it with another unusual characteristic 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 $\Lambda$ . Moreover, let us say that $\alpha$ is consistent if $\nvdash _{\Lambda } \neg \alpha$ .

Now we introduce the Kripke semantics for intuitionistic logic. A Kripke frame is a pair $\langle S, \leq \rangle$ , where $\leq$ is a preorder, that is, a reflexive and transitive relation on $S$ . A Kripke model is a Kripke frame equipped with a valuation $V$ , that is, a function that assigns to each atomic formula an upward closed subset of $S$ (i.e., if $w \in V(p)$ and $w \leq 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:

1. (a) $w \nVdash \bot$ ,

2. (b) $w \Vdash \varphi \rightarrow \psi$ iff for any $v \geq w$ , if $v \Vdash \varphi$ , then $v \Vdash \psi$ ,

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

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

The relation is persistent: if $w \Vdash \varphi$ and $w \leq v$ , then $v \Vdash \varphi$ . We say that $\varphi$ is valid in a model $\langle S, \leq, 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 (Kripke, Reference Kripke, Dummett and Crossley1965). The recursive clauses for $\Vdash$ actually mirror some characteristic properties of $\vdash$ in inquisitive gsi-logics, as is shown in the following proposition.

This observation motivates the following construction of a characteristic Kripke model $\mathscr{M}_{\Lambda }=\langle S_{\Lambda }, \leq _{\Lambda }, V_{\Lambda } \rangle$ , where $S_{\Lambda }=\{ \alpha \mid \alpha \text{ is } {\vee}\text{-free and consistent} \}$ ; $\alpha \leq _{\Lambda } \beta$ iff $\beta \vdash _{\Lambda } \alpha$ ; $\alpha \in V_{\Lambda }(p)$ iff $\alpha \vdash _{\Lambda } p$ . Then Proposition 19 directly implies that $\Vdash$ in $\mathscr{M}_{\Lambda }$ coincides with $\vdash _{\Lambda }$ .

Note that the previous result is intuitively related to the fact that $\vee$ -free formulas are associated with statements and as such describe specific states of affairs (pieces of information), as opposed to questions. The logic of questions is determined by the logic of statements.

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

Using this observation, we can build from $D$ -substitutions a particular characteristic Kripke model $\mathscr{M}^{\Lambda }=\langle S^{\Lambda }, \leq ^{\Lambda }, V^{\Lambda } \rangle$ , where $S^{\Lambda }$ is the set of all $D$ -substitutions; $s \leq ^{\Lambda } t$ iff there is a $D$ -substitution $u$ such that $t = u \circ s$ ; $s \in V^{\Lambda }(p)$ iff $s \succ p$ .Footnote ⁷

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

The previous result follows from $SD$ -completeness of $\Lambda$ . Note that since $SD$ -completeness implies $SG$ -completeness, and thus $\Lambda$ is also $SG$ -complete, we could build the characteristic model also from all substitutions in $sub(\Lambda )$ rather than just from $D$ -substitutions. For inquisitive gsi-logics, $D$ -substitutions are equivalent to $H$ -substitutions because every Harrop formula is equivalent to a $\vee$ -free formula. However, we demonstrated in Proposition7 that $sub(\Lambda )$ may be substantially different from the classes of $D$ -substitutions and $H$ -substitutions.

In the rest of this section, we will look at the previous result from a different angle and spell out its meaning in purely algebraic terms. For this purpose, we will need some basic algebraic terminology. Recall that a Heyting algebra is a structure ${\mathscr{H}}{} = \langle H, \sqcap, \sqcup, \Rightarrow, 0 \rangle$ , where $\mathscr{A} = \langle A, \sqcap, \sqcup \rangle$ is a distributive lattice; $0$ is its least element with respect to the lattice ordering $\sqsubseteq$ ; and $\Rightarrow$ is a binary operation on $A$ satisfying

\begin{equation*} a \sqsubseteq b \Rightarrow c \text{ iff } a \sqcap b \sqsubseteq c. \end{equation*}

Let ${\mathscr{H}}_1 = \langle H_1, \sqcap _1, \sqcup _1, \Rightarrow _1, 0_1 \rangle$ , ${\mathscr{H}}_2 = \langle H_2, \sqcap _2, \sqcup _2, \Rightarrow _2, 0_2 \rangle$ be Heyting algebras. A homomorphism from ${\mathscr{H}}_1$ to ${\mathscr{H}}_2$ is a function $h:H_1 \to H_2$ satisfying: $h(a \sqcap _1 b)=h(a) \sqcap _2 h(b)$ , $h(a \sqcup _1 b)=h(a) \sqcup _2 h(b)$ , $h(a \Rightarrow _1 b)=h(a) \Rightarrow _2 h(b)$ , and $h(0_1)=0_2$ . An embedding of ${\mathscr{H}}_1$ into ${\mathscr{H}}_2$ is an injective homomorphism form ${\mathscr{H}}_1$ to ${\mathscr{H}}_2$ . An endomorphism on ${\mathscr{H}}\,$ is a homomorphism from ${\mathscr{H}}\,$ to ${\mathscr{H}}$ .

We keep fixed a gsi-logic $\Lambda$ . For any formula $\varphi$ , we define its equivalence class $[\varphi ]_{\Lambda } = \{\psi \mid \varphi \equiv _{\Lambda } \psi \}$ . The Lindenbaum–Tarski algebra of $\Lambda$ is the following Heyting algebra:

\begin{equation*} {\mathscr{H}}_{\Lambda } = \langle Prop(\Lambda ), \sqcap, \sqcup, \Rightarrow, 0_\Lambda \rangle, \end{equation*}

where $Prop(\Lambda )$ contains all the equivalence classes $[\varphi ]_{\Lambda }$ , for every formula $\varphi$ , and the operations are defined as follows:

\begin{equation*}\text{$[\varphi ]_\Lambda \sqcap [\psi ]_\Lambda = [ \varphi \wedge \psi ]_\Lambda $, $[\varphi ]_\Lambda \sqcup [\psi ]_\Lambda = [ \varphi \vee \psi ]_\Lambda $, $[\varphi ]_\Lambda \Rightarrow [\psi ]_\Lambda = [ \varphi \rightarrow \psi ]_\Lambda $, $0_\Lambda = [ \bot ]_\Lambda $.}\end{equation*}

Now we can observe that we can identify (a) substitutions under which $\Lambda$ is closed with arbitrary endomorphisms on the Lindenbaum–Tarski algebra of $\Lambda$ and (b) $D$ -substitutions with endomorphisms of a special kind.

Let us describe this idea more carefully. Recall that two substitutions $s, t$ are $\Lambda$ -equivalent if $s(p) \equiv _\Lambda t(p)$ , for every atomic formula $p$ . In that case, we write $s \sim _\Lambda t$ . The equivalence class of all substitutions equivalent to a substitution $s$ is denoted as $[s]_\Lambda$ . If clear from the context, we will be omitting the subscript $\Lambda$ .

Let $[s]$ be an equivalence class of substitutions. We say that $[s]$ is admissible if $[s] \subseteq sub(\Lambda )$ . Note that if $s \in sub(\Lambda )$ , then $[s]$ is admissible. We say that $[s]$ is declarative if there is a $D$ -substitution $t \in [s]$ . Moreover, we say that an endomorphism $h$ on ${\mathscr{H}}_{\Lambda }$ is declarative if for every atomic formula $p$ , there is a $\vee$ -free formula $\alpha \in h([p])$ .

Now we define a function assigning an endomorphism to any admissible equivalence class of substitutions. For any substitution $s \in sub(\Lambda )$ , we define:

\begin{equation*} [s]^{*}([\varphi ]) = [s(\varphi )].\end{equation*}

Note that this is a well defined function since if $s \sim t$ and $\varphi \equiv \psi$ , then $[s(\varphi )] = [t(\psi )]$ because $\Lambda$ is closed under $s$ . Moreover, we can observe that $[s]^{*}$ is indeed an endomorphism on ${\mathscr{H}}_{\Lambda }$ .

On the other hand, we define, for any endomorphism $h$ on ${\mathscr{H}}_{\Lambda }$ , a set of substitutions $h^{\circ }$ in this way:

\begin{equation*} h^{\circ } = \{ s \in sub(\Lambda ) \mid s(p) \in h([p]), \text{for every atomic formula } p\}. \end{equation*}

Let us demonstrate that $h^{\circ }$ is an admissible equivalence class of substitutions. We need to show that $h^{\circ }=[s]$ , for some substitution $s \in sub(\Lambda )$ . Take any substitution $s$ such that $s(p) \in h([p])$ , for every atomic formula $p$ . Assume $\varphi \in \Lambda$ . Then $s(\varphi ) \in h([\varphi ])=h([\top ])=[\top ]$ , and so $s(\varphi ) \in \Lambda$ . This means that $s \in sub(\Lambda )$ . Hence, $s \in h^{\circ }$ . Moreover, it holds that (a) if $t \in h^{\circ }$ , then $s \sim t$ , and (b) if $s \sim t$ , then $t \in h^{\circ }$ . Hence $[s] = h^{\circ }$ .

Proposition 21 shows that the two functions $*$ and $\circ$ are mutually inverse bijections between endomorphisms and all admissible classes of substitutions and, when suitably restricted, between declarative endomorphisms and declarative classes of substitutions.

A monoid is an algebraic structure $\mathscr{A}=\langle A, \cdot, e \rangle$ , where $\cdot$ is an associative operation on $A$ , and $e$ is a neutral element, that is, $e\cdot a = a \cdot e = a$ , for every $a \in A$ . Note that the Lindenbaum–Tarski algebra of $\Lambda$ determines the monoid of its endomorphisms $\mathscr{E}_\Lambda =\langle E_\Lambda, \circ, id \rangle$ , where $E_\Lambda$ is the set of all endomorphisms on ${\mathscr{H}}_{\Lambda }$ , $\circ$ is composition, and $id$ is the identity endomorphism. In the same way, ${\mathscr{H}}_\Lambda$ determines the monoid of its declarative endomorphisms $\mathscr{E}^{D}_\Lambda =\langle E^D_\Lambda, \circ, id \rangle$ .

Let $\mathscr{A}=\langle A, \cdot, e \rangle$ be a monoid. A set $I \subseteq A$ is called a left ideal in $A$ if $a \cdot i \in I$ for all $a \in A$ and $i \in I$ . Left ideals in $\mathscr{A}$ form a Heyting algebra $LeId(\mathscr{A})=\langle LeId(A), \cap, \cup, \Rrightarrow, \emptyset \rangle$ , where $LeId(A)$ is the set of all left ideals in $\mathscr{A}$ ; $\cap, \cup, \emptyset$ are just intersection, union, and the empty set; and $\Rrightarrow$ is defined as follows:

\begin{equation*} I \Rrightarrow J = \{ a \in A \mid \text{ for all}\, b \in A, \text{if}\, b \cdot a \in I \text{ then}\, b \cdot a \in J \}.\end{equation*}

Note that left ideals in $\mathscr{A}$ are precisely the downward closed sets of the so-called Green’s preorder on $\mathscr{A}$ defined as follows: $a \leq _{\mathscr{L}} b$ iff $a = c \cdot b$ , for some $c \in A$ . The algebra $LeId(\mathscr{A})$ is the Heyting algebra of such downward closed sets. Note that when defined on substitutions, the Green’s preorder $\leq _{\mathscr{L}}$ is the converse of the preoder considered above in the construction of the characteristic model $\mathscr{M}^{\Lambda }$ . For more details on these notions, see Grillet (Reference Grillet1995). We define functions $F_\Lambda$ from ${\mathscr{H}}_\Lambda$ to $LeId(\mathscr{E}_\Lambda )$ and $F^D_\Lambda$ from ${\mathscr{H}}_\Lambda$ to $LeId(\mathscr{E}^{D}_\Lambda )$ :

\begin{equation*} F_\Lambda ([\varphi ]_\Lambda ) = \{ h \in E_\Lambda \mid h([\varphi ]_\Lambda )=[\top ]_\Lambda \} \text{ and } F^D_\Lambda ([\varphi ]_\Lambda ) = \{ h \in E^D_\Lambda \mid h([\varphi ]_\Lambda )=[\top ]_\Lambda \}. \end{equation*}

The algebraic fact behind Theorem11 can now be spelled out in the following way.

Proof. We will consider the case of $F_\Lambda$ . To simplify the notation, we will be omitting the subscript $\Lambda$ , and we will write $h[\varphi ]$ and $F[\varphi ]$ instead of $h([\varphi ])$ and $F([\varphi ])$ . First, we will prove that $F$ is a homomorphism.

\begin{equation*} \begin{array}{lll} F([\varphi ] \sqcap [\psi ]) & = & \{ h \in E \mid h([\varphi ] \sqcap [\psi ])=[\top ] \} \\ & = & \{ h \in E \mid h[\varphi ] \sqcap h[\psi ]=[\top ] \} \\ & = & \{ h \in E \mid h[\varphi ]=[\top ] \text{ and } h[\psi ]=[\top ] \} \\ & = & \{ h \in E \mid h[\varphi ]=[\top ] \} \cap \{ h \in E \mid h[\psi ]=[\top ] \} \\ & = & F[\varphi ] \cap F[\psi ] \\[-8pt] & & \\ F([\varphi ] \sqcup [\psi ]) & = & \{ h \in E \mid h([\varphi ] \sqcup [\psi ])=[\top ] \} \\ & = & \{ h \in E \mid h[\varphi ] \sqcup h[\psi ]=[\top ] \} \\ & \overset {(a)}{=} & \{ h \in E \mid h[\varphi ]=[\top ] \text{ or } h[\psi ]=[\top ] \} \\ & = & \{ h \in E \mid h[\varphi ]=[\top ] \} \cup \{ h \in E \mid h[\psi ]=[\top ] \} \\ & = & F[\varphi ] \cup F[\psi ] \\[-8pt] & & \\ F([\varphi ] \Rightarrow [\psi ]) & = & \{ h \in E \mid h([\varphi ] \Rightarrow [\psi ])=[\top ] \} \\ & = & \{ h \in E \mid h[\varphi ] \Rightarrow h[\psi ]=[\top ] \} \\ & \overset {(b)}{=} & \{ h \in E \mid \text{ for all}\, g \in E, \text{if}\, g \circ h[\varphi ]=[\top ] \text{then} \,g \circ h[\psi ]=[\top ] \} \\ & = & \{ h \in E \mid \text{ for all}\, g \in E, \text{ if}\, g \circ h \in F[\varphi ] \text{ then} \,g \circ h \in F[\psi ] \} \\ & = & F[\varphi ]\Rrightarrow F[\psi ] \\ \end{array} \end{equation*}

The equation (a) is obtained by the disjunction property and the equation (b) by SG-completeness of $\Lambda$ . Moreover, it holds that $F[\bot ]=\{ h \in E \mid h[\bot ]=[\top ] \}=\emptyset$ , which finishes the proof that $F$ is a homomorphism. It remains to be proved that $F$ is injective. Assume $F[\varphi ]=F[\psi ]$ . This means that for every $h \in E$ , $h[\varphi ]=[\top ]$ iff $h[\psi ]=[\top ]$ . It follows, by SG-completeness, that $\varphi \equiv \psi$ , that is, $[\varphi ]=[\psi ]$ .

The case of $F^D_\Lambda$ is strongly analogous. Only in the justification of the equation (b) and in the justification of injectivity we have to refer to SD-completeness instead of SG-completeness.

The construction that we described in this section is analogous to the familiar canonical model construction, where we represent every proposition by a set of prime theories that make the proposition true. Our untypical construction shows that in the case of inquisitive gsi-logics, we can similarly represent every proposition by a set of substitutions that make the proposition logically true. Unfortunately, we do not have a deeper philosophical explanation of this fact, but we find it quite intriguing. In purely algebraic terms, we have shown that every inquisitive gsi-logic has the property that its Lindenbaum–Tarski algebra can be embedded into the algebra of left ideals on the monoid of its endomorphisms.