Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus^††thanks: The results published in this paper were obtained by the authors as part of the project granted by National Science Centre, grant no 2017/26/E/HS1/00127.

We now turn to the fragment of ISCI expressed in the language containing only $\bot,\supset,\equiv$. The intuitionistic negation $\neg\phi$ is omitted due to its definitional equivalence to $\phi\supset\bot$. The other connectives are not definable by $\supset,\bot$ in intuitionistic logic, but we omit them for simplicity.

Sequent calculi for SCI and ISCI presented in [3, 4] do not have the subformula property understood in the usual sense. In [4] this issue is discussed but no solution is presented. Here we analyse a property called extended subformula property. The idea behind it is that when constructing a derivation of a formula $\phi$ in a logic with non-Fregean identity we can use a formula $\psi$ built from subformulas of $\phi$, though $\psi$ is not itself a subformula of $\phi$. To warrant that the set of extended subformulas of $\phi$ is finite, we put a complexity constraint on the elements of the set. Formally:

We recall the Kripke semantics for ISCI proposed in [4].

An $\mathsf{ISCI}$ frame is simply an ordered pair $\mathbf{F}=\langle W,\leq\rangle$, where $W$ is a non-empty set and $\leq$ is a reflexive and transitive binary relation on $W$. If $\mathbf{F}=\langle W,\leq\rangle$ is an $\mathsf{ISCI}$ frame, then by assignment in $\mathbf{F}$ we mean a function:

Let us note that by (1), $v(\bot\equiv\bot,w)=1$, hence a special case of (2) is: if $v(\psi\equiv\phi,w)=1$, then $v((\psi\supset\bot)\equiv(\phi\supset\bot),w)=1$. Hence we can see that the notion of ISCI-admissible assignment captures axioms $(\equiv_{\_}1)$, $(\equiv_{\_}3)$ and $(\equiv_{\_}4)$. Axiom $(\equiv_{\_}2)$ will be incorporated into the notion of forcing.

The definition of forcing presented in [4] contains a mistake, which is the lack of clause (2) below; here we introduce the corrected version. For simplicity, we also generalize the monotonicity condition to formulas of arbitrary shape. (This is a negligible difference, however.)

In [4] it was proved that the axiomatic account of ISCI is both sound and complete with respect to the presented Kripke semantics.

Let $\mathcal{M}=\langle W,\leq,\Vdash\rangle$ be an arbitrary model. A sequent $\Gamma\Rightarrow\phi$ will be called true in $\mathcal{M}$, provided that: if all formulas in $\Gamma$ are true in $\mathcal{M}$, then so is $\phi$. A sequent is called ISCI-valid, or simply valid, if it is true in every model.

It is pretty clear that the intuitionistic component of $\mathsf{SC_{\_}{ISCI}}$ is correct with respect to the semantics of ISCI, hence we do not analyse the correctness of rules $L_{\_}\supset$ and $R_{\_}\supset$. We only briefly sketch the arguments that the identity rules of $\mathsf{SC_{\_}{ISCI}}$ preserve the validity of sequents.

1. $L_{\_}\equiv^{1}$

   Suppose that $\Gamma\Rightarrow\gamma$ is not true in a model $\mathcal{M}$. Then there is a world $w$ in $\mathcal{M}$ forcing each formula in $\Gamma$ but not $\gamma$. Since the relation of forcing is determined by some ISCI-admissible assignment $v$, and $v(\psi\equiv\psi)=1$ for each such assignment, also each world of $\mathcal{M}$ forces $\psi\equiv\psi$. Therefore $w\Vdash\psi\equiv\psi$, which shows that $\psi\equiv\psi,\Gamma\Rightarrow\gamma$ is not true in $\mathcal{M}$.

2. $L_{\_}\equiv^{2}$

   Suppose $\phi\equiv\chi,\Gamma\Rightarrow\gamma$ is not true in some $\mathcal{M}$. Then there is a world $w$ in $\mathcal{M}$ forcing formulas from $\Gamma$ and formula $\phi\equiv\chi$ and at the same time $w\not\Vdash\gamma$. By (4) in the definition of forcing $w\Vdash\phi\supset\chi$ and $w\Vdash\chi\supset\phi$. Hence it follows that $\phi\equiv\chi,\phi\supset\chi,\chi\supset\phi,\Gamma\Rightarrow\gamma$ is not true in $\mathcal{M}$.

The case of $L_{\_}\equiv^{3}$ is proved similarly, with reference to property (2) of an ISCI-admissible assignment. Correctness of the rules of $\mathsf{SC_{\_}{ISCI}}$, together with the fact that the axioms of $\mathsf{SC_{\_}{ISCI}}$ are valid, yields

As far as invertibility of the rules is concerned, it can be easily seen that the invertibility of the identity rules is warranted by the fact that the antecedents of the conclusions are subsets of the antecedents of the premises. Things are not that simple with the rules for implication. More specifically,

We assume that we start with a sequent of the form $\Rightarrow\phi$ and that $c(\phi)=n$.

We consider derivations constructed bottom-up, starting with the root. Rules are ‘applied’ in this direction to conclusions to obtain premises; we write ‘b-applied’ for ‘backwards-applied’, so we are not forced to language abuse. Our derivations are constructed under the following conditions:

1. (C1)

   axioms: no rules are b-applied to axioms,

2. (C2)

   repetitions-check and intuitionistic loop-check: no rules are b-applied to $\Gamma\Rightarrow\psi$, if the premise (at least one of the premises in the case of $L_{\_}\supset$) would be $\Gamma\Rightarrow\psi$ or any other sequent already present on the branch under construction,

3. (C3)

   saturation wrt equations: rules for identity are b-applied first, until all possible identities from $ex.sub(\phi)$ are constructed; only then the rules for implication are b-applied.

4. (C4)

   extended subformula: if a rule for identity is b-applied, then the active equation in the premise of the rule is an element of $ex.sub(\phi)$.

It also goes without saying that the rules are b-applied to sequents as long as it is possible to do so without violation of one of the mentioned conditions. A derivation constructed in line with (C1)–(C4) will be called restricted. Clause (C2) warrants that, e.g., if $L_{\_}\supset$ is b-applied, then none of the premises is a copy of the conclusion. Clause (C4) yields that restricted derivations satisfy the extended subformula property (recall Fact 1).

Before we move on, let us establish the following: for each formula $\phi$, set $ex.sub(\phi)$ is finite; hence the number of different sequents that may occur in any restricted derivation of $\Rightarrow\phi$ is finite. Since by clause (C2) there are no repetitions of sequents in a restricted derivation of $\Rightarrow\phi$, it follows that each such derivation is finite. But there is more to it. The same clause warrants that

Sketch of the proof-search procedure: starting with the root, the rules are b-applied maintaining the following priorities of rules: (i) identity rules, (ii) $R_{\_}\supset$, (iii) exactly one application of $L_{\_}\supset$. After (iii) we go back to (i). In point (iii), if there is more than one implication formula in the antecedent (which is usually the case), then there is a choice, and, obviously, one can make a wrong one. This is to be expected in a calculus for intuitionistic logic with a noninvertible rule. At this point backtracking must be employed: if a proof is not constructed, we must go back to the last choice of implication formula in (iii) and choose another one. An alternative form of employing backtracking seems to be by switching to a hypersequent format, where b-applications of $L_{\_}\supset$ would result in extending a hypersequent with all possible sequents that correspond to the possible choices of implication formula. We postpone this issue, however, for further research.

Suppose that the proof-procedure fails for $\Rightarrow\phi$. In order to build a contermodel for $\phi$ we will need a set of derivations, sometimes a large one. However, taking into account Fact 6, we may claim that our approach is constructive.

Worlds of the conuntermodel will be built from the occurrences of sequents and the values of formulas in the worlds will depend on their presence in antecedents/succedents of sequents. As is usually the case in such constructions, in order to obtain the desired effect the worlds need to be saturated and this can be assured only be suitable applications of the rules.

Here is an auxiliary notion. Suppose that a sequent $\Gamma\Rightarrow\gamma$ occurs on a branch of a restricted derivation. Let $\psi\supset\chi$ be an implication formula, not necessarily an element of $\Gamma$. If (i) $\chi\in\Gamma$, or (ii) $\psi=\gamma$, then we say that the sequent is saturated with respect to implication $\psi\supset\chi$.

Now we will give rule $L_{\_}\supset$ priority before rule $R_{\_}\supset$. More specifically, until the end of this section we expect that restricted derivations satisfy, in addition, the following

• (C5)

  if rule $R_{\_}\supset$ is b-applied to a sequent $\Gamma\Rightarrow\chi$ and there is $\gamma\supset\delta\in\Gamma$ (an implication formula in the antecedent), then either the sequent is saturated with respect to this implication, or there is a successor $S$ of this sequent on the given branch such that (i) there is no application of $R_{\_}\supset$ between $\Gamma\Rightarrow\chi$ and $S$, and (ii) $S$ is saturated with respect to $\gamma\supset\delta$.

By giving rule $L_{\_}\supset$ priority before $R_{\_}\supset$ we mean that if a sequent does not satisfy (C5), then before rule $R_{\_}\supset$ is applied, $L_{\_}\supset$ needs to be applied in order to saturate the sequent.

By assumption, a restricted derivation constructed in line with (C5) is still not a proof of $\Rightarrow\phi$ in $\mathsf{SC_{\_}{ISCI}}$, hence it has an open branch. We will be interested in the leftmost open one.

Let $\mathcal{D}_{\_}{\Rightarrow\phi}$ stand for a restricted derivation of sequent $\Rightarrow\phi$ satisfying (C5); by $\mathcal{B}_{\_}{\Rightarrow\phi}$ we shall refer to the leftmost open branch of $\mathcal{D}_{\_}{\Rightarrow\phi}$. Each such branch determines a structure as follows. Let $W_{\_}0$ stand for the set of all occurrences of sequents on $\mathcal{B}_{\_}{\Rightarrow\phi}$ (below we would say ‘sequent’ instead of ‘occurrence of a sequent’, but this should not lead to a confusion). Accessibility relation will be defined by the applications of $R_{\_}\supset$ and $L_{\_}\supset$, we start with some auxiliary notions. For all $S,S^{*}\in W_{\_}0$: we say that $S$ and $S^{*}$ are in relation $r$ iff (i) $S=S^{*}$, or (ii) $S$ is an immediate predecessor or immediate successor of $S^{*}$ on $\mathcal{B}_{\_}{\Rightarrow\phi}$, but $S/S^{*}$, respectively $S^{*}/S$, is not an instance of $R_{\_}\supset$. Let $\overline{r}$ stand for the transitive closure of $r$. Classes of abstraction of $\overline{r}$ will constitute points of our countermodel. Less formally, a class of abstraction of $\overline{r}$ contains all occurrences of sequents on $\mathcal{B}_{\_}{\Rightarrow\phi}$ between two applications of $R_{\_}\supset$.

We take $W=\{[S]_{\_}{\overline{r}}:S\in W_{\_}0\}$. For $w,y\in W$ we set:

• •

  $w\leq_{\_}0y$ iff for some $S\in w,S^{*}\in y$, $S^{*}/S$ is an instance of $R_{\_}\supset$ in $\mathcal{B}_{\_}{\Rightarrow\phi}$.

Let $\leq_{\_}W$ stand for the reflexive and transitive closure of $\leq_{\_}0$. We say that the structure $\langle W,\leq_{\_}W\rangle$ is determined by $\mathcal{B}_{\_}{\Rightarrow\phi}$ of $\mathcal{D}_{\_}{\Rightarrow\phi}$. Since there is no risk of a confusion, later on we will omit the relativisation to relation $\overline{r}$, and we will write $[S]$ instead of $[S]_{\_}{\overline{r}}$.

It can be easily seen that the above construction warrants that sequents considered within one class of abstraction of $\overline{r}$ ‘get saturated’ with respect to implication formulas in the antecedent. However, implications in the succedents of sequents cause a problem now, as we can have such sequents on the branch and no warranty that $R_{\_}\supset$ was applied: each time when rule $L_{\_}\supset$ is applied and the leftmost open branch goes through its left premise, the succedent of a sequent is altered. On the other hand, we still know that the sequents that occur on an open branch—in particular, those with implication formulas on the right side—are not provable in the calculus. In what follows we shall pick an appropriate open branch of a derivation of each such troublesome sequent. The branch will serve in the construction of additional points of our countermodel; ones that do not force the implications that occur in the succedents of sequents.

Let $\mathbb{S}$ stand for the set of all restricted derivations of $\Rightarrow\phi$ satisfying (C5) and all subderivations of these derivations. By Fact 6, $\mathbb{S}$ is finite. It follows that for each sequent, $S$, that occurs in a derivation in $\mathbb{S}$, $\mathbb{S}$ contains a restricted derivation, satisfying (C5), of this very sequent. We will denote such a derivation with $\mathcal{D}_{\_}S$ (it does not mean that the derivation is unique; if there is a choice—just pick one). By $\mathcal{B}_{\_}S$ we shall refer to the leftmost open branch of $\mathcal{D}_{\_}S$. What is more, for each sequent $S$ we define the structure $\langle W_{\_}S,\leq_{\_}S\rangle$ determined by $\mathcal{B}_{\_}S$ of $\mathcal{D}_{\_}S$, just as above. Instead of $\langle W_{\_}S,\leq_{\_}S\rangle$ we may use also $\langle W_{\_}{\mathcal{B}_{\_}S},\leq_{\_}{\mathcal{B}_{\_}S}\rangle$, or $\langle W_{\_}{\mathcal{B}},\leq_{\_}{\mathcal{B}}\rangle$ when the reference to a sequent $S$ is not important (the structure depends on the content of the whole branch, anyway).

We are almost in a position to supplement the initial structure $\langle W,\leq_{\_}W\rangle$ (determined by $\mathcal{B}_{\_}{\Rightarrow\phi}$) with worlds that do not force the troublesome implication formulas occurring in succedents of sequents. Before we continue, however, we need what follows.

Now we go back to the initial structure $\langle W,\leq_{\_}W\rangle$ determined by $\mathcal{B}_{\_}{\Rightarrow\phi}$. For each sequent of the form $\Gamma\Rightarrow\psi\supset\chi$ on $\mathcal{B}_{\_}{\Rightarrow\phi}$ we first define a maximum $\Gamma^{M}$ for the sequent in $W$:

which is, literally, the sum of all antecedents of sequents that were obtained on the branch going through $\Gamma\Rightarrow\psi\supset\chi$ between two applications of rule $R_{\_}\supset$. Due to Fact 1, we could have defined $\Gamma^{M}$ just as the maximal (wrt inclusion) antecedent in $[\Gamma\Rightarrow\psi\supset\chi]$, or as the least element wrt to the predecessor-successor relation induced by the rules. All accounts lead to the same effect. By Fact 7, sequent $\Gamma^{M}\Rightarrow\psi\supset\chi$ is not provable in $\mathsf{SC}_{\_}\mathsf{ISCI}$. It follows that neither is sequent $\Gamma^{M},\psi\Rightarrow\chi$ (for if it was, one application of $R_{\_}\supset$ would make the previous sentence false). Now we need a restricted derivation of $\Gamma^{M},\psi\Rightarrow\chi$ and the structure determined by its leftmost branch to supplement the constructed countermodel.

There is still one more subtle impediment to this construction, and it is the fact that—as we have established—there is no warranty that $R_{\_}\supset$ was b-applied here, which means that there is no warranty that sequent $\Gamma^{M},\psi\Rightarrow\chi$ is in $\mathbb{S}$. For this reason, in the final definitions below we refer to $\mathbb{B}$ instead of $\mathbb{S}$. $\mathbb{B}$ is a set of branches constructed as follows. Take $\{\mathcal{B}_{\_}{\Rightarrow\phi}\}$ and close this singleton set with the following rule: whenever the conclusion $\Gamma\Rightarrow\psi\supset\chi$ of rule $R_{\_}\supset$ occurs on a branch in $\mathbb{B}$, add to $\mathbb{B}$ the leftmost branch of a restricted derivation of sequent $\Gamma^{M},\psi\Rightarrow\chi$. Finally, let

Let $i,n\in\mathds{N}$. We set $\mathsf{Eq}^{i}=\{\psi\equiv\chi:c(\psi\equiv\chi)=i\}$ and $\mathsf{Form}^{n}_{\_}0=\mathsf{Prop}\cup\bigcup^{n}_{\_}{i=1}\mathsf{Eq}^{i}$. We define the assignment

by requiring that for each $w\in\overline{W}$, $v_{\_}0(\psi,w)=1$ iff (i) $\psi$ is of the form $\chi\equiv\chi$ or (ii) there is a sequent of the form ‘$\Gamma,\psi\Rightarrow\delta$’ in $w$. Next, we extend $v_{\_}0$ to a valuation $v:\mathsf{Form}_{\_}0\times\overline{W}\longrightarrow\{0,1\},$ as follows: $v(\psi\equiv\chi,w)=1$ iff (i) $\psi=\chi$ or (ii) $v_{\_}0(\psi\equiv\chi,w)=1$ or (iii) $\psi$ is of the form $\psi_{\_}1\otimes\psi_{\_}2$, $\chi$ is of the form $\chi_{\_}1\otimes\chi_{\_}2$ and $v(\psi_{\_}1\equiv\chi_{\_}1,w)=v(\psi_{\_}2\equiv\chi_{\_}2,w)=1$. It is easy to verify:

Let $\mathcal{M}=\langle\overline{W},\overline{\leq},\Vdash\rangle$ be an $\mathsf{ISCI}$-model with the forcing relation $\Vdash$ determined by assignment $v$.