Subintuitionistic logics and their modal companions: a nested approach

Abstract

In the present paper we deal with subintuitionistic logics and their modal companions. In particular, we introduce nested calculi for subintuitionistic systems and for modal logics in the $\mathbf{S}\mathbf{5}$ modal cube ranging from $\mathbf{K}$ to $\mathbf{S}\mathbf{4}$. The latter calculi differ from standard nested systems, as there are multiple rules handling the modal operator. As an upshot, we get a purely syntactic proof of the Gödel-McKinsey-Tarski embedding which preserves the structure and the height of the derivations. Finally, we obtain a conservativity result for classical logic over a weak subintuitionistic system.

1. Introduction

Constructive reasoning is distilled in intuitionistic logic introduced by Arend Heyting based on the seminal work in the field of mathematics by Brouwer. Intuitionistic logic has been widely investigated both from the semantic and the syntactic viewpoint (Dummett, 1977).

The semantic characterisations of intuitionistic logic – in particular the one in terms of Kripke frames – brings to the fore the connections between the modal logic $\mathbf{S}\mathbf{4}$ and constructive logic. Modal logics weaker than $\mathbf{S}\mathbf{4}$, for example $\mathbf{K}$, $\mathbf{T}$ and so forth, have received considerable attention in the literature (Chagrov & Zakharyaschev, 1997).

In contrast, systems weaker than intuitionistic logic, also called subintuitionistic logic, have not been extensively studied [the only exception being Visser's logic (Visser, 1981)]. These logics were introduced in Corsi (1987) and later studied semantically and syntactically in (Celani & Jansana, 2001, 2005; Moniri & Shirmohammadzadeh Maleki, 2015; Restall, 1994; Shirmohammadzadeh Maleki & De Jongh, 2017).

Sequent calculi for subintuitionistic logic have been designed in the form of labelled systems (Negri, 2021). Currently, there is not a satisfactory analytic proof theory based on internal calculi available for this family of logics [an exception being the natural deduction system for Visser's logic (Suzuki & Ono, 1997)], i.e. calculi in which every sequent can be interpreted as a formula of the language, for the family of subintuitionistic logics. An interesting proof-theoretic approach in this sense is given in Ishigaki and Kikuchi (2007) where tree-sequents are introduced for first-order subintuitionistic logics and they are proved to be sound and complete with respect to Kripkean semantics. Tree-sequents are tightly connected to nested sequents, but the analysis cannot be regarded as proof-theoretically satisfactory, insofar as the structural properties of the systems are obtained indirectly via semantic methods.

In this paper, we aim to fill this gap by introducing nested calculi for these logics. In particular, we propose nested calculi for subintuitionistic logics corresponding (in the sense of the modal interpretation) to the modal logics $\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}$ and for Visser's logic.

The calculi are obtained through suitable modifications of a base system introduced in Ciabattoni et al. (2022) and, independently in Lyon (2021) [which is in turn based on a system by Fitting (2014)]. The systems are thus modular, in the sense that they can be obtained by adding or modifying rules starting from a base system. Furthermore, they satisfy good structural properties, namely the admissibility of certain structural rules and the cut rule. All these properties are established through purely syntactic methods via inductive arguments.

This is interesting as it can be used to deepen our understanding of subintuitionistic logics and not consider them as (conceptually and technically) parasitical with respect to their modal companions. In addition to that, we propose a new family of modal nested calculi. These systems bear a strong resemblance to the ones introduced in Brünnler (2009), but they differ insofar as they have multiple rules governing the modal operator □.

This alternative formulation of the modal calculi enables us to give a new proof of the modal interpretation of subintuitionistic logics. The interpretation of constructive systems into modal logics was first proposed by Gódel (1933). He proved the soundness of the translation, i.e. every proof of an intuitionistic formula can be transformed into a proof of the translated formula, and conjectured the faithfulness of the translation, i.e. every proof of a translated formula can be transformed into a proof of the formula in the intuitionistic system. The faithfulness was formally proved in 1948 by McKinsey and Tarski (1948) using algebraic and topological methods, thus leaving unsolved the task of finding a syntactic proof of the embedding.

Various syntactic proofs of the embedding have been provided in the literature, see Dyckhoff and Negri (2012), Troelstra and Schwichtenberg (1996), and Tesi and Negri (2021, 2023). A proof for Visser's logic which is based on standard sequent calculi is given in Yamasaki and Sano (2017). However, the latter calculi are based on a rather involved rule for the implicative connectives.

Furthermore, the method has the following advantages:

• Once the structural properties of the systems are spelled out, the proof is rather elegant and concise.

• The proof transformations are minimal in the sense that the structure of intuitionistic and modal proofs are closely related.

• The proof uses internal calculi and it gives a refinement of usual results, by preserving the height of the derivations in both directions of the translation (with the only exception of the embedding of Visser's logic).

The latter point is also conceptually interesting. Indeed, in this case the preservation of the height reveals that every line of an intuitionistic derivation can be immediately associated with one in the modal calculus and conversely. Therefore the resulting systems can be regarded as identical under the translation.

Finally, we connect the methodology here proposed with classical themes in the literature on proof theory and non-classical logics. In particular, we prove a strengthening of Barr's theorem in the propositional setting (see Negri, 2003 for a proof-theoretic proof of the result in the first-order setting), by showing that classical logic is conservative over the subintuitionistic logic whose modal companion is $\mathbf{T}$. This proves that constructive reasoning in propositional geometric logic can be carried out in systems which are significantly weaker than intuitionistic logic.

The plan of the paper is as follows. In Section 2, we spell out some preliminaries concerning nested calculi. Section 3 introduces the nested calculi for subintuitionistic logics whose structural properties are established in Section 4. Section 5 introduces new systems for modal logics weaker than $\mathbf{S}\mathbf{4}$ in the $\mathbf{S}\mathbf{5}$ modal cube. These calculi are exploited in Section 6 to give a new proof of the modal embedding for subintuitionistic logics. Section 7 explores conservativity results with respect to classical logic. Finally, Section 8 discusses possible extensions of the present work.

2. Preliminaries

We work with two different languages: the one of (sub)intuitionistic logic(s) and the one of modal logics. The first language $\mathsf{FM}$ contains a denumerable set of atomic formula $p,q,r,\dots$, the zeroary connective ⊥ and is closed under the connectives $\wedge ,\vee$ and →. Negation is defined as $\mathrm{\neg A}\equiv A\to \mathrm{\perp }$. The modal language ${\mathsf{FM}}^{◻}$ is obtained by adding to $\mathsf{FM}$ the unary connective □.

A nested sequent is a finite tree of multisets of formulas. In ordinary sequents we distinguish between the left and the right-hand side of the turnstile. To make this distinction in nested sequents, we use polarities on formulas. There are two polarities, input (intuitively as if on the left of the turnstile in the conventional sequent calculus), denoted by a • superscript and output (intuitively as if on the right of the turnstile), denoted by a ° superscript. Now, a nested sequent can be written as: (1) $\mathrm{\Gamma }=A_1^{\bullet },\dots ,A_m^{\bullet },B_1^{\circ },\dots ,B_n^{\circ },\left[{\mathrm{\Gamma }}_1\right],\dots ,\left[{\mathrm{\Gamma }}_k\right]$(1) where $A_1^{\bullet },\dots ,A_m^{\bullet },B_1^{\circ },\dots ,B_n^{\circ }$ is the multiset of formulas at the root of the sequent tree of Γ, and where ${\mathrm{\Gamma }}_1,\dots ,{\mathrm{\Gamma }}_k$ are its immediate subtrees. We use ∅ the empty sequent, i.e. where m = n = k = 0 in (1(1) $\mathrm{\Gamma }=A_1^{\bullet },\dots ,A_m^{\bullet },B_1^{\circ },\dots ,B_n^{\circ },\left[{\mathrm{\Gamma }}_1\right],\dots ,\left[{\mathrm{\Gamma }}_k\right]$(1) ) above. We use capital Greek letters Γ, Δ, Σ, …, to denote nested sequents, and we assume that the associativity and commutativity of the comma are implicit in our systems, and that ∅ acts as its unit. We write for $A_1^{\bullet },\dots ,A_m^{\bullet }$ and for $B_1^{\circ },\dots ,B_n^{\circ },\left[{\mathrm{\Gamma }}_1\right],\dots ,\left[{\mathrm{\Gamma }}_k\right]$ if Γ is as in (1(1) $\mathrm{\Gamma }=A_1^{\bullet },\dots ,A_m^{\bullet },B_1^{\circ },\dots ,B_n^{\circ },\left[{\mathrm{\Gamma }}_1\right],\dots ,\left[{\mathrm{\Gamma }}_k\right]$(1) ) above. In other words, for every nested sequent Γ we have that . More generally, we will write , , , …, for multisets of input formulas (i.e. all formulas have •-polarity, and there are no nestings), and we will write , , , …, for sequents that have only °-formulas at their root nodes (i.e. there are no •-formulas at the root, but there can be nestings with •-formulas inside).

Depending on the language, there are two different possible interpretations of nested sequent. The corresponding formula in $\mathsf{FM}$ of the sequent in (1(1) $\mathrm{\Gamma }=A_1^{\bullet },\dots ,A_m^{\bullet },B_1^{\circ },\dots ,B_n^{\circ },\left[{\mathrm{\Gamma }}_1\right],\dots ,\left[{\mathrm{\Gamma }}_k\right]$(1) ) above is defined as (2) $\mathit{fm}\left(\mathrm{\Gamma }\right)=\underset{i=1}{\overset{m}{\bigwedge }}{A}_i\to (\underset{j=1}{\overset{n}{\bigvee }}{B}_j\vee \underset{l=1}{\overset{k}{\bigvee }}\mathit{fm}({\mathrm{\Gamma }}_l\left)\right)$(2) The corresponding formula in ${\mathsf{FM}}_{◻}$ of the sequent in (1(1) $\mathrm{\Gamma }=A_1^{\bullet },\dots ,A_m^{\bullet },B_1^{\circ },\dots ,B_n^{\circ },\left[{\mathrm{\Gamma }}_1\right],\dots ,\left[{\mathrm{\Gamma }}_k\right]$(1) ) above is defined as (3) $\mathit{fm}\left(\mathrm{\Gamma }\right)=\underset{i=1}{\overset{m}{\bigwedge }}{A}_i\to (\underset{j=1}{\overset{n}{\bigvee }}{B}_j\vee \underset{l=1}{\overset{k}{\bigvee }}◻\mathit{fm}({\mathrm{\Gamma }}_l\left)\right)$(3) A (sequent) context is a nested sequent with a hole $\left\{\right\}$, taking the place of a formula. Contexts are denoted by $\mathrm{\Gamma }\left\{\right\}$, and $\mathrm{\Gamma }\left\{\mathrm{\Delta }\right\}$ is the sequent obtained from $\mathrm{\Gamma }\left\{\right\}$ by replacing the occurrence of with Δ. We write for the sequent obtained from by removing the (i.e. the hole is filled with nothing). We will use the notation as abbreviation for .

Example

Let . We have that:

3. Nested Sequent Calculus for (sub)intuitionistic propositional logic(s)

We start from the calculus $\mathbf{NSI}$ (independently presented in Ciabattoni et al., 2022; Lyon, 2021), a variant of Fitting's calculus for intuitionistic propositional logic (Fitting, 2014) designed to have all invertible rules, and to admit a direct cut elimination proof. The system $\mathbf{NSI}$, whose rules are shown in Figure 1 (and the cut rule is displayed in Figure 2), is obtained from Fitting's calculus by using multisets instead of sets and by absorbing the rule $\mathsf{l}$ (see Figure 3) into the initial sequents and the rule .

Figure 1. The calculus $\mathbf{NSI}$.

Figure 2. The cut rule.

Figure 3. Admissible structural rules.

We now introduce starting from the system $\mathbf{NSI}$ sequent calculi for various subintuitionistic logics. Due to their connections with modal logics (to be detailed below) in the $\mathbf{S}\mathbf{5}-$cube, we shall refer to them as $\mathbf{NSIX}$, where $\mathbf{X}$ is a modal logic, with the exception of the nested sequent calculus for Visser's logic, which we label as $\mathbf{NSIB}$.

1. The system $\mathbf{NSIK}$ is obtained by (i) removing $\mathsf{ax}$ and substituting it with and (ii) replacing the rule ${\to }^{\bullet }$ with:

   

2. The system $\mathbf{NSIT}$ is obtained from the system $\mathbf{NSIK}$ adding the following rule:

   

3. The system $\mathbf{NSIK}\mathbf{4}$ is obtained from the system $\mathbf{NSIK}$ by substituting the rule ${\to }_{\mathsf{k}}^{\bullet }$ the following rule:

   

4. The system $\mathbf{NSIB}$ is obtained from the system $\mathbf{NSI}$ by substituting the rule ${\to }^{\bullet }$ with the following rule:

   

Terminology: As in standard sequent calculi, we call context the part left unchanged from premises to conclusions, we call principal the introduced formula in any logical rule different from ${\to }^{\bullet }$. In the latter rule the principal formula is the implication ${A\to B}^{\bullet }$ in the conclusion. The formulas , , and in initial sequents are active part/formulas. When not differently specified, we shall write $\mathbf{NSIX}$ to denote all the subintuitionistic systems, with $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{4}\mathbf{,}\mathbf{B}\right\}$.

We recall that a rule is admissible, whenever the derivability of the premises entails the derivability of the conclusion. A rule is invertible if, whenever the conclusion is derivable, so is each of its premises. The height of a derivation is the number of nodes minus one in a branch of maximal length. These notions can be strengthened with the property of being height-preserving, i.e. the height of the derivation of the conclusion is less or equal to the one of each premise. We use a single line to denote an application of a rule and a double dashed line to indicate the application of a Lemma or a Theorem to transform a proof.

Let us mention two useful features of $\mathbf{NSI}$ and its subsystems $\mathbf{NSIX}$. The first is standard in well-designed sequent-style calculi: the general form of the ${\mathsf{ax}}^{\prime }$-rule is derivable.

Lemma 3.1

Axiom expansion

The sequent is derivable in $\mathbf{NSI}$ and $\mathbf{NSIX}$ for every context Γ and every formula A.

Proof.

By induction on the degree of the formula A. We detail the case in $\mathbf{NSIK}$ in which A is of the shape $B\to C$, the other cases being similar.

The premises are derivable by the induction hypothesis.

The systems $\mathbf{NSI}$ and $\mathbf{NSIB}$ allow for a strengthening of the previous result.

Lemma 3.2

Axiom expansion

The sequent is derivable in $\mathbf{NSI}$ and $\mathbf{NSIB}$ for every context $\mathrm{\Gamma },\mathrm{\Pi }$ and every formula A.

Proof.

We discuss the case of the implication in the system $\mathbf{NSIB}$; the case of $\mathbf{NSI}$ is analogous.

The premises are derivable by the induction hypothesis.

The second feature concerns the admissibility of the necessitation and the denecessitation rules.

Lemma 3.3

The rules:

are height-preserving admissible in $\mathbf{NSI}$ and $\mathbf{NSIX}$.

Proof.

Immediate by induction on the height n of the derivation of the premise noticing that initial sequents and rules are independent with respect to the removal or the addition of an outermost box.

4. Syntactic cut elimination for subintuitionistic logics

In this section, we discuss and establish the main structural properties of the systems $\mathbf{NSI}$ and $\mathbf{NSIX}$, with $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{4}\mathbf{,}\mathbf{B}\right\}$. In what follows IH denotes the application of the inductive hypothesis.

Lemma 4.1

The weakening rule $\mathsf{w}$ is height-preserving admissible in $\mathbf{NSI}$ and in the systems $\mathbf{NSIX}$.

Proof.

By induction on the height n of the derivation of . If n = 0, then is an initial sequent and so is . If n>0, we apply the induction hypothesis to the premise(s) of the last rule applied and then the rule again.

Remark

Let us observe that various subintuitionistic logic do not satisfy the a fortiori axiom $A\to (B\to A)$. For example, the formula $(p\to (q\to p){)}^{\circ }$ is not derivable in the system $\mathbf{NSIK}$. By contrast, the weakening rule is height-preserving admissible in every system here considered. This is interesting as it shows that structural rules in the sequent calculus can be independent of the validity of corresponding logical principles.

Lemma 4.2

Every rule in $\mathbf{NSI}$ and in the systems $\mathbf{NSIX}$ is height-preserving invertible.

Proof.

By induction on the height n of the derivation of the conclusion of each rule.

• The left rules for the implication are height-preserving invertible by the height-preserving admissibility of the rule of weakening (Lemma 4.1).

• We discuss the rule . We prove that whenever is derivable, so is and the height is preserved.

  	–	If n = 0, then is an initial sequent. So is an initial sequent too, because compound formulas are never principal in initial sequents.
  	–	If n>0 and ${A\to B}^{\circ }$ is not principal, then we apply the induction hypothesis to each of the premise(s) and then we apply the rule again. Let us give a concrete example of this qualitative analysis. Suppose the last rule applied is (we assume w.l.o.g. that the principal formula is at the same level of nesting of $A\to B$). We proceed as follows:
  	–	If n>0 and ${A\to B}^{\circ }$ is principal, then the premise yields the desired conclusion.

  The proofs for the conjunction and disjunction rules are similar and follow the pattern detailed, for example, in chapter 3 in Troelstra and Schwichtenberg (1996) or in Brünnler (2009).

The invertibility of every rule is easily seen to entail the height-preserving admissibility of the rule of contraction.

Lemma 4.3

The contraction rule $\mathsf{c}$ is height-preserving admissible in $\mathbf{NSI}$ and in the systems $\mathbf{NSIX}$, with $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{B}\right\}$.

Proof.

By induction on the height n of the derivation of . If is an initial sequent, then so is . If n>0 and the principal formula is not in Δ, we apply the induction hypothesis to each of the premises and then the rule again. If n>0 and the principal formula is in Δ, we exploit the height-preserving invertibility of the logical rules as shown below in the case of a unary rule:

The application of $\mathsf{c}$ is removed invoking the induction hypothesis which can be applied because the height is preserved by the invertibility (see Lemma 4.2). The case of the binary rule is:

Once again the applications of contraction are removed by induction on the height of the derivation.

Let us give a concrete example of this qualitative analysis. Suppose that the formula $(A\to B{)}^{\circ }$ is principal in Δ. We have:

Remark

Let us observe that, as in the case of the weakening rule, the admissibility of the rule of contraction does not grant the derivability of the corresponding logical principle. Namely, the sequent ${(p\to (p\to r\left)\right)\to (p\to r)}^{\circ }$ is not derivable in $\mathbf{NSIK}\mathbf{,}\mathbf{NSIK}\mathbf{4}\mathbf{,}\mathbf{NSIB}$ as a root-first application of the rules easily shows.

The way we formulated the rules in $\mathbf{NSI}$ and in $\mathbf{NSIB}$ allows us to establish the admissibility of the $\mathsf{l}$-rule.

Lemma 4.4

The $\mathsf{l}$-rule is height-preserving admissible in $\mathbf{NSIB}$ and in $\mathbf{NSI}$.

Proof.

We discuss the case of the system $\mathbf{NSIB}$, the case of $\mathbf{NSI}$ is similar. Proceed by induction on the height n of the derivation of the premise of the rule. If n = 0, then is an initial sequent and so is . If n>0 and no formula in Σ is principal, we apply the induction hypothesis to the premise(s) of the rule and then the rule again.

If a formula in is principal in or , we apply the induction hypothesis, e.g.

We discuss now a case specific to the system $\mathbf{NSIB}$, the one for $\mathbf{NSI}$ is analogous. If a formula $A^{\bullet }$ in is principal in ${\to }^{\bullet }$ as in

we apply the induction hypothesis and the rule ${\to }_{\mathsf{4}}^{\bullet }$, as in

◼

Notice that the admissibility of the lift rule entails the derivability of the a fortiori axiom $A\to (B\to A)$.

Lemma 4.5

The lift rule is not admissible in the calculi $\mathbf{NSIK}\mathbf{,}\mathbf{NSIT}\mathbf{,}\mathbf{NSIK}\mathbf{4}$.

Proof.

Suppose it was, then the sequent ${p\to (q\to p)}^{\circ }$ would be derivable as follows:

but this is not possible as the sequent is not derivable in the above mentioned calculi. Indeed, a root-first application of the rules in all the three calculi would give:

but no rule is applicable to the topmost sequent and thus it is underivable.

We now show the admissibility of a rule which is crucial in order to establish cut elimination and which merges two boxed sequents into one.

Lemma 4.6

The rule:

is height-preserving admissible in $\mathbf{NSI}$ and in $\mathbf{NSIX}$, with $\mathbf{X}\in \{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{B}\}$.

Proof.

We discuss the case of the system $\mathbf{NSIK}$, the other cases are similar. The proof is by induction on the height of the derivation of . If $\mathrm{\Gamma }\left\{\right[\mathrm{\Delta }],[\mathrm{\Sigma }\left]\right\}$ is an initial sequent, so is $\mathrm{\Gamma }\left\{\right[\mathrm{\Delta },\mathrm{\Sigma }\left]\right\}$. If it is the conclusion of a rule, we simply apply the induction hypothesis and then the rule again. To witness an example, we consider the rule ${\to }_{\mathsf{k}}^{\bullet }$:

We construct the following derivation:

Next, we show the admissibility of the rule ${\mathsf{4}}^{\prime }$ which holds for $\mathbf{NSI}$, and $\mathbf{NSIB}$.

Lemma 4.7

The ${\mathsf{4}}^{\prime }$-rule is height-preserving admissible in $\mathbf{NSI}$ and $\mathbf{NSIB}$.

Proof.

We discuss the cases of the two systems simultaneously arguing by induction on the height n of the derivation of the rule premise. If is an initial sequent, then so is . If n>0 we assume that a formula in is principal, otherwise the proof is trivial. We apply the induction hypothesis to the premise(s) of the rule and then the rule again. For example, if the last rule applied is , we have:

Notice that the rule ${\mathsf{4}}^{\prime }$ is not admissible in the system $\mathbf{NSIK}\mathbf{4}$. Indeed, only a weaker form of the rule is admissible. In particular, the admissibility breaks down in the presence of initial sequents.

Lemma 4.8

The rule ${\mathsf{4}}^{\prime }$ is not admissible in $\mathbf{NSIK}\mathbf{4}$.

Proof.

Consider the case of the derivable sequent . If the rule was admissible, then the sequent would be derivable too, but this is not the case.

The rule $\mathsf{4}$ is admissible in $\mathbf{NSIK}\mathbf{4}$ (and, consequently, also in $\mathbf{NSIB}$ and in $\mathbf{NSI}$).

Lemma 4.9

The rule:

is height-preserving admissible in $\mathbf{NSIK}\mathbf{4}$.

Proof.

The proof is by induction on the height of the derivation and follows the same pattern as the one detailed for $\mathbf{NSI}$ and $\mathbf{NSIB}$. Notice that the pathological case of initial sequents is now removed due to the shape of $\left[\mathrm{\Sigma }\right]$.

Lemma 4.10

The $\mathsf{lw}$-rule is height-preserving admissible in $\mathbf{NSI}$ and $\mathbf{NSIB}$.

Proof.

The $\mathsf{lw}$-rule is derivable with the following height-preserving steps:

A weaker version of the lower rule $\mathsf{wlw}$ is height-preserving admissible in $\mathbf{NSIK}\mathbf{4}$.

Lemma 4.11

The rule:

is height-preserving admissible in $\mathbf{NSIK}\mathbf{4}$.

Proof.

We proceed as follows:

Finally, we show the admissibility of the rule $\mathsf{t}$ which corresponds to a form of reflexivity in terms of Kripkean semantics.

Lemma 4.12

The $\mathsf{t}$-rule is height-preserving admissible in $\mathbf{NSI}$ and in $\mathbf{NSIT}$.

Proof.

We discuss the case of $\mathbf{NSIT}$. By induction on the height n of the premise . If n = 0, then is an initial sequent and so is . If n>0, we apply the induction hypothesis to the premise(s) and then the rule again. As an example, consider the case in which the last rule applied is ${\to }_{\mathsf{k}}^{\bullet }$ and formulas are introduced (bottom-up) in $\left[\mathrm{\Delta }\right]$. We have:

We construct the following derivation:

where the applications of $\mathsf{t}$ are removed by induction hypothesis.

We now state and prove cut-elimination for the base system $\mathbf{NSIK}$. When proving the cut admissibility theorem we will replace the cuts with cuts of smaller height or on formulas of lesser degree. With a slight abuse of notation, we shall label as $\mathsf{cut}$ applications of the induction hypothesis in proof transformations. We will explicitly indicate the applications of the induction hypothesis after each proof transformation.

Theorem 4.13

Cut admissibility

The $\mathsf{cut}$-rule is admissible for $\mathbf{NSIK}$.

Proof.

We consider an uppermost cut and proceed by induction on the lexicographically ordered pair $(c,n)$ where c is the degree of its cut formula and n is the height of the derivation of .¹

• If n = 0, then is an initial sequent. If is not active, is an initial sequent too. If is active in an initial sequent, we have:

  

  The cut is eliminated as follows:

  

• If n>0 and is not principal, we apply the invertibility of the corresponding rule to , permute the cut upwards, and remove it by secondary induction hypothesis. E.g. in the case of a binary rule we have:

  

  We construct the following derivation:

  

  where Invρ denote applications of Lemma 4.2 to obtain derivations of the premises to cut. Indeed, notice that if the cut formula is not active in the last rule applied ρ, the rule acts only on the context Γ modifying it in the premises: ${\mathrm{\Gamma }}^{\prime }\left\{A^{\bullet }\right\}$ and ${\mathrm{\Gamma }}^{″}\left\{A^{\bullet }\right\}$ (looking bottom-up). This is why the application of the invertibility lemma w.r.t. ρ to the sequent $\mathrm{\Gamma }\left\{A^{\circ }\right\}$ gives exactly ${\mathrm{\Gamma }}^{\prime }\left\{A^{\circ }\right\}$ and ${\mathrm{\Gamma }}^{″}\left\{A^{\circ }\right\}$. The cuts are removed by the secondary induction hypothesis because the derivations of ${\mathrm{\Gamma }}^{\prime }\left\{A^{\bullet }\right\}$ and ${\mathrm{\Gamma }}^{″}\left\{A^{\bullet }\right\}$ have lower height than the one of .

• If n>0 and is principal in ∧ or ∨, the case is handled in the usual way using the rules invertibility. For example

  

  is eliminated as follows (each cut is on a formula of lesser degree):

  

• If n>0 and is principal in ${\to }^{\bullet }$

  

  is handled as follows. We first construct a derivation of :

  

  The cut is removed by the secondary induction hypothesis. A symmetrical derivation yields , and the reduction is completed as follows:

  

  The cuts are removed by the primary induction hypothesis on the degree of the cut formula.

The cut elimination theorem for the extensions of the system $\mathbf{NSIK}$ is handled by exploiting the dedicated structural rules that are admissible.

Theorem 4.14

The cut rule is admissible in $\mathbf{NSIT}\mathbf{,}\mathbf{NSIK}\mathbf{4}\mathbf{,}\mathbf{NSIB}$ and in $\mathbf{NSI}$.

Proof.

The strategy remains unchanged. The only new cases to detail are the ones involving either initial sequents or the implication, as the rules change. We discuss the cases separately:

• In system $\mathbf{NSIT}$ the new case arising is:

  

  We first make two cross-cuts to obtain derivations of and of . Then we have:

  

  all the displayed cuts are removed by the primary induction hypothesis on the degree of the cut formula.

• In the case of $\mathbf{NSIB}$ we need to discuss the case of initial sequents and the new case for implication.

  

  We proceed as follows:

  

  The case for implication is as follows:

  

  We proceed as follows:

  

  all the cuts are removed by primary induction hypothesis.

• The cut admissibility for $\mathbf{NSI}$ and $\mathbf{NSIK}\mathbf{4}$ follows from a combination of the methods detailed for $\mathbf{NSIT}$ and $\mathbf{NSIB}$.

This concludes the syntactic investigation of the subintuitionistic logics. We have provided nested sequents for a wide family of such logics.

4.1. Soundness and completeness for subintuitionistic systems

We now present the Kripkean semantics for subintuitionistic logics and we establish soundness and completeness with respect to our systems. The soundness result follows straightforwardly by induction on the height of the derivation. With respect to completeness, we will show that a complete calculus can be embedded in the corresponding nested system, thus yielding the desired result.

Definition 4.1

A subintuitionistic frame is an ordered pair $\mathcal{F}=(W,⩽)$, where $W\ne \mathrm{\varnothing }$ and ≤ a binary relation on it.

Definition 4.2

A subintuitionistic model is an ordered pair $\mathcal{M}=(\mathcal{F},v)$ where $\mathcal{F}$ is a subintuitionistic frame and $v:\mathrm{AT}\to \mathcal{P}\left(W\right)$ is the valuation function.

Notice that the range of the valuation function is the entire power set of W and not only the set of its open subsets as in the case of intuitionistic logic. When v maps atomic formulas to open sets we say that it is monotonic.

Definition 4.3

Given a subintuitionistic model $\mathcal{M}$, a world $x\in \mathcal{M}$, $A\in \mathsf{FM}$, the satisfiability conditions for A are inductively defined:

• $x{\models }_{\mathcal{M}}p$ if and only if $x\in v\left(p\right)$

• $x{⊭}_{\mathcal{M}}\mathrm{\perp }$

• $x{\models }_{\mathcal{M}}B\wedge C$ if and only if $x{\models }_{\mathcal{M}}B$ and $x{\models }_{\mathcal{M}}C$

• $x{\models }_{\mathcal{M}}B\vee C$ if and only if $x{\models }_{\mathcal{M}}B$ or $x{\models }_{\mathcal{M}}C$

• $x{\models }_{\mathcal{M}}B\to C$ if and only if for every y such that $x⩽y$, whenever $y{\models }_{\mathcal{M}}B$, then $y{\models }_{\mathcal{M}}C$

Definition 4.4

$A\in \mathsf{FM}$ is true in a subintuitionistic model, in symbols ${\models }_{\mathcal{M}}A$, iff for every $x\in \mathcal{M}$, $x{\models }_{\mathcal{M}}A$.

Definition 4.5

$A\in \mathsf{FM}$ is a logical truth with respect to a class of subintuitionistic frames $\mathcal{C}$, in symbols ${\models }_{\mathcal{C}}A$, iff for every model $\mathcal{M}$ whose frame is in $\mathcal{C}$, ${\models }_{\mathcal{M}}A$.

The soundness and completeness proofs of the previous section can be adapted so as to cover the family of subintuitionistic logics. To show the completeness of the nested systems, we embed the sequent calculi presented in Celani and Jansana (2001) for subintuitionistic logics. We recall the formulation of the base system $\mathbf{GSIK}$ and its extensions.

Table

$\mathbf{GSIK}$
Initial Sequents
Structural rules
Logical rules

The extensions are obtained by adding the rules:

The extensions of $\mathbf{GSIK}$ are thus defined: $\mathbf{GSIT}$ is obtained by adding the rule MP to $\mathbf{GSIK}$, $\mathbf{GSIK}\mathbf{4}$ is obtained by adding the rule A fortiori to $\mathbf{GSIK}$, $\mathbf{GSIB}$ is obtained by adding the rule Visser to $\mathbf{GSIK}$. We have the following characterisation results.

Theorem 4.15

The following statements hold:

• $\mathbf{GSIK}$ is sound and complete with respect to the class of all subintuitionistic Kripke frames.

• $\mathbf{GSIT}$ is sound and complete with respect to the class of all reflexive subintuitionistic Kripke frames.

• $\mathbf{GSIK}\mathbf{4}$ is sound and complete with respect to the class of all transitive subintuitionistic Kripke frames.

• $\mathbf{GSIB}$ is sound and complete with respect to the class of all transitive subintuitionistic Kripke frames with a monotonic valuation.

Proof.

The reader is referred to Celani and Jansana (2001).

Theorem 4.16

For $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{B}\right\}$, if $\mathbf{GSIX}$ proves $\mathrm{\Gamma }\Rightarrow A$, then $\mathbf{NSIX}$ derives ${\mathrm{\Gamma }}^{\bullet },A^{\circ }$.

Proof.

The proof is by induction on the height of the derivation in the calculus $\mathbf{GSIX}$. We limit ourselves to considering the cases of MP, A fortiori and V isser the other being rather straightforward.

• In the case of MP (specific to $\mathbf{GSIT}$), we proceed as follows:

  

  Hence the rule MP is admissible in $\mathbf{NSIT}$.

• In the case of A fortiori (specific to $\mathbf{GSI}\mathbf{4}$), we proceed as follows:

  

  Hence the rule A fortiori is admissible in $\mathbf{NSIK}\mathbf{4}$.

• In the case of Visser's rule we argue as follows:

  

  Hence the rule V isser is admissible in $\mathbf{NSIB}$.

As a result, we obtain indirect completeness results for our nested systems for subintuitionistic logics.

Theorem 4.17

The following statements hold:

• $\mathbf{NSIK}$ is sound and complete with respect to the class of all subintuitionistic Kripke frames.

• $\mathbf{NSIT}$ is sound and complete with respect to the class of all reflexive subintuitionistic Kripke frames.

• $\mathbf{NSIK}\mathbf{4}$ is sound and complete with respect to the class of all transitive subintuitionistic Kripke frames.

• $\mathbf{NSIB}$ is sound and complete with respect to the class of all transitive subintuitionistic Kripke frames with a monotonic valuation.

Proof.

Soundness follows from a routine induction on the height of the derivation. Completeness stems from the embedding of the corresponding sequent calculi $\mathbf{GSIX}$. In particular, if A is valid in the class of every subintuitionistic Kripke frame, then by Theorem 4.15 it is derivable in $\mathbf{GSIK}$, so by Theorem 4.16 is derivable in $\mathbf{NSIK}$. The argument can be repeated for the other systems.

Completeness for the system $\mathbf{NSI}$ w.r.t. intuitionistic logic was established in Ciabattoni et al. (2022). Having established the completeness of our systems and their analyticity, we can now turn our attention to modal systems and a new presentation of nested calculi for such logics.

5. Decomposed nested systems for modal logics

We now present a new nested sequent system for $\mathbf{S}\mathbf{4}$ -- $\mathbf{NSS}\mathbf{4}$ -- which is specifically tailored to provide an extremely simple proof of the soundness and the faithfulness of the modal interpretation of intuitionistic logic. The rules are displayed in the table below. The modal rules are split according to the shape of the formulas in the scope of the modal operator □. For this reason, we shall label the system as a decomposed nested system for $\mathbf{S}\mathbf{4}$.

Table

Initial Sequents
Logical Rules
Modal Rules
The calculus $\mathbf{NSS}\mathbf{4}$

The systems corresponding to the modal logics $\mathbf{K}\mathbf{,}\mathbf{K}\mathbf{4}$ and $\mathbf{T}$ are obtained via suitable modifications of the rules of the calculus. In particular:

• $\mathbf{NSK}$ is obtained from $\mathbf{NSS}\mathbf{4}$ by replacing ${\mathsf{ax}}_1$ with and ${\mathsf{ax}}_3$ with and substituting the rules with their variants in which the context $\mathrm{\Delta }\left\{\right\}$ is replaced with $\left[\right]$. For example, ${{◻}_{\wedge }}^{\bullet }$ is replaced by:

  

• $\mathbf{NST}$ is obtained by adding to $\mathbf{NSK}$ the initial sequent and a set of rules for in which the context $\left[\mathrm{\Sigma }\right]$ is replaced with the empty context. For example, we add the following rule:

  

• Finally, $\mathbf{NSK}\mathbf{4}$ is obtained by adding to $\mathbf{NSK}$ the initial sequent $\mathsf{a}{\mathsf{x}}_{\mathsf{1}}$ and the initial sequents . Furthermore, we modify the rules for by replacing the context $\left[\mathrm{\Sigma }\right]$ with . For example:

  

We now start the structural analysis of our calculi. As in the case of subintuitionistic systems, we write $\mathbf{NSX}$ to refer to the systems $\mathbf{NSK}\mathbf{,}\mathbf{NST}\mathbf{,}\mathbf{NSK}\mathbf{4}$.

Lemma 5.1

The rule:

is height-preserving admissible in $\mathbf{NSX}$ for $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{4}\right\}$.

Proof.

By induction on the height of the derivation of Γ. If Γ is an initial sequent, then so is $\left[\mathrm{\Gamma }\right]$. If Γ is the conclusion of a rule, we apply the induction hypothesis to each premise of the rule and then the rule again.

Lemma 5.2

The sequent is derivable for every formula A in $\mathbf{NSS}\mathbf{4}$ and in the systems $\mathbf{NSX}$.

Proof.

The proof is by induction on the degree of A.

Lemma 5.3

The rule $\mathsf{w}$ is height-preserving admissible in $\mathbf{NSS}\mathbf{4}$ and in the systems $\mathbf{NSK}\mathbf{,}\mathbf{NST}\mathbf{,}\mathbf{NSK}\mathbf{4}$.

Proof.

By straightforward induction on the height of the derivation.

A peculiar feature of decomposed modal systems is the fact that the input rules for formulas of the shape $\mathrm{◻p}$ can be shown to be admissible.

Lemma 5.4

The rule:

is height-preserving admissible in $\mathbf{NSS}\mathbf{4}$.

Proof.

The proof runs by induction on the height n of the derivation of . If n = 0, then is an initial sequent. Either $p^{\bullet }$ is active or not. If not, then the proof is trivial. Otherwise the sequent is of the shape . In this case is an instance of ${\mathsf{ax}}_3$. If n>0, we apply the induction hypothesis to the premise(s) of the last rule applied and then we apply the rule again.

We now state the analogous admissibility results for the systems $\mathbf{NST}$, $\mathbf{NSK}\mathbf{4}$, and $\mathbf{NSK}$. We avoid giving the details of the proofs as they are analogous to the one for $\mathbf{NSS}\mathbf{4}$.

Lemma 5.5

The rule:

is height-preserving admissible in $\mathbf{NSK}$.

Lemma 5.6

The rule:

is height-preserving admissible in $\mathbf{NSK}\mathbf{4}$.

Lemma 5.7

The rule:

is height-preserving admissible in $\mathbf{NST}$.

We now show that every rule is height-preserving invertible in the decomposable systems for modal logics.

Lemma 5.8

Every rule is height-preserving invertible in $\mathbf{NSX}$ for $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{S}\mathbf{4}\right\}$.

Proof.

We distinguish cases according to the rules.

• The modal rules which act on input formulas are height-preserving invertible by height-preserving admissibility of weakening.

• For every rule different from ${{◻}_{\mathrm{at}}}^{\circ }$, the proof follows by applying the induction hypothesis. For example, we consider the case of the modal rule ${◻}_{\vee }^{\circ }$ (the proof is the same for every system $\mathbf{NSX}$ for every $\mathbf{X}$). If is an initial sequent, then so is , because ${◻(A\vee B)}^{\circ }$ cannot be active in an initial sequent. If n>0 and ${◻(A\vee B)}^{\circ }$ is principal, the premise yields the desired conclusion. Otherwise, we apply the induction hypothesis to the premises of the rule applied and then the rule again. For example, if the last rule applied is ${\wedge }^{\bullet }$ we have:

  

• If the last rule applied is ${{◻}_{\mathrm{at}}}^{\circ }$, we would like to prove that whenever is derivable, then so is and the height is preserved. We argue by induction on the height n of the derivation of . We consider the case of $\mathbf{NSS}\mathbf{4}$, the other cases are analogous and we leave them to the reader. If n = 0, then is an initial sequent, then we distinguish cases. If ${\mathrm{◻p}}^{\circ }$ is not active, then the proof is trivial. If it is active, then the initial sequent is an instance of ${\mathsf{ax}}_1$ is of the shape . In this case is an instance of ${\mathsf{ax}}_3$. If is the conclusion of a rule, the proof follows applying the induction hypothesis to the premise(s) and then the rule again.

Lemma 5.9

The contraction rule is height-preserving admissible in $\mathbf{NSS}\mathbf{4}$ and $\mathbf{NSX}$.

Proof.

The proof follows the pattern detailed in Lemma 4.3.

Lemma 5.10

The rule $\mathsf{m}$ is height-preserving admissible in $\mathbf{NSX}$ with $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{S}\mathbf{4}\right\}$.

Proof.

See the proof of Lemma 4.6.

Lemma 5.11

The rules $\mathsf{4}$ and $\mathsf{t}$ are admissible in $\mathbf{NSS}\mathbf{4}$.

Proof.

The proof follows the structure of the one detailed for subintuitionistic systems. We refer the reader to Lemmas 4.9 and 4.12.

Lemma 5.12

The rule $\mathsf{wlw}$ is height-preserving admissible in $\mathbf{NSS}\mathbf{4}$ and in $\mathbf{NSK}\mathbf{4}$.

Proof.

We proceed as follows:

We now give a proof of the cut-elimination theorem for $\mathbf{NSS}\mathbf{4}$.

Theorem 5.13

The $\mathsf{cut}$ rule is admissible in $\mathbf{NSS}\mathbf{4}$.

Proof.

The proof is by double induction, with main induction hypothesis on the degree of the cut formula and secondary induction hypothesis on the height of the derivation of the premise . We distinguish cases according to the shape of the cut formula.

• If the cut formula is atomic, then the proof is immediate.

• If the cut formula is of the shape $A\wedge B,A\vee B$ or $A\to B$ we appeal to the invertibility of the corresponding connective to replace the cut with cuts on formulas of lesser degree.

• If the formula is $\mathrm{◻A}$ and ${\mathrm{◻A}}^{\bullet }$ is not principal in the last rule applied in , then we can permute the cut upwards and replace it with cuts of lesser height since all the right rules are invertible (see Theorem 4.13). We have:

  

  We proceed as follows:

  

  The cuts are removed by the secondary induction hypothesis.

• If the formula is $\mathrm{◻A}$ and it is principal we need to consider five subcases according to its shape. We limit ourselves to dealing with the ones in which $A\equiv \mathrm{◻p}$, $A\equiv ◻(B\to C)$ (the cases in which $A\equiv ◻(B\wedge C)$ or $A\equiv ◻(B\vee C)$ are analogous) and $A\equiv \mathrm{◻B}$.

  	–	If $A\equiv \mathrm{◻p}$, we have: We distinguish two subcases. Either is an initial sequent or not. If not, then ${\mathrm{◻p}}^{\bullet }$ is never principal and the cut can be permuted upwards. If it is an initial sequent, we assume that ${◻p}^{\bullet }$ is active (otherwise the reduction is trivial) and we distiguish cases. The premise is of the shape: or (either an instance of ${\mathsf{ax}}_{\mathsf{3}}$ or ${\mathsf{ax}}_{\mathsf{1}}$). In the second case we consider the other premise of the cut rule and the cut is eliminated as follows: The other case is analogous and so we omit the details.
  	–	If the cut formula is $◻(B\to C)$, we have: We first perform a cross-cut: The cut is removed by secondary induction hypothesis. A symmetric argument gives a derivation of . Finally, we construct the following derivation exploiting the invertibility lemma and usual cut reductions: The cuts are removed by primary induction hypothesis on the degree of the cut formula.
  	–	If the cut formula is $\mathrm{◻◻B}$, we have: We construct the following derivation: The topmost cut is removed by the secondary induction hypothesis, whereas the lowermost is removed by the primary induction hypothesis on the degree of the cut formula.

Next, we need to establish the cut-elimination theorem for the remaining systems.

Theorem 5.14

The cut rule is admissible in $\mathbf{NSK}\mathbf{,}\mathbf{NST}\mathbf{,}\mathbf{NSK}\mathbf{4}$.

Proof.

The proof follows the pattern detailed for $\mathbf{NSS}\mathbf{4}$. As in the (sub)intuitionistic case, the new cases arise when considering the initial sequents and the rules involving the intensional connective, which is the modal operator in this context.

• In the case of $\mathbf{NSK}$ we consider the case in which the cut formula is $\mathrm{◻p}$. If the premise is not an initial sequent, then we can permute the cut upwards and eliminate it by secondary induction hypothesis. If it is an initial sequent, we can assume that it is active in ${\mathsf{ax}}_{\mathsf{3}}^{\mathsf{k}}$, otherwise the reduction is trivial. Thus we have . We take the left premise of the cut, i.e. and we proceed as follows:

  

  In the cases in which the cut formula is $\mathrm{◻A}$ where A is a compound formula, we need to distinguish cases according to their shape. We limit ourselves to discussing one case, the remaining ones are similar.

  

  We apply the crosscuts to eliminate the repetition of the principal formula and then we conclude the reduction as follows:

  

  the other cases are similar and we avoid entering the details.

• In the case of $\mathbf{NST}$, we need to discuss the case in which the right premise of the cut is an initial sequent of the shape . We take the left premise of the cut: and we have:

  

  If the formula A is compound, then we have new possible cases arising from the $\mathsf{t}$-version of the rules, for example:

  

  We proceed as follows:

  

• The case of $\mathbf{NSK}\mathbf{4}$ is analogous and exploits the admissibility of the specific admissible rule $\mathsf{4}$, so we omit the details.

5.1. Soundness and completeness

In this subsection, we shall establish the soundness and completeness of the nested systems with respect to the semantics of the modal logics $\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{4}$ and $\mathbf{S}\mathbf{4}$. We recall the definition of the semantics and the axiomatizations of these systems (Chagrov & Zakharyaschev, 1997).

The axiomatic calculus $\mathbf{K}$ is obtained by adding to a propositional classic calculus the axiom schema $◻(A\to B)\to (\mathrm{◻A}\to \mathrm{◻B})$. The system $\mathbf{T}$ is obtained by adding to $\mathbf{K}$ the axiom schema $\mathrm{◻A}\to A$. The system $\mathbf{K}\mathbf{4}$ is obtained by adding to $\mathbf{K}$ the axiom $\mathrm{◻A}\to \mathrm{◻◻A}$. Finally, the calculus $\mathbf{S}\mathbf{4}$ is obtained by augmenting $\mathbf{K}$ with $\mathrm{◻A}\to A$ and $\mathrm{◻A}\to \mathrm{◻◻A}$. We briefly recall their semantic characterisation.

Definition 5.1

A modal frame is an ordered pair $\mathcal{F}=(W,⩽)$, where $W\ne \mathrm{\varnothing }$ and ≤ a binary relation on it.

Definition 5.2

A modal model is an ordered pair $\mathcal{M}=(\mathcal{F},v)$ where $\mathcal{F}$ is a modal frame and $v:\mathrm{AT}\to \mathcal{P}\left(W\right)$ is the valuation function.

Definition 5.3

Given a modal model $\mathcal{M}$, a world $x\in \mathcal{M}$, $A\in {\mathsf{FM}}^{◻}$, the satisfiability conditions for A are inductively defined:

• $x{\models }_{\mathcal{M}}p$ if and only if $x\in v\left(p\right)$.

• $x{⊭}_{\mathcal{M}}\mathrm{\perp }$.

• $x{\models }_{\mathcal{M}}B\wedge C$ if and only if $x{\models }_{\mathcal{M}}B$ and $x{\models }_{\mathcal{M}}C$.

• $x{\models }_{\mathcal{M}}B\vee C$ if and only if $x{\models }_{\mathcal{M}}B$ or $x{\models }_{\mathcal{M}}C$.

• $x{\models }_{\mathcal{M}}B\to C$ if and only if $x{⊭}_{\mathcal{M}}B$ or $x{\models }_{\mathcal{M}}C$.

• $x{\models }_{\mathcal{M}}\mathrm{◻B}$ if and only if for every y such that $x⩽y$, $y{\models }_{\mathcal{M}}B$.

Definition 5.4

$A\in {\mathsf{FM}}^{◻}$ is true in a model, in symbols ${\models }_{\mathcal{M}}A$, iff for every $x\in \mathcal{M}$, $x{\models }_{\mathcal{M}}A$.

Definition 5.5

$A\in \mathsf{FM}$ is a logical truth with respect to a class of modal frames $\mathcal{C}$, in symbols ${\models }_{\mathcal{C}}A$, iff for every model $\mathcal{M}$ whose frame is in $\mathcal{C}$, ${\models }_{\mathcal{M}}A$.

As it is well known, the system $\mathbf{K}$ is sound and complete w.r.t. the class of all modal Kripke frames; $\mathbf{T}$ is sound and complete w.r.t. the class of modal reflexive Kripke frames; $\mathbf{K}\mathbf{4}$ is sound and complete w.r.t. the class of modal transitive Kripke frames; $\mathbf{S}\mathbf{4}$ is sound and complete w.r.t. the class of modal reflexive and transitive Kripke frames (Chagrov & Zakharyaschev, 1997). To show the completeness of the modal calculi, it is enough to show that the axiomatic system can be embedded in the corresponding nested calculi.

To do so, we prove some preliminary lemmas showing the generalisation of the rules for the modal operators.

Lemma 5.15

The rule:

is admissible in $\mathbf{NSX}$ with $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{S}\mathbf{4}\right\}$.

Proof.

We argue by induction on the degree of A. If A is atomic, then the desired conclusion follows from the rule ${◻}_{\mathrm{at}}^{\circ }$. If A is a conjunction, disjunction or an implication we apply the invertibility of the corresponding rule and then the corresponding modal rule. For example, in the case in which A is of the shape $B\to C$, we assume that is derivable and we have:

If A is of the shape $\mathrm{◻B}$, the conclusion follows from an application of the rule ${◻}_{◻}^{\circ }$.

Lemma 5.16

The following statements hold:

1.	The sequent is provable in $\mathbf{NSX}$ for every $\mathbf{X}$.
2.	The sequent is provable in $\mathbf{NST}$ and in $\mathbf{NSS}\mathbf{4}$.
3.	The sequent is provable in $\mathbf{NSK}\mathbf{4}$ and in $\mathbf{NSS}\mathbf{4}$.
4.	The sequent is provable in $\mathbf{NSS}\mathbf{4}$.

Proof.

We discuss the items separately.

1. We argue by induction on the degree of the formula A. If A is atomic, then is an initial sequent. If A is of the shape $B\wedge C$, we argue as follows:

   

   The topmost sequents are derivable by Lemma 5.2. The cases in which A is a disjunction or an implication are analogous and thus we omit the details. If A is $\mathrm{◻B}$ the conclusion immediately follows by a root-first application of ${◻}_{◻}^{\bullet }$.

2. We argue by induction on the degree of the formula A. If A is atomic, then is an initial sequent. If A is a conjunction, a disjunction or an implication the proof is similar to the one detailed for item 1 and we omit the details. If it is of the shape $\mathrm{◻B}$, we have:

   

   The topmost sequents are derivable by Lemma 5.2.

3. We omit the details as the proof follows the pattern outlined for items 1. and 2.

4. Follows immediately from items 2. and 3.

The admissibility of $\mathsf{cut}$ and Lemma 5.16 gives the following result.

Lemma 5.17

The rules:

are admissible in $\mathbf{NSK}$ $\left({◻}_{\mathsf{k}}^{\bullet }\right)$, in $\mathbf{NST}$ $({◻}_{\mathsf{k}}^{\bullet }$ and ${◻}_{\mathsf{t}}^{\bullet })$, in $\mathbf{NSK}\mathbf{4}$ $({◻}_{\mathsf{k}}^{\bullet }$ and ${◻}_{\mathsf{4}}^{\bullet })$ and in $\mathbf{NSS}\mathbf{4}$ $({◻}_{\mathsf{k}}^{\bullet }$, ${◻}_{\mathsf{t}}^{\bullet }$, ${◻}_{\mathsf{4}}^{\bullet }$ and ${◻}^{\bullet })$.

Proof.

We discuss only the first case, the other ones being analogous.

The $\mathsf{cut}$ rule is admissible by Theorems 5.13 and 5.14. The rightmost sequent is derivable via Lemma 5.16.

Theorem 5.18

If $\mathbf{X}\in \{\mathbf{K},\mathbf{T}\mathbf{,}\mathbf{S}\mathbf{4},\mathbf{K}\mathbf{4}\}$ and $\mathbf{X}⊢A$, then $\mathbf{NSX}⊢A^{\circ }$.

Proof.

The proof is by induction on the height of the derivation in $\mathbf{X}$. If n = 0, then we need to check that the axioms are derivable.

• The classical axioms are derivable in $\mathbf{NSX}$ for every $\mathbf{X}$.

• Axiom $\mathbf{K}$ is derivable in $\mathbf{NSX}$ for every $\mathbf{X}$ using Lemmas 5.17 and 5.15.

  

  The topmost sequent is clearly provable.

• The axiom $\mathrm{◻A}\to A$ is derivable in $\mathbf{NST}$ and $\mathbf{NSS}\mathbf{4}$ as follows:

  

• The axiom $\mathrm{◻A}\to \mathrm{◻◻A}$ is derivable in $\mathbf{NSK}\mathbf{4}$ and $\mathbf{NSS}\mathbf{4}$. We omit the details (the proof is analogous to the one for the previous items).

If n>0, we show the admissibility of the rules of the axiomatic systems. Modus ponens can be simulated via $\mathsf{cut}$ (admissible by Theorems 5.13 and 5.14), whereas necessitation rests on Lemma 5.1.

Theorem 5.19

For every $\mathbf{X}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{4}\right\}$, if $\mathbf{NSX}$ is sound and complete with respect to Kripke semantics for $\mathbf{X}$.

Proof.

Soundness is easily established by induction on the height of the derivations. Completeness follows from the Theorem 5.18. Indeed, if A is valid w.r.t. to the Kripke semantics for system $\mathbf{X}$, then by completeness it is derivable in the axiomatic system $\mathbf{X}$ and so in $\mathbf{NSX}$.

6. Modalizing subintutionistic logics

We are now in the position to state and prove the embedding of intuitionistic logic and subintuitionistic logics into the modal logics $\mathbf{S}\mathbf{4}\mathbf{,}\mathbf{K}\mathbf{4}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}$ and to give a syntactic proof of the results. Compared to other proofs, our result has the following advantages:

• The proof follows from a trivial induction.

• The proof is completely syntactic.

• The height of the derivation is preserved in both directions with the exception of the case of Visser's logic.

We start by recalling the different translations.

Table

NSI	NSIK, NSIT, NSIK4	NSIB
$P^{\ast }=\mathrm{◻P}$	$P^{\ast }=P$	$P^{\ast }=\mathrm{◻P}\wedge P$
$(A\wedge B{)}^{\ast }=A^{\ast }\wedge B^{\ast }$	$(A\wedge B{)}^{\ast }=A^{\ast }\wedge B^{\ast }$	$(A\wedge B{)}^{\ast }=A^{\ast }\wedge B^{\ast }$
$(A\vee B{)}^{\ast }=A^{\ast }\vee B^{\ast }$	$(A\vee B{)}^{\ast }=A^{\ast }\vee B^{\ast }$	$(A\vee B{)}^{\ast }=A^{\ast }\vee B^{\ast }$
$(A\to B{)}^{\ast }=◻(A^{\ast }\to B^{\ast })$	$(A\to B{)}^{\ast }=◻(A^{\ast }\to B^{\ast })$	$(A\to B{)}^{\ast }=◻(A^{\ast }\to B^{\ast })$

In essence, it could be argued that the two calculi are strongly similar in the sense that there is a step to step correspondence in the translation.

Theorem 6.1

If $\mathbf{NSI}⊢\mathrm{\Gamma }$, then $\mathbf{NSS}\mathbf{4}⊢{\mathrm{\Gamma }}^{\ast }$ and the height is preserved.

Proof.

The proof is by induction on the height of the derivation. If Γ is an initial sequent in $\mathbf{NSI}$, then ${\mathrm{\Gamma }}^{\ast }$ is an initial sequent in $\mathbf{NSS}\mathbf{4}$. If n>0, the proof follows by applying the induction hypothesis and then the rule. For example, we have:

We transform the derivation as follows:

Theorem 6.2

If Γ is derivable in $\mathbf{NSS}\mathbf{4}$ and Γ contains only $\ast$-translated formulas and atomic formulas, then ${\mathrm{\Gamma }}^{\prime }$ is derivable in $\mathbf{NSI}$, where $(A^{\ast }{)}^{\mathrm{\prime }}=A$ and $p^{\prime }=p$.

Proof.

The proof is by induction on the height n of the derivation. If n = 0, then ${\mathrm{\Gamma }}^{\prime }$ is an initial sequent in $\mathbf{NSI}$. If n>0, the proof follows immediately by applying the induction hypothesis and then the corresponding rule in $\mathbf{NSI}$. For example,

is transformed into:

If the principal formula is ${\mathrm{◻p}}^{\circ }$, we have:

We proceed as follows:

The proof for the subintuitionistic systems different from $\mathbf{NSIB}$ is streamlined.

Theorem 6.3

$\mathbf{NSIY}⊢\mathrm{\Gamma }$ if and only if $\mathbf{NSY}⊢{\mathrm{\Gamma }}^{\ast }$ and the height is preserved, with $\mathbf{Y}\in \left\{\mathbf{K}\mathbf{,}\mathbf{T}\mathbf{,}\mathbf{K}\mathbf{4}\right\}$.

Proof.

The proof is by induction on the height of the derivation and follows the exact same pattern as the one detailed for $\mathbf{NSI}$. The proof is streamlined by the fact that atomic formulas are left unchanged by the translation.

A syntactic proof of these results has also been obtained in Negri (2021). However, our approach is different, inasmuch we make use of nested sequents, thereby avoiding a direct appeal to labelling and we also obtain a strengthening due to the peculiar formulation of the rules. In particular, the translations preserve the height of the derivations in both directions.

Theorem 6.4

If $\mathbf{NSIB}$ proves Γ, then $\mathbf{NSK}\mathbf{4}$ derives ${\mathrm{\Gamma }}^{\ast }$.

Proof.

The proof is by induction on the height of the derivation. We discuss the left to right direction. If Γ is an initial sequent, then it is of the shape . It is enough to observe that is derivable. If it is the conclusion of a rule, the proof consists in applying the induction hypothesis and then the rule again.

The other direction, namely the faithfulness of the embedding, is slightly more delicate and requires a strengthening of the induction hypothesis.

Theorem 6.5

Let Γ be a nested sequents containing only translated formulas, atomic formulas and formulas of the shape $\mathrm{◻p}$. If $\mathbf{NSK}\mathbf{4}$ proves Γ, then $\mathbf{NSIB}$ derives ${\mathrm{\Gamma }}^{\prime }$ which is thus defined: $(A^{\ast }{)}^{\prime }=A$, $(p{)}^{\prime }=p$ and $(\mathrm{◻p}{)}^{\prime }=p$.

Proof.

The proof is by induction on the height of the derivation. If Γ is an initial sequent, then ${\mathrm{\Gamma }}^{\prime }$ is an initial sequent too. To give a concrete example of this qualitative analysis, let us consider the case in which Γ is of the shape . It is immediate to observe that is an initial sequent in the system $\mathbf{NSIB}$. If Γ is the conclusion of an application of a rule, we distinguish cases. The general strategy consists once again of applying the induction hypothesis and then the rule in the subintuitionistic system. As an example, we discuss the case of the rule ${◻}_{{\to }_{\mathsf{b}}}^{\bullet }$:

We argue as follows:

7. Conservativity results

It is well-known that there are classes of formulas for which classical derivability is conservative over intuitionistic derivability. In essence, there are formulas for which we know that classical derivability entails intuitionistic derivability. A relevant example of this phenomenon is represented by geometric implications, i.e. formulas of the shape $A\to B$, where A and B do not contain universal quantifiers or implications (Negri, 2003). In the propositional case, a geometric formula can be conceived of as an implication in which the antecedent (succedent) is a finite conjunction (disjunction) of atomic formulas.

In this final section, we prove a strengthening of the usual conservativity results concerning classical derivability. We aim at showing that when considering propositional logic, to achieve conservativity we do not need to consider intuitionistic logic. Indeed, classical logic is conservative over a much weaker system, i.e. $\mathbf{NSIT}$. The first step to obtain the result consists in showing a reinforcement of the necessitation rule which is allowed to be applied inside a node of a nested sequent depending on the shape of the formulas.

Lemma 7.1

Let $A_1,\dots ,A_m$ be propositional geometric formulas.

Proof.

The proof is by induction on the height of the derivation in $\mathbf{NSIT}$. If $A_1^{\bullet },\dots ,A_m^{\bullet },p_1^{\bullet },\dots ,p_n^{\bullet },q_1^{\circ },\dots ,q_k^{\circ }$ is an initial sequent, then so is the desired conclusion. If it is not an initial sequent, then it has to be the conclusion of the rule ${{\to }_{\mathsf{t}}}^{\bullet }$. We have:

with $A_1^{\bullet }$ principal and $A_1^{\bullet }={r_1\wedge \dots \wedge r_u\to s_1\vee \dots \vee s_w}^{\bullet }$. We apply the height-preserving invertibility of the rules ${\wedge }^{\circ }$ and ${\vee }^{\bullet }$ to obtain derivations of:

1. $A_1^{\bullet },A_2^{\bullet },\dots ,A_m^{\bullet },p_1^{\bullet },\dots ,p_n^{\bullet },q_1^{\circ },\dots ,q_k^{\circ },{r_i}^{\circ }$, with $1\le i\le u$

2. $A_1^{\bullet },A_2^{\bullet },\dots ,A_m^{\bullet },p_1^{\bullet },\dots ,p_n^{\bullet },q_1^{\circ },\dots ,q_k^{\circ },{s_j}^{\bullet }$, with $1\le j\le w$

We then apply the induction hypothesis to each of these sequents to get:

• $A_1^{\bullet },A_2^{\bullet },\dots ,A_m^{\bullet },[p_1^{\bullet },\dots ,p_n^{\bullet },q_1^{\circ },\dots ,q_k^{\circ },{r_i}^{\circ }]$ with $1\le i\le u$

• $A_1^{\bullet },A_2^{\bullet },\dots ,A_m^{\bullet },[p_1^{\bullet },\dots ,p_n^{\bullet },q_1^{\circ },\dots ,q_k^{\circ },{s_j}^{\bullet }]$, with $1\le j\le w$

Applying the rules ${\wedge }^{\circ }$ and ${\vee }^{\bullet }$ we get:

• $A_1^{\bullet },A_2^{\bullet },\dots ,A_m^{\bullet },[p_1^{\bullet },\dots ,p_n^{\bullet },q_1^{\circ },\dots ,q_k^{\circ },{r_1\wedge \dots \wedge r_u}^{\circ }]$

• $A_1^{\bullet },A_2^{\bullet },\dots ,A_m^{\bullet },[p_1^{\bullet },\dots ,p_n^{\bullet },q_1^{\circ },\dots ,q_k^{\circ },{s_1\vee \dots \vee s_w}^{\bullet }]$

The desired conclusion: $A_1^{\bullet },A_2^{\bullet },\dots ,A_m^{\bullet },[p_1^{\bullet },\dots ,p_n^{\bullet },q_1^{\circ },\dots ,q_k^{\circ }]$now follows from an application of the rule ${{\to }_{\mathsf{k}}}^{\bullet }$.

We recall the presentation of classical logic $\mathbf{NSIC}$ with polarities in Figure 4.

Figure 4. The calculus $\mathbf{NSIC}$.

Theorem 7.2

Let ${\mathrm{\Gamma }}^{\bullet },A^{\circ }$ be a sequent containing only propositional geometric formulas. If ${\mathrm{\Gamma }}^{\bullet },A^{\circ }$ is derivable in $\mathbf{NSIC}$, then it is derivable in $\mathbf{NSIT}$ with the same height.

Proof.

The proof is by induction on the height of the derivation. If $\mathrm{\Gamma },A^{\circ }$ is an initial sequent in $\mathbf{NSIC}$, then so is in $\mathbf{NSIT}$. If the last rule applied is any rule different from ${\to }^{\circ }$, the conclusion follows from applying the induction hypothesis and, possibly, height-preserving admissibility of weakening in $\mathbf{NSIT}$. If the last rule applied is ${\to }^{\circ }$, we have:

By induction hypothesis we get the derivability of the sequent ${\mathrm{\Gamma }}^{\bullet },{p_1\wedge \dots \wedge p_m}^{\bullet },{q_1\vee \dots \vee q_n}^{\circ }$in $\mathbf{NSIT}$. Next, we construct the following derivation:

The above result shows that classical conservative results can be suitably sharpened showing that it is enough to consider significant weakenings of intuitionistic logic, such as the subintuitionistic logic whose modal companion is the modal logic $\mathbf{T}$. This is of peculiar interest insofar as it tells us something more. In particular, it shows that -- at least at a propositional level -- constructive reasoning is strongly connected to the acceptability of the modus ponens principle. Indeed, it is not hard to see that all the other subintuitionistic systems here considered fail to preserve derivability for geometric formulas (to witness this, consider the sequent ${p\to q}^{\bullet },p^{\bullet },q^{\circ }$ which is classically derivable, geometric, but not derivable in the remaining systems).

8. Concluding remarks

We have introduced nested sequent calculi for subintuitionistic logics and a variation of the usual calculi for modal logics. We have proposed a syntactic proof of the modal embedding of intuitionistic logic into the modal logic $\mathbf{S}\mathbf{4}$ and of subintuitionistic logics in their modal companions, obtaining a strengthening in terms of preservation of the height. Furthermore, we have investigated conservativity results of classical logic over the subintuitionistic logic whose modal companion is $\mathbf{T}$. We leave it as a theme for further research to identify conservativity classes for the other systems. The completeness theorem could be also obtained by extraction of a countermodel out of a failed proof search. Decidability results should also be easily obtainable showing the finiteness of the proof search procedures. Finally, the systems could be employed to explore further metalogical properties of the systems here considered such as the disjunction property.

Disclosure statement

No potential conflict of interest was reported by the author(s).

Additional information

Funding

This work was funded by the FWF project I 6372-N Logical methods for Deontic Explanations (LoDEx). FWF (Austrian Science Fund) Weave schema with Luxemburg and Germany; MSCA IEF Project REMODEL 101152658.

Notes

1 It is enough to consider only the height of the left premise as every right rule is invertible.