Proof Theory for Positive Logic with Weak Negation

TL;DR

This paper develops proof-theoretic methods for positive logic with weak negation, establishing cut-free calculi, interpolation, and PSPACE-completeness of the systems.

Contribution

It introduces novel sequent calculi for positive logic with weak negation, proving properties like cut-elimination, interpolation, and complexity results.

Findings

Cut-free complete sequent calculi constructed

Systems satisfy Craig interpolation property

Logical systems are PSPACE-complete

Abstract

Proof-theoretic methods are developed for subsystems of Johansson's logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is proved, and used to conclude that the considered logical systems are PSPACE-complete.

Equations

$$(p\leftrightarrow q)\to (\neg p\leftrightarrow \neg q)\approx 1.$$

$$(p\wedge \neg p)\to \neg q\approx 1$$

$$(p\to q)\to (\neg q\to \neg p)\approx 1.$$

$$\mathsf{N}\subset \mathsf{NeF}\subset \mathsf{CoPC}\subset \mathsf{MPC},$$

$$p\mid \phi \wedge \phi \mid \phi \vee \phi \mid \phi \to \phi \mid \neg \phi$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},p\Rightarrow p&&\mathrm{\Gamma}\Rightarrow\top&\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma}\Rightarrow\alpha\to\beta\mathrm{\Gamma},\alpha\Rightarrow\beta&\mathrm{\Gamma},\alpha\to\beta\Rightarrow\varphi\mathrm{\Gamma},\alpha\to\beta\Rightarrow\alpha\qquad\mathrm{\Gamma},\beta\Rightarrow\varphi\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma}\Rightarrow\alpha\land\beta\mathrm{\Gamma}\Rightarrow\alpha\qquad\mathrm{\Gamma}\Rightarrow\beta\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\alpha\land\beta\Rightarrow\varphi\mathrm{\Gamma},\alpha,\beta\Rightarrow\varphi\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma}\Rightarrow\alpha\lor\beta\mathrm{\Gamma}\Rightarrow\alpha&\mathrm{\Gamma}\Rightarrow\alpha\lor\beta\mathrm{\Gamma}\Rightarrow\beta\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\alpha\lor\beta\Rightarrow\varphi\mathrm{\Gamma},\alpha\Rightarrow\varphi\qquad\mathrm{\Gamma},\beta\Rightarrow\varphi\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta\mathrm{\Gamma},\neg\alpha,\beta\Rightarrow\alpha\qquad\mathrm{\Gamma},\neg\alpha,\alpha\Rightarrow\beta\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta\mathrm{\Gamma},\neg\alpha\Rightarrow\alpha\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta\mathrm{\Gamma},\neg\alpha,\beta\Rightarrow\alpha&\mathrm{\Gamma}\Rightarrow\neg\alpha\mathrm{\Gamma},\alpha\Rightarrow\neg\alpha\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\alpha\Rightarrow\varphi\mathrm{\Gamma}\Rightarrow\varphi&\mathrm{\Gamma},\alpha\Rightarrow\varphi\mathrm{\Gamma},\alpha,\alpha\Rightarrow\varphi&\mathrm{\Gamma},\mathrm{\Delta}\Rightarrow\varphi\mathrm{\Gamma}\Rightarrow\alpha\quad\mathrm{\Delta},\alpha\Rightarrow\varphi\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\alpha\Rightarrow\varphi\mathrm{\Gamma}\Rightarrow\varphi\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\beta\Rightarrow\neg\gamma\mathrm{\Gamma},\neg\beta,\beta\Rightarrow\gamma\qquad\mathrm{\Gamma},\neg\beta,\gamma\Rightarrow\beta\end{array}$$

$$⊢\mathrm{\Gamma },\neg \beta ,\beta ,\alpha \Rightarrow \gamma \text{ and }⊢\mathrm{\Gamma },\neg \beta ,\gamma ,\alpha \Rightarrow \beta$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\beta\Rightarrow\neg\gamma\mathrm{\Gamma},\neg\beta\Rightarrow\beta\end{array}$$

$$⊢\mathrm{\Gamma },\neg \beta ,\alpha \Rightarrow \beta$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\beta\Rightarrow\neg\gamma\mathrm{\Gamma},\neg\beta,\gamma\Rightarrow\beta\end{array}$$

$$⊢\mathrm{\Gamma },\neg \beta ,\gamma ,\alpha \Rightarrow \beta$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma}\Rightarrow\neg\beta\mathrm{\Gamma},\beta\Rightarrow\neg\beta\end{array}$$

$$⊢\mathrm{\Gamma },\beta ,\alpha \Rightarrow \neg \beta$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\alpha\Rightarrow\varphi\mathrm{\Gamma},\alpha,\alpha\Rightarrow\varphi\end{array}$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\beta,\alpha,\alpha\Rightarrow\neg\gamma\mathrm{\Gamma},\neg\beta,\beta,\alpha,\alpha\Rightarrow\gamma\qquad\mathrm{\Gamma},\neg\beta,\gamma,\alpha,\alpha\Rightarrow\beta\end{array}$$

$$⊢\mathrm{\Gamma },\neg \beta ,\beta ,\alpha \Rightarrow \gamma \text{ and }⊢\mathrm{\Gamma },\neg \beta ,\gamma ,\alpha \Rightarrow \beta$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\alpha_{1},\neg\alpha_{1}\Rightarrow\neg\gamma\mathrm{\Gamma},\neg\alpha_{1},\neg\alpha_{1},\alpha_{1}\Rightarrow\gamma\qquad\mathrm{\Gamma},\neg\alpha_{1},\neg\alpha_{1},\gamma\Rightarrow\alpha_{1}\end{array}$$

$$⊢\mathrm{\Gamma },\neg {\alpha }_1,{\alpha }_1\Rightarrow \gamma \text{ and }⊢\mathrm{\Gamma },\neg {\alpha }_1,\gamma \Rightarrow {\alpha }_1$$

$$\begin{array}[]{ccccccccc}\mathrm{\Gamma},\neg\beta,\alpha,\alpha\Rightarrow\neg\gamma\mathrm{\Gamma},\neg\beta,\alpha,\alpha\Rightarrow\beta\end{array}$$

Full text

††journal: ArXiv

1 Introduction

Minimal propositional calculus (Minimalkalkül, denoted here as MPC) is the system obtained from the positive fragment of intuitionistic propositional calculus (equivalently, positive logic [27]) by adding a unary negation operator satisfying the so-called principle of contradiction (sometimes referred to as reductio ad absurdum, e.g., in [24]). This system was introduced in this form by Johansson in 1937 [21], and goes back to Kolmogorov’s first formalization of intuitionistic logic [22], obtained by discarding ex falso quodlibet (ex falso, from now on) from the nowadays standard axioms for intuitionistic logic. A letter from Johansson to Heyting (1935 - 1936) reads [32]:

[ex falso] says that once $\neg a$ has been proved, $b$ follows from $a$, even if this had not been the case before.

This implies that the constructive interpretation of negation (i.e., implication) characteristic of intuitionism may give rise to doubts concerning the legitimacy of ex falso as an axiom of intuitionistic logic. More generally, by rejecting ex falso, one earns the right to study the notion of contradiction on its own and thereby, the related notion of negation.

The axiomatization proposed by Johansson preserves the whole positive fragment and most of the negative fragment of Heyting’s intuitionistic logic. As a matter of fact, many important properties of negation provable in Heyting’s system remain provable (in some cases, in a slighlty weakened form) in minimal logic. The absence of ex falso made Johansson’s system the focus of interest in the field of paraconsistency, conceived as the study of those logics which admit inconsistent non-trivial theories. From a standard paraconsistent view, minimal logic still has unfortunate features [24]. In fact, the provability of what we are going to refer to as ‘negative ex falso’ $(a\land\neg a)\to\neg b$ makes negation meaningless in inconsistent theories—since every negated formula is provable—hence preserving some of the trivial aspects distinctive of ex falso. Interestingly enough, in the setting of positive logic, negative ex falso follows already from the assumption that negation is a functional antitone operator, i.e., that it satisfies the contraposition axiom $(a\to b)\to(\neg b\to\neg a)$ [7, 8]. The latter is a theorem of Johansson’s logic and one of its main ‘sources of explosiveness’111Logical systems in which all the inconsistent theories are trivial are sometimes said to be explosive [24]. The fact that negative ex falso is seen as a weak form of explosion justifies this statement.. The two formulas mentioned in this paragraph will play a fundamental rôle throughout the paper. These formulas arose as central principles in the semantic investigations of [7, 8]. There, the class of those logics is studied that extend a basic logic of a unary operator axiomatized by $(a\leftrightarrow b)\to(\neg a\leftrightarrow\neg b)$ over positive logic. The present paper can be seen as a continuation of the study of these logics in a proof-theoretic direction. It is worth mentioning that the system with contraposition as the only negation axiom (here, CoPC) has been considered as a theory of subminimal negation before: Hazen [14], following a personal communication with Humberstone, arrives at this logics by weakening Johansson’s original motivations, avoiding in particular the principle $(a\to\neg a)\to\neg a$. The same logic has also been discussed by Humberstone himself in [20, Section 8.33].222We thank Allen P. Hazen, and consequently Dick de Jongh, for pointing out and discussing this reference.

Working in a paraconsistent setting and with weaker notions of negation sounds appealing when dealing with phenomena such as descriptions of counterfactual situations or fictional objects, information in a computer data base, negations in natural language, etc. For instance, fragments of intuitionistic logic have been considered to formalize information flow or access control, mostly because of their good balance between expressivity and tractability. A relevant example in this direction can be found looking at the logic of infons [13], used in Distributed Knowledge Authorization Language (DKAL): ‘infons’ are statements viewed as containers of information, and infon logic turns out to be a conservative extension of the positive and disjunction-free fragment of intuitionistic logic with certain simple multiagent modalities.

A formal study of the properties of (constructive) negation taken individually has the potential of disclosing unexplored paths in the study of negation in these more applied contexts. In this respect, we would like to point out the possibility of exploiting these studies in the setting of inquisitive logic [12, 5, 6]. The propositional fragment of inquisitive logic can be regarded as the disjunctive-negative fragment of intuitionistic logic, and negation plays a fundamental rôle in inquisitive semantics. Nonetheless, having a univocal notion of negation does not make it easy to model the many different shades of negation within natural language. An attempt to extending the inquisitive logic framework by adding a ‘weak’ negation has been already pursued in [26], where to the persistent negation a weaker non-persistent negation is added, with the aim of taking care of problems as ‘might’-sentences or sentences expressing denial of conditionals.

This short introduction is meant to outline where the study of weak negations and, in particular, our work find their roots and motivations. The search for a ‘most appropriate’ or ‘significant’ notion of constructive negation given a fixed positive setting suggests a broad but well-defined realm of possibility, whose uniform study is typical of algebraic semantics. An algebraic presentation of the logical systems of our interest is the focus of Section 2. This section is a condensed presentation of the results of [7, 2], and earlier papers on which these articles are based. After this, the remaining and main part of the paper is concerned with the development of a proof theory for the relevant systems. While this proof-theoretic account lacks uniformity, the sequent calculi that we present happen to be the most natural ones, obtained via a straightforward translation of equations (or equivalently, Hilbert-style axioms) into sequent rules. First, cut-free Gentzen systems are presented in Section 3, and used in Section 4 to argue for fundamental results about the logical systems, such as Craig’s interpolation, disjunction property, decidability. Later, the non-termination issues affecting the Gentzen systems are solved by means of a loop-checking history mechanism, presented and justified in Section 5. The latter concludes the paper, as the termination property of the modified calculi allows us to improve the decidability result from Section 4 to an argument that the considered logical systems are decidable in PSPACE.

2 Preliminaries

In this preliminary section we introduce the setting and present the main technical tools that will be used throughout the paper.

An algebraic semantics for minimal logic is given by the variety of contrapositionally complemented lattices. A contrapositionally complemented lattice is an algebraic structure $\langle A,\land,\lor,\to,1,\neg\rangle$, where $\langle A,\land,\lor,\to,1\rangle$ is a relatively pseudo-complemented lattice333In the sense of [27]; alternatively called Brouwerian algebras (e.g., [1]) or lattices (e.g., [3]), generalized Heyting algebras (e.g., [10, 11]), implicative lattices (e.g., [24]). and the unary fundamental operation $\neg$ satisfies the identity $(p\to\neg q)\to(q\to\neg p)\approx 1$. A first algebraic account of Johansson’s logic can be found in Rasiowa’s main work on non-classical logics [27]. The variety presented by Rasiowa is term-equivalent to the variety of relatively pseudo-complemented lattices with a negation operator defined by the algebraic formulation of the principle of non-contradiction $(p\to q)\land(p\to\neg q)\to\neg p\approx 1$, originally employed in Johansson’s axiomatization. Observe that Heyting algebras can be seen as contrapositionally complemented lattices where $\neg 1$ is a distinguished bottom element [math].

As stated in the introduction, we focus on subsystems of minimal logic obtained by weakening Johansson’s notion of negation. Algebraically, we start from a class of algebraic structures $\langle A,\land,\lor,\to,1,\neg\rangle$ that generalize contrapositionally complemented lattices [27]. Again $\langle A,\land,\lor,\to,1\rangle$ is a relatively pseudo-complemented lattice and the unary operation $\neg$ is restricted only by the identity:

[TABLE]

We call these structures N-algebras, and we refer to the equivalent logical system as N. Note that this class of algebras play a fundamental rôle in the attempts of defining a connective over positive logic. In fact, the considered equation states that the function $\neg$ is a compatible function (or compatible connective), in the sense that every congruence of $\langle A,\land,\lor,\to,1\rangle$ is a congruence of $\langle A,\land,\lor,\to,1,\neg\rangle$. This is somehow considered a minimal requirement when introducing a new connective over a fixed setting. A study of compatible connectives on Heyting algebras can be found in [4], in the attempt of defining and studying new connectives over intuitionistic logic. In the setting of positive logic, a similar algebraic approach is carried out in [10].

Given the variety of N-algebras, we are particularly interested in two of its subvarieties that were implicitly considered in Section 1, and are defined, respectively, by the following identities:

[TABLE]

[TABLE]

Observe that 2.2 and 2.3 are algebraic formulations of, respectively, negative ex falso and the contraposition axiom, and for this reason we shall refer to the corresponding logics as negative ex falso logic (NeF) and contraposition logic (CoPC). Here, we also consider contrapositionally complemented lattices in terms of their term-equivalent variety of N-algebras defined by $(p\to q)\to(\neg q\to\neg p)\approx 1$ plus $(p\to\neg p)\to\neg p\approx 1$. It was proved in [7, 8, 2] that the following relations hold between the considered logical systems:

[TABLE]

where the strict inclusion ${\sf L}_{1}\subset{\sf L}_{2}$ means that every theorem of ${\sf L}_{1}$ is a theorem of ${\sf L}_{2}$, and at least one theorem of ${\sf L}_{2}$ is not provable in ${\sf L}_{1}$.

In the remainder of this paper we focus on a proof-theoretic study of (the logics corresponding to) these varieties. We will talk interchangeably about logical systems and their corresponding algebraic presentation, assuming an algebraic completeness result that goes beyond the scope of this paper and is therefore not included here. In order to keep the structure of the paper as clean as possible, the reader interested in a broader and introductory account of the topic from an algebraic perspective should refer to [7]. It is worth mentioning that in [7, 8], the presentation and the study of these logical systems are developed also in a Kripke-style semantical framework. Finally, [2] is concerned with a deeper algebraic account of these logics, and a first study of their modal companions.

3 Sequent Calculi

Following the notation of [31], we refer to the Gentzen systems introduced here as G3-systems. The letters $p,q,\ldots$ range over propositional variables, the Greek letters $\alpha,\beta,\ldots,\varphi,\ldots$ range over formulas, and $\mathrm{\Gamma},\mathrm{\Delta},\ldots$ range over finite multisets of formulas. We write $\mathrm{\Gamma},\mathrm{\Delta}$ for the multiset obtained as the union of $\mathrm{\Gamma}$ and $\mathrm{\Delta}$. We consider the propositional language $\mathcal{L}({\sf Prop})$, where ${\sf Prop}$ is a countable set of propositional variables, generated by the following grammar:

[TABLE]

where $p\in{\sf Prop}$. We consider $\top$ as a constant in the language, while we omit $\bot$. We call a formula positive if it contains only connectives from $\{\land,\lor,\to,\top\}$, and we refer to the positive fragment of intuitionistic logic as positive logic. We define the notion of weight (or complexity) $w(\varphi)$ of a formula $\varphi$ inductively as follows:

$w(p)=w(\top)=1$, for every atom $p$;

• 2.

$w(\varphi_{1}\circ\varphi_{2})=w(\varphi_{1})+w(\varphi_{2})+1$, where $\circ\in\{\land,\lor,\to\}$;

• 3.

$w(\neg\varphi)=w(\varphi)+1$.

In Figures 1 and 2, four different sequent systems are presented. Keeping the rules for the positive connectives and the structural rules fixed, the rule (n) defines a proof system for N-algebras; by adding the rule (nef) and by substituting the rule (n) with (copc), we obtain systems for the two proper subvarieties of N-algebras defined, respectively, by 2.2 and 2.3. Finally, by adding the rule (an) to the system obtained with (copc), we obtain a sequent proof system for contrapositionally complemented lattices.

Sequent proof systems for MPC were already introduced, e.g., in [31], using a different presentation of MPC. In fact, MPC is often formulated with the negation $\neg\varphi$ as a defined connective $\varphi\to f$, where $f$ is a distinguished propositional variable in the language. This formulation naturally suggests a sequent calculus for MPC  obtained by discarding the axiom ruling the constant $\bot$ from the system for intuitionistic propositional logic.

We call the height of a derivation $\vdash\mathrm{\Gamma}\Rightarrow\varphi$ the number of inference steps of a maximal branch within a proof tree with root $\mathrm{\Gamma}\Rightarrow\varphi$. A rule is said to be admissible if, whenever its premises are derivable in the system, so is the conclusion, and height-preserving admissible if, whenever its premises are derivable via a proof of height (at most) $n\in\mathbb{N}$, then so is the conclusion. We say that an inference rule is invertible if, for every instance of the rule, the premises are derivable if, and only if, the conclusion is, and height-preserving invertible if the two derivations have the same height. It can be proved that all the rules in Figure 1 except ($\lor$r1), ($\lor$r2), ($\to$l), (n), (nef) and (copc) are height-preserving invertible.

The arguments for admissibility of weakening (w) and contraction (c) are standard, and for the positive part of the calculus they can be adopted directly from a number of sources. Therefore we concentrate on the negative rules only, and refer the reader to the textbook [31] for the remaining cases. The full proofs can be found in [7].

Proposition 3.1**.**

The following weakening rule is height-preserving admissible:

[TABLE]

Proof.

The proof goes by induction on the height of a derivation of the premise sequent $\mathrm{\Gamma}\Rightarrow\varphi$.

Suppose that the derivation (of height $n$) ends with an application of (n)

[TABLE]

By the induction hypothesis twice, we have derivations

[TABLE]

of height, respectively, at most $m_{1}$ and at most $m_{2}$, where $m_{1}$ and $m_{2}$ are the height of derivations of the corresponding premises. By using (n), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\beta,\alpha\Rightarrow\neg\gamma$.

Suppose that the derivation ends with an application of (nef)

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

of height at most $n-1$. By using (nef), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\beta,\alpha\Rightarrow\neg\gamma$.

Suppose that the derivation ends with an application of (copc)

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

of height at most $n-1$. By using (copc), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\beta,\alpha\Rightarrow\neg\gamma$.

Finally, suppose that the derivation ends with an application of (an)

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

of height at most $n-1$. By using (an), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\alpha\Rightarrow\neg\beta$. ∎

Proposition 3.2**.**

The following contraction rule is height-preserving admissible:

[TABLE]

Proof.

The proof goes by induction (with respect to the lexicographic order) on the pair $(n,m)$, where $n=w(\alpha)$ and $m$ is the height of a derivation of $\mathrm{\Gamma},\alpha,\alpha\Rightarrow\varphi$.444The induction on the ordered pair is needed for the positive rules, e.g., the ($\land$l)-case with $\alpha$ principal (see [31]; cf. [7]).

Suppose that the derivation ends with an application of (n) where $\alpha$ is not a principal formula:

[TABLE]

By the induction hypothesis twice, we have derivations

[TABLE]

of height, respectively, at most $m_{1}$ and at most $m_{2}$, where $m_{1}$ and $m_{2}$ are the height of derivations of the corresponding premises. By using (n), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\beta,\alpha\Rightarrow\neg\gamma$.

Suppose that the derivation ends with an application of (n) where $\alpha$ is a principal formula $\neg\alpha_{1}$:

[TABLE]

By the induction hypothesis twice, we have derivations

[TABLE]

of height, respectively, at most $m_{1}$ and at most $m_{2}$, where $m_{1}$ and $m_{2}$ are the height of derivations of the corresponding premises. By using (n), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\alpha_{1}\Rightarrow\neg\gamma$.

Suppose that the derivation ends with an application of (nef) where $\alpha$ is not a principal formula:

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

of height at most $n-1$. By using (nef), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\beta,\alpha\Rightarrow\neg\gamma$.

Suppose that the derivation ends with an application of (nef) where $\alpha$ is a principal formula $\neg\alpha_{1}$:

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

of height at most $n-1$. By using (nef), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\alpha_{1}\Rightarrow\neg\gamma$.

Suppose that the derivation ends with an application of (copc) where $\alpha$ is not a principal formula:

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

of height at most $n-1$. By using (copc), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\beta,\alpha\Rightarrow\neg\gamma$.

Suppose that the derivation ends with an application of (copc) where $\alpha$ is a principal formula $\neg\alpha_{1}$:

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

of height at most $n-1$. By using (copc), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\neg\alpha_{1}\Rightarrow\neg\gamma$.

Finally, suppose that the derivation ends with an application of (an)

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

of height at most $n-1$. By using (an), we get a derivation of height at most $n$ of the sequent $\mathrm{\Gamma},\alpha\Rightarrow\neg\beta$. ∎

A reader used to dealing with the sequent calculus for intuitionistic logic won’t find it hard to believe the following fundamental result [7].

Theorem 3.1** (Soundness and Completeness).**

Given a finite multiset of formulas $\mathrm{\Gamma},\varphi$, the sequent $\mathrm{\Gamma}\Rightarrow\varphi$ is derivable in the G3-system if, and only if, $\bigwedge\mathrm{\Gamma}\to\varphi\approx 1$ is a valid equation in the corresponding variety of N-algebras.

4 Elimination of Cut

It is often said that finding the right (i.e., sound and complete) set of rules for a logical system requires a certain amount of ingenuity. In order to carry out proof search in the sequent system, and to use the calculus to understand the corresponding logic, we seek to eliminate the cut rule. The family of calculi presented in Section 3 is obtained by translating in the most natural way equations into sequent rules, and consists of ‘good’ systems, in the sense that they are cut-free. We don’t go into the details of the proof of cut admissibility, that are somehow standard and can be found in full in [7]. We will however outline the two interesting cases in the inductive proof—concerning the negative rules—and later focus on some relevant consequences ensuing from cut elimination.

Theorem 4.1**.**

The following cut rule is admissible:

[TABLE]

Proof.

The proof goes by induction (with respect to the lexicographic order) on the pair $(n,m)$, where $n=w(\alpha)$ and $m$ is the combined heights of derivations of the premises, i.e., if $\vdash_{m_{1}}\mathrm{\Gamma}\Rightarrow\alpha$ and $\vdash_{m_{2}}\mathrm{\Delta},\alpha\Rightarrow\varphi$, then $m=m_{1}+m_{2}$. We focus on the negative rules, and consider two cases: the case in which (only) the left premise is an axiom, and the case in which neither of the premises is an axiom and the formula $\alpha$ is principal in both of them. For the remainig cases, we refer to [31] and [7].

Consider the case in which the left premise is an axiom.

Suppose that the last step in the derivation of the right premise is (n):

[TABLE]

By the induction hypothesis twice, we have derivations

[TABLE]

and

[TABLE]

By using (n), we get a derivation of the sequent $\mathrm{\Gamma},\mathrm{\Delta},\neg\beta\Rightarrow\neg\gamma$.

Suppose that the last step in the derivation of the right premise is (nef):

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

By using (nef), we get a derivation of the sequent $\mathrm{\Gamma},\mathrm{\Delta},\neg\beta\Rightarrow\neg\gamma$.

Suppose that the derivation ends with an application of (copc):

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

By using (copc), we get a derivation of the sequent $\mathrm{\Gamma},\mathrm{\Delta},\neg\beta\Rightarrow\neg\gamma$.

Suppose that the last step in the derivation of the right premise is (an):

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

By using (an), we get a derivation of the sequent $\mathrm{\Gamma},\mathrm{\Delta}\Rightarrow\neg\beta$.

Consider the case in which neither of the premises is an axiom, and the formula $\alpha$ is principal in both of them. The left sequent comes as the conclusion of a negation rule if and only if the right premise sequent does.

Suppose that the last step in the derivation of both premises is (n):

[TABLE]

[TABLE]

By the induction hypothesis twice, we have derivations

[TABLE]

and

[TABLE]

Again, by the induction hypothesis twice, and the contraction rule, we get

[TABLE]

and

[TABLE]

Finally, by using (n), we get a derivation of the sequent $\mathrm{\Gamma},\mathrm{\Delta},\neg\beta\Rightarrow\neg\gamma$.

Suppose that the last step in the derivation of the left premise is (n), and the right premise comes from an application of (nef):

[TABLE]

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

But then, by the induction hypothesis, and the contraction rule, we get

[TABLE]

Finally, by using (nef), we get a derivation of the sequent $\mathrm{\Gamma},\mathrm{\Delta},\neg\beta\Rightarrow\neg\gamma$.

Suppose that the last step in the derivation of both premises is (copc):

[TABLE]

[TABLE]

By the induction hypothesis, we have a derivation

[TABLE]

By the induction hypothesis again, and the contraction rule, we also get

[TABLE]

Hence, by using (copc), we get a derivation of the sequent $\mathrm{\Gamma},\mathrm{\Delta},\neg\beta\Rightarrow\neg\gamma$.

Suppose the derivation of the left premise ends with an application of (an), and the right premise comes from an application of (copc):

[TABLE]

[TABLE]

By the induction hypothesis twice, we have derivations

[TABLE]

and

[TABLE]

By the induction hypothesis again, and the weakening rule, we also get

[TABLE]

But then, by using (an), we get a derivation of $\mathrm{\Gamma},\mathrm{\Delta}\Rightarrow\neg\gamma$.

The remaining cases go similarly, and are left to the reader—who can also find them in [7]. ∎

It is immediate to see that the calculi can be used to give an effective proof that, if the sequent $\mathrm{\Gamma}\Rightarrow\varphi\lor\psi$ can be proved via a derivation of height $n\in\mathbb{N}$, and $\mathrm{\Gamma}$ does not contain any disjunction, then (at least) one of the two sequents $\mathrm{\Gamma}\Rightarrow\varphi$ and $\mathrm{\Gamma}\Rightarrow\psi$ can be proved via a derivation of height at most $n$. The most striking consequence of cut elimination is the possibility of computable proof search, and hence, of providing a proof-theoretic decision method for the considered logics. As for complexity results, we cannot say much with the tools developed in the first part of the paper. In fact, proof search in the calculi presented in Figure 1 need not terminate, since we might encounter loops resulting in infinite branches.

Example 4.1**.**

Consider a proof-search procedure for the sequent $\neg\neg\neg p\Rightarrow\neg\neg p$ in the calculus for CoPC. The only possibility is to consider a backward application of (copc), obtaining the sequent $\neg\neg\neg p,\neg p\Rightarrow\neg\neg p$. At this point, considering a further backward application of (copc), with context $\neg p$, we get $\neg\neg\neg p,\neg p,\neg p\Rightarrow\neg\neg p$, and we can already see that the bottom-up proof-search procedure does not necessarily terminate.

Observe that sequents of the form $\mathrm{\Gamma},\varphi\Rightarrow\varphi$ can be proved to be derivable for every formula $\varphi$. By this and a straightforward induction on the height of a derivation, we can also prove that we can uniformly substitute formulas in derivable sequents obtaining derivable sequents. The following result reduces the number of negated formulas to be considered when dealing with any system containing the (copc) rule.

Proposition 4.1**.**

Let $n\in\mathbb{N}$ be an arbitrary natural number such that $n\geq 1$. Then, we have that $\neg^{(2n+1)}p\to\neg p\text{ and }\neg^{(2n)}p\leftrightarrow\neg\neg p$ are derivable via the rule (copc), where $\neg^{(m)}$ denotes $m$ nested applications of the negation operator for any natural number $m$.

Proof.

The proof goes by induction on $n\in\mathbb{N}$. The base case consists of presenting a derivation of the sequent $\Rightarrow\neg\neg\neg p\to\neg p$. After an application of ($\to$r), it is sufficient to apply to the obtained sequent $\neg\neg\neg p\Rightarrow\neg p$ the rule (copc) three times, with principal formulas respectively the pairs $(\neg\neg\neg p,\neg p)$, $(\neg\neg\neg p,\neg\neg p)$, and $(\neg p,\neg\neg p)$. This leads to the axiom:

[TABLE]

As for the induction step for $n>1$, by the induction hypothesis and the invertibility of ($\to$r), we have derivations of the sequents $\neg^{(2n-1)}p\Rightarrow\neg p$ and $\neg\neg\neg p\Rightarrow\neg p$. From $\neg^{(2n-1)}p\Rightarrow\neg p$, by using (w) and (copc),

[TABLE]

and hence, we get $\neg\neg p\to\neg^{(2n)}p$. Further, by (w) and (copc),

[TABLE]

But then, by (cut),

[TABLE]

to get $\neg^{(2n+1)}p\to\neg p$. Finally, by the induction hypothesis, the formula $\neg^{(2n-1)}p\to\neg p$ is a theorem. But then, by uniformly substituting $\neg q$ for $p$ in it, we obtain the desired $\neg^{(2n)}q\to\neg\neg q$. ∎

It is worth mentioning a further application of the calculi, whose details can be found in [7, 8]. If $\varphi$ is a formula in the language $\mathcal{L}({\sf Prop})$, the inductively defined $\sim$ operator that leaves the atoms unchanged, maps $\varphi\circ\psi$ to $(\varphi^{\sim}\circ\psi^{\sim})$ for $\circ\in\{\land,\lor,\to\}$, and $\neg\varphi$ to $(\varphi^{\sim}\to\neg\varphi^{\sim})$, soundly and truthfully translates MPC into the logic CoPC (and, even more, into the logic N).

We conclude this section with a remark. It can be seen by looking at the rules of the proof systems presented in Figure 1 that none of the theorems of the logics N, NeF, and CoPC is of the form $\neg\varphi$ (or, similarly, $\neg\varphi\lor\neg\psi$). In fact, there is no way to start the proof search for a sequent of the form $\Rightarrow\neg\varphi$, since the only rules for negation that can be applied require the left-hand side of the sequent to contain a negated formula.

4.1 Craig’s Interpolation

Craig’s interpolation theorem states that for each provable implication $\phi\to\psi$, there exists an interpolant $\sigma$ in the common language of $\psi$ and $\phi$, with both $\phi\to\sigma$ and $\sigma\to\psi$ being provable. Syntactic proofs of this result for intuitionistic logic go back to Schütte [29], and Maehara [23] (cf. [31]), and use the idea of splitting sequents in Gentzen’s calculus. We adopt the same method here, and prove the result by proof-theoretical means for the logics we consider in this paper, using the analytical calculi we have at hand.

By common language of two multisets of formulas $\mathrm{\Gamma}$ and $\mathrm{\Delta}$ we mean the set of propositional variables $\{p_{1},\ldots,p_{n}\}$ that appear both in (at least) a formula from $\mathrm{\Gamma}$ and in (at least) a formula from $\mathrm{\Delta}$. It is not necessary to require the common language to be non-empty. In fact, if this is the case, the interpolant is given by the constant $\top$ (or by a formula obtained from $\top$ via negations).

Theorem 4.2**.**

Let $\mathrm{\Gamma},\mathrm{\Delta}$ be finite multisets of formulas and let $\varphi$ be a formula such that the common language of $\mathrm{\Gamma}$ and $\mathrm{\Delta},\varphi$ is not empty. If $\vdash\mathrm{\Gamma},\mathrm{\Delta}\Rightarrow\varphi$, there exists a formula $\sigma$ such that:

the language of $\sigma$ is contained in the common language of $\mathrm{\Gamma}$ and $\mathrm{\Delta},\varphi$, 2. 2.

$\vdash\mathrm{\Gamma}\Rightarrow\sigma$* and $\vdash\mathrm{\Delta},\sigma\Rightarrow\varphi$.*

Proof.

The proof goes by induction on the height of a derivation $\vdash\mathrm{\Gamma},\mathrm{\Delta}\Rightarrow\varphi$, where the induction hypothesis states that an interpolant $\sigma$ exists for every possible splitting of the considered sequents. Given a sequent $\mathrm{\Gamma},\mathrm{\Delta}\Rightarrow\varphi$, we use $\mathrm{\Gamma}^{\prime}$ to denote a sub-multiset of $\mathrm{\Gamma}$ and $\mathrm{\Delta}^{\prime}$ for a sub-multiset of $\mathrm{\Delta}$. We focus on the negative rules, and for the positive ones we refer to [31].

Suppose that the derivation ends with an application of (n) of the form

[TABLE]

By the induction hypothesis twice, there exist $\sigma_{1}$ and $\sigma_{2}$ in the common language of $\mathrm{\Gamma}^{\prime},\neg\alpha$ and $\mathrm{\Delta},\beta$ such that the sequents

[TABLE]

are derivable. We are going to prove that the desired interpolant is of the form:

[TABLE]

First of all, observe that the considered formula is in the common language of $\mathrm{\Gamma}^{\prime},\neg\alpha$ and $\mathrm{\Delta},\beta$. It remains to find derivations of the sequents

[TABLE]

[TABLE]

By using (cut) and (c),

[TABLE]

But then, by ($\to$r), we get $\mathrm{\Gamma}^{\prime},\neg\alpha\Rightarrow\sigma_{2}\to\sigma_{1}$, and we weaken it to obtain a derivation of $\mathrm{\Gamma}^{\prime},\neg\alpha,\sigma_{1}\to\sigma_{2}\Rightarrow\sigma_{2}\to\sigma_{1}\,\,(*)$. Now, by using (w), ($\to$l) and the derivability of the sequent $\mathrm{\Gamma}^{\prime},\neg\alpha,\sigma_{1}\to\sigma_{2},\sigma_{1}\Rightarrow\sigma_{1}$, we obtain

[TABLE]

But then, by (w) and (n),

[TABLE]

From the latter and from $(*)$, by ($\land$r) and ($\to$r),

[TABLE]

At this point we start again and, by (cut), (c) and ($\to$r), we get

[TABLE]

Now, by (w), we obtain a derivation of

[TABLE]

We shall use the obtained sequent as the left premise of an application of ($\to$l), and hence, we look for a derivation of $\mathrm{\Delta},((\sigma_{2}\to\sigma_{1})\land\neg\sigma_{1})\Rightarrow\neg\beta$. By the induction hypothesis, we get the following derivations:

[TABLE]

[TABLE]

Suppose now that the derivation ends with an application of (n) of the form

[TABLE]

By the induction hypothesis twice, there exist $\sigma_{1}$ and $\sigma_{2}$ in the common language of $\mathrm{\Gamma}$ and $\mathrm{\Delta}^{\prime},\neg\alpha,\beta$ such that the sequents

[TABLE]

are derivable. By ($\land$r),

[TABLE]

Now, by (w), (n) and ($\land$l),

[TABLE]

But now, given that $\sigma_{1}\land\sigma_{2}$ is in the common language of $\mathrm{\Gamma}$ and $\mathrm{\Delta}^{\prime},\neg\alpha,\beta$, it is the desired interpolant.

Now, suppose that the derivation ends with an application of (nef) of the form

[TABLE]

By the induction hypothesis, there exists a formula $\sigma_{1}$ in the common language of $\mathrm{\Gamma}^{\prime},\neg\alpha$ and $\mathrm{\Delta}$ such that the sequents

[TABLE]

are derivable. By (w), (nef) and ($\to$l),

[TABLE]

But also, by (nef) and ($\to$r),

[TABLE]

Now it is sufficient to notice that the formula $\sigma_{1}\to\neg\sigma_{1}$ is in fact in the common language of $\mathrm{\Gamma}^{\prime},\neg\alpha$ and $\mathrm{\Delta}$ and hence, is the desired interpolant.

At this point, suppose that the derivation ends with an application of (nef) of the form

[TABLE]

By the induction hypothesis, there exists $\sigma_{1}$ in the common language of $\mathrm{\Gamma}$ and $\mathrm{\Delta}^{\prime},\neg\alpha$ such that the sequents

[TABLE]

are derivable. By a straightforward application of (nef), we get a derivation of $\mathrm{\Delta}^{\prime},\neg\alpha,\sigma_{1}\Rightarrow\neg\beta$, and we conclude that $\sigma_{1}$ is the desired interpolant.

Suppose that the derivation ends with an application of (copc) of the form

[TABLE]

By the induction hypothesis, there exists $\sigma_{1}$ in the common language of $\mathrm{\Gamma}^{\prime},\neg\alpha$ and $\mathrm{\Delta},\beta$ such that the sequents

[TABLE]

are derivable. By using (copc) on the first sequent, we get a derivation of $\mathrm{\Gamma}^{\prime},\neg\alpha\Rightarrow\neg\sigma_{1}$. Moreover, by (w) and (copc) we derive $\mathrm{\Delta},\neg\sigma_{1}\Rightarrow\neg\beta$.

Suppose now that the derivation ends with an application of (copc) of the form

[TABLE]

By the induction hypothesis, there exists $\sigma_{1}$ in the common language of $\mathrm{\Gamma}$ and $\mathrm{\Delta}^{\prime},\neg\alpha,\beta$ such that the sequents

[TABLE]

are derivable. By (copc), we get a derivation of $\mathrm{\Delta}^{\prime},\neg\alpha,\sigma_{1}\Rightarrow\neg\beta$. Hence, $\sigma_{1}$ is the desired interpolant.

Finally, suppose that the derivation ends with an application of (an)

[TABLE]

By the induction hypothesis, there is a formula $\sigma_{1}$ in the common language of $\mathrm{\Gamma}$ and $\mathrm{\Delta},\neg\alpha$ such that the sequents

[TABLE]

are derivable. By using (an) on the second sequent, we get a derivation of $\mathrm{\Delta},\sigma_{1}\Rightarrow\neg\alpha$ and hence, the desired interpolant is exactly $\sigma_{1}$. ∎

5 Terminating Systems

For the systems considered in the previous section, a naive backward proof search strategy is clearly not terminating (cf. Example 4.1). To obtain terminating systems, we adapt a history mechanism developed in [16] and [19]. We mention that the method employed here is obtained by modifying what in [19] is called ‘Swiss history’ (or ‘Bern Approach’). For further literature, see, e.g., [16, 15]. Another variant is given by the so-called ‘Scottish history’ (or ‘St. Andrews Approach’) [17, 18].

The original idea of preventing loops in a proof search using history mechanisms consists in adding a history to a sequent in order to store information about all the sequents that have occurred so far on a branch of a proof search tree. The method employed here is based on the assumption that storing goal formulas—given a sequent $\mathrm{\Gamma}\Rightarrow\varphi$, we refer to the formula $\varphi$ as the goal of the sequent—is sufficient to avoid possible loops.

We consider modifications of the $\mathbf{G3}$ sequent calculi presented in Section 3. We use $\mathbf{G3}^{\varphi}$ to denote the modification of the $\mathbf{G3}$ calculi obtained by considering the goals of the left rules to be restricted to atoms, negations or disjunctions. Here we call a left (respectively, right) rule an inference rule which introduces a principal formula on the left (respectively, right).

Further, we employ a history mechanism, and obtain the sequent calculi $\mathbf{G3}^{Hist}$ from Figures 3 and 4. The goal formula $\varphi$ in $\mathbf{G3}^{Hist}$ is again either an atom, a negation or a disjunction. Note that reading the $\mathbf{G3}^{Hist}$ rules bottom-up, the context is always non-decreasing; also, the left rules, the rule ($\to$r), and the rule (an) have side conditions for the context and/or for the history. The side conditions make sure that we empty the history set only if the context is properly extended. If this is not the case, we keep the history as it is and, if necessary, we enhance it with the new goal formula. If we meet a sequent whose goal is already in the history, then we know that we are dealing with a loop. Therefore, having a derivation of the sequent ${\mathcal{H}}\mid\mathrm{\Gamma}\Rightarrow\varphi$ in one of the $\mathbf{G3}^{Hist}$ systems amounts to saying that the proof tree of ${\mathcal{H}}\mid\mathrm{\Gamma}\Rightarrow\varphi$ does not contain sequents of the form ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}\Rightarrow\psi$ for every $\psi\in{\mathcal{H}}$. Note that the rule ($\land$l) in the terminating system is not purely $\mathbf{G3}$, but is a $\mathbf{G2}$-type rule with Kleene’s trick of building contraction in. We define the size of a proof tree as the number of nodes of the tree.

The first step towards a proof of the equivalence between $\mathbf{G3}$ and $\mathbf{G3}^{Hist}$ is the following.

Lemma 5.1**.**

The weakening rule is admissible in $\mathbf{G3}^{\varphi}$.

Proof.

Easy consequence of [19, Lemma 4.1] and of Proposition 3.1. ∎

The following result ensures that we can restrict ourselves to $\mathbf{G3}^{\varphi}$.

Lemma 5.2**.**

The sequent calculi $\mathbf{G3}$ and $\mathbf{G3}^{\varphi}$ are equivalent.

Proof.

It is trivial that if a sequent is provable in $\mathbf{G3}^{\varphi}$, then is provable in $\mathbf{G3}$. For the converse, the proof proceeds by induction on the height of a derivation.

Consider a $\mathbf{G3}$ inference which is not a $\mathbf{G3}^{\varphi}$ inference. This must be an instance of a left rule with an implicational or a conjunctive goal. By the induction hypothesis, we have $\mathbf{G3}^{\varphi}$ derivations of the premises. This implies the implicational or conjunctive goals to be principal formulas in the premises. Hence, the result follows from the proof of [19, Proposition 4.1]. ∎

Lemma 5.3**.**

The following contraction rule is admissible in $\mathbf{G3}^{Hist}$

[TABLE]

Proof.

By induction on the height of a derivation of the premise. We focus on the induction step, and on the non-intuitionistic rules.

Suppose that the last step in the derivation is an instance of (n1) of the form

[TABLE]

with $\beta\not\in\mathrm{\Gamma}\cup\{\neg\alpha\}$ and $\alpha\not\in\mathrm{\Gamma}$. By the induction hypothesis twice,

[TABLE]

But then, by (n1),

[TABLE]

Suppose that the last step in the derivation is an instance of (n2) of the form

[TABLE]

with $\beta\not\in\mathrm{\Gamma}\cup\{\neg\alpha\}$ and $\alpha\in\mathrm{\Gamma}$. By the induction hypothesis twice,

[TABLE]

But then, by (n2),

[TABLE]

Suppose the last step in the derivation to be an instance of (n3) as follows

[TABLE]

with $\beta\in\mathrm{\Gamma}\cup\{\neg\alpha\}$, $\neg\beta\not\in{\mathcal{H}}$ and $\alpha\not\in\mathrm{\Gamma}$. By the induction hypothesis twice, we get

[TABLE]

Hence, via an application of (n3),

[TABLE]

Suppose the last step in the derivation to be an instance of (n4) as follows

[TABLE]

with $\beta\in\mathrm{\Gamma}\cup\{\neg\alpha\}$, $\neg\beta\not\in{\mathcal{H}}$ and $\alpha\in\mathrm{\Gamma}$. By the induction hypothesis twice, we get

[TABLE]

Hence, via an application of (n4),

[TABLE]

Now, suppose that the last step in the derivation is an instance of (n1) of the form

[TABLE]

where $\beta\not\in\mathrm{\Gamma}\cup\{\alpha,\neg\gamma\}$ and $\gamma\not\in\mathrm{\Gamma}\cup\{\alpha\}$. By applying the induction hypothesis twice,

[TABLE]

Therefore,

[TABLE]

Now, suppose that the last step in the derivation is an instance of (n2) of the form

[TABLE]

where $\beta\not\in\mathrm{\Gamma}\cup\{\alpha,\neg\gamma\}$ and $\gamma\in\mathrm{\Gamma}\cup\{\alpha\}$. By applying the induction hypothesis twice,

[TABLE]

Therefore,

[TABLE]

Suppose now the last step in the derivation to be an instance of (n3),

[TABLE]

with $\beta\in\mathrm{\Gamma}\cup\{\alpha,\neg\gamma\}$, $\neg\beta\not\in{\mathcal{H}}$ and $\gamma\not\in\mathrm{\Gamma}\cup\{\alpha\}$. By the induction hypothesis twice, we get

[TABLE]

Hence, an application of (n3) leads to the desired conclusion. Suppose now the last step in the derivation to be an instance of (n4),

[TABLE]

with $\beta\in\mathrm{\Gamma}\cup\{\alpha,\neg\gamma\}$, $\neg\beta\not\in{\mathcal{H}}$ and $\gamma\in\mathrm{\Gamma}\cup\{\alpha\}$. By the induction hypothesis twice, we get

[TABLE]

Hence, an application of (n4) leads to the desired conclusion.

Suppose that the last step in the derivation is an application of (nef) of the form

[TABLE]

with $\neg\beta\not\in{\mathcal{H}}$. By the induction hypothesis,

[TABLE]

and hence, by (nef),

[TABLE]

Now, suppose that the last step in the derivation is an instance of (nef) as follows

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}$. Again, by the induction hypothesis,

[TABLE]

Hence, an appropriate application of (nef) gives us the desired result.

Suppose that the last step in the derivation is an instance of (copc1) of the form

[TABLE]

with $\beta\not\in\mathrm{\Gamma}\cup\{\neg\alpha\}$. By the induction hypothesis,

[TABLE]

But then,

[TABLE]

Suppose now that the last step in the derivation is an instance of (copc2) of the form

[TABLE]

with $\beta\in\mathrm{\Gamma}\cup\{\neg\alpha\}$ and $\neg\beta\not\in{\mathcal{H}}$. By the induction hypothesis,

[TABLE]

and hence, by (copc2), we can conclude

[TABLE]

Now suppose the last step in the derivation to be an instance of (copc1) of the form

[TABLE]

with $\beta\not\in\mathrm{\Gamma}\cup\{\alpha,\neg\gamma\}$. By the induction hypothesis, we get

[TABLE]

But then, we can conclude

[TABLE]

Now, suppose that the last step in the derivation is an instance of (copc2) of the form

[TABLE]

with $\beta\in\mathrm{\Gamma}\cup\{\alpha,\neg\gamma\}$ and $\neg\beta\not\in{\mathcal{H}}$. By the induction hypothesis,

[TABLE]

Hence, by (copc2),

[TABLE]

Finally, suppose the last step in the derivation to be an instance of (an) of the form

[TABLE]

where $\beta\not\in\mathrm{\Gamma}\cup\{\alpha\}$. By the induction hypothesis,

[TABLE]

Hence, by (an),

[TABLE]

∎

For the next result, we start from a $\mathbf{G3}^{\varphi}$ derivation of a sequent $\mathrm{\Gamma}\Rightarrow\varphi$, and construct a proof tree in $\mathbf{G3}^{Hist}$ for the corresponding sequent $\emptyset\mid\mathrm{\Gamma}\Rightarrow\varphi$. The proof trees that we are going to use are hybrid, in the sense that we deal with fragments of $\mathbf{G3}^{Hist}$ proof trees combined with $\mathbf{G3}^{\varphi}$ proof trees. Namely, every branch of the $\mathbf{G3}^{Hist}$ proof tree that do not have axiom leaves ends with a $\mathbf{G3}^{\varphi}$ proof tree. We work from the root up, and hence we focus on a uppermost history sequent ${\mathcal{H}}\mid\mathrm{\Gamma}\Rightarrow\varphi$ with non-history premises. More precisely, the argument below shows how the history mechanism allows us to detect and remove loops. The most interesting cases are the ones concerning rules with side conditions for the history. If the history side condition is not satisfied (i.e., $\varphi\in{\mathcal{H}}$), it means that we are dealing with a (non-trivial) loop: the same sequent ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}\Rightarrow\varphi$ already occurs previously in the proof tree (with ${\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$). This has the further consequence that the history has not been reset at any point in this fragment of the tree, because the context is stable (i.e., has not been properly extended). At this point, we know how to remove the loop, by removing the fragment of the tree from, but not including, the sequent ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}\Rightarrow\varphi$ up to and including ${\mathcal{H}}\mid\mathrm{\Gamma}\Rightarrow\varphi$.

Theorem 5.1**.**

The calculi $\mathbf{G3}$ and $\mathbf{G3}^{Hist}$ are equivalent. That is, a sequent $\mathrm{\Gamma}\Rightarrow\varphi$ is provable in $\mathbf{G3}$ if, and only if, the sequent $\emptyset\mid\mathrm{\Gamma}\Rightarrow\varphi$ is provable in $\mathbf{G3}^{Hist}$.

Proof.

From Lemma 5.2 it is enough to show that $\mathbf{G3}^{Hist}$ is equivalent to $\mathbf{G3}^{\varphi}$. It is immediate that any sequent provable in $\mathbf{G3}^{Hist}$ is also provable in $\mathbf{G3}^{\varphi}$, just by dropping the history and, if necessary, using some contractions. For the other direction, we enhance the proof of [19, Theorem 4.1] by adding arguments for the negation rules where needed.

Suppose that the last inference rule applied is ($\to$l). If the side conditions are satisfied, then we follow the proof in [19]. If not, we have

[TABLE]

The only tricky case is when $\varphi\in{\mathcal{H}}$. If the history condition is not met, we have to consider the additional cases in which $\varphi$ is $\neg\delta$.

Suppose that below the conclusion the hybrid tree has the form:

[TABLE]

where $\neg\delta\not\in{\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$ and $\mathrm{\Gamma}=\mathrm{\Gamma}^{\prime}\cup\{\neg\gamma\}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}^{\prime},\alpha\to\beta,\neg\gamma\Rightarrow\neg\delta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\alpha\to\beta\Rightarrow\neg\delta$. We can now apply backwards ($\to$l) to the first of these sequents (we may need some contractions).

Suppose that below the conclusion the hybrid tree has the form:

[TABLE]

where $\neg\delta\not\in{\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$ and $\mathrm{\Gamma}=\mathrm{\Gamma}^{\prime}\cup\{\neg\gamma\}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}^{\prime},\alpha\to\beta,\neg\gamma\Rightarrow\neg\delta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\alpha\to\beta\Rightarrow\neg\delta$. We can now apply backwards ($\to$l) to the first of these sequents (we may need some contractions).

Suppose now that the hybrid tree has the form:

[TABLE]

where $\neg\delta\not\in{\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$ and $\mathrm{\Gamma}=\mathrm{\Gamma}^{\prime}\cup\{\neg\gamma\}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}^{\prime},\alpha\to\beta,\neg\gamma\Rightarrow\neg\delta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\alpha\to\beta\Rightarrow\neg\delta$. We can now apply backwards ($\to$l) to the first of these sequents (we may need some contractions).

Finally, suppose that the hybrid tree has the following form:

[TABLE]

where $\neg\delta\not\in{\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$ and $\mathrm{\Gamma}=\mathrm{\Gamma}^{\prime}\cup\{\neg\gamma\}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}^{\prime},\alpha\to\beta,\neg\gamma\Rightarrow\neg\delta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\alpha\to\beta\Rightarrow\neg\delta$. We can now apply backwards ($\to$l) to the first of these sequents (we may need some contractions).

Suppose now that the last step in the derivation is an application of (n). If one among the side conditions of the history rules \textup{\sc(n{}{1})},\textup{\sc(n{}{2})},\textup{\sc(n{}{3})},\textup{\sc(n{}{4})} is satisfied, we simply add the appropriate history to the premises and possibly apply contraction. Otherwise, we have the following situation:

[TABLE]

with $\beta\in\mathrm{\Gamma}\cup\{\neg\alpha\}$ and $\neg\beta\in{\mathcal{H}}$. Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$, $\mathrm{\Gamma}=\mathrm{\Gamma}^{\prime}\cup\{\gamma\to\delta\}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}^{\prime},\gamma\to\delta,\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply backwards one between (n3) and (n4) to the first of these sequents, depending on which of the side conditions are satisfied (we may need some contractions).

Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}$ and ${\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply backwards (n3) to the first of these sequents (we may need some contractions).

Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}$ and ${\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply backwards (n4) to the first of these sequents (we may need some contractions).

Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}$ and ${\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply backwards one between (n3) and (n4) to the first of these sequents (we may need some contractions).

Suppose now that the last step in the derivation is an application of (nef). If the side condition of the history rule (nef) is satisfied, we simply add the appropriate history to the premises and possibly apply contraction. Otherwise, we have the following situation:

[TABLE]

with $\neg\beta\in{\mathcal{H}}$. Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$ and $\mathrm{\Gamma}=\mathrm{\Gamma}^{\prime}\cup\{\gamma\to\delta\}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}^{\prime},\gamma\to\delta,\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply backwards (nef) to the first of these sequents (we may need some contractions).

Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}$ and ${\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply backwards (nef) to the first of these sequents (we may need some contractions).

Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}$ and ${\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply backwards (nef) to the first of these sequents (we may need some contractions).

Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}$ and ${\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$. The new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply backwards (nef) to the first of these sequents (we may need some contractions).

Suppose now that the last inference rule is (copc). If the side condition of the history rule (copc1) is satisfied, we simply add the appropriate history to the premise. Else, we have

[TABLE]

where $\beta\in\mathrm{\Gamma}\cup\{\neg\alpha\}$. If $\neg\beta\not\in{\mathcal{H}}$, we simply apply (copc2) backwards and add the appropriate history (we may need an application of contraction). If $\neg\beta\in{\mathcal{H}}$, we need to consider two possibilities.

Suppose that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$ and $\mathrm{\Gamma}=\mathrm{\Gamma}^{\prime}\cup\{\gamma\to\delta\}$. Similarly to the previous case, the new hybrid tree is obtained by removing from the hybrid tree described above all the sequents from, and not including, ${\mathcal{H}}^{\prime}\mid\mathrm{\Gamma}^{\prime},\gamma\to\delta,\neg\alpha\Rightarrow\neg\beta$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can now apply (copc2) backwards to the first of these sequents (we may need some contractions).

Suppose now that below the conclusion the hybrid tree has the form

[TABLE]

where $\neg\beta\not\in{\mathcal{H}}^{\prime}$ and ${\mathcal{H}}^{\prime}\subseteq{\mathcal{H}}$. The new hybrid tree can be obtained now by removing from the old hybrid tree all the sequents from, and including, $(\neg\beta,{\mathcal{H}}^{\prime})\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\alpha$ up to, and including, ${\mathcal{H}}\mid\mathrm{\Gamma},\neg\alpha\Rightarrow\neg\beta$. We can again proceed with an application of (copc2) backwards to the first newly obtained sequent (we may need some contractions).

Finally, suppose that the last inference rule is (an). If the side condition of the history rule (an) is satisfied, we simply add the appropriate history to the premise. Otherwise, from the point of view of looping, both the premise and the conclusion are the same and we are in the presence of a trivial loop. The new hybrid tree is simply the old one with the premise obtained by contraction. ∎

Theorem 5.2**.**

Backwards proof search in the calculus $\mathbf{G3}^{Hist}$ is terminating.

Proof.

Consider the weight of a sequent defined as a triple

[TABLE]

of natural numbers, where $k$ is the number of subformulas of $\Gamma\cup\{\varphi\}$ computed as a set, $n$ is the number of formulas of $\Gamma$ computed as a set, $m$ is the number of formulas of ${\mathcal{H}}$, and $w$ is the weight of $\varphi$. It is easy to check that all the rules are such that the weight for the premises is lower than the one for the conclusion. ∎

We exploit now the termination property of our sequent calculus and establish a bound on the complexity of the decision problem for the considered logical systems.

Theorem 5.3**.**

There exists an algorithm for backwards proof search in the calculus $\mathbf{G3}^{Hist}$ that terminates in polynomial space.

Proof.

Given a formula $\varphi$, we want to search for a proof of the sequent $\emptyset\ |\ \emptyset\Rightarrow\varphi$. We use a standard argument, inspecting the proof-search tree. If the weight of $\varphi$ is $w$, the size of $\emptyset\ |\ \emptyset\Rightarrow\varphi$ is (at most) $(w,w,w)$, and decreases with every step of the search. Hence, it is enough to observe the following: the length of a branch in the proof-search tree is bounded by $w^{3}$; the branching degree of the tree is bounded by $2w$; the number of formulas contained in any sequent occurring during the search can be seen to be bounded by $O(w^{2})$. Therefore, the result follows. More precisely, as we in fact always need to remember just one whole branch, an upper bound of the needed space is $O(w^{5})$. ∎

Statman provides, in his seminal paper [30], a polynomial translation of intuitionistic logic into its implicational fragment. As IPC is PSPACE-hard, so is its implicational fragment (see also [28]). Therefore, any conservative extension of the implicational fragment of IPC is PSPACE-hard as well, including logics considered in this paper555It has been known before that MPC is PSPACE-complete, and we include it here for the sake of completeness. Statman’s polynomial translation from [30] can in fact be seen as one from IPC into MPC. Another polynomial translation of IPC into MPC, which makes use of the constant $f$, was found in a letter from Johansson to Heyting from 1935 [32] and is discussed in [8]. Note that MPC can be in turn translated into CoPC (see the remark after Proposition 4.2), but this translation is not polynomial.. To sum up:

Corollary 5.1**.**

The satisfiability problem for either one of the logical systems N, NeF, CoPC or MPC is PSPACE-complete.

Proof.

The inclusion in PSPACE is Theorem 5.3. Hardness follows from the fact that all the logics we consider are conservative extensions of the implication fragment of intuitionistic logic, known to be PSPACE-hard [30, 28]. ∎

6 Conclusions and Further Research

The question whether the logics addressed in this paper enjoy the property of uniform interpolation remains open. We conclude the article with some comments and remarks on this problem.

Uniform interpolation is a strengthening of the Craig interpolation property, claiming that for each formula $\phi(\vec{q},\vec{p})$ there exists a post-interpolant $\exists\vec{q}\phi(\vec{p})$ such that: (1) $\phi\to\exists\vec{q}\phi$ is provable, and (2) for each $\psi(\vec{p},\vec{r})$ with $\phi\to\psi$ provable, also $\exists\vec{q}\phi\to\psi$ is provable. Symmetrically, for each $\psi(\vec{p},\vec{r})$ there exists a pre-interpolant $\forall\vec{r}\psi(\vec{p})$ such that: (1) $\forall\vec{r}\psi\to\psi$ is provable, and (2) for each $\phi(\vec{q},\vec{p})$ with $\phi\to\psi$ provable, $\phi\to\forall\vec{r}\psi$ is provable as well. Note that here we deliberately confuse the existence of a post-interpolant and a pre-interpolant with the possibility of simulating propositional quantification. In terms of the Craig interpolation property, uniform interpolation means that there are a least ($\exists\vec{q}\phi$) and a greatest ($\forall\vec{r}\psi$) interpolant with respect to ‘provability order’, for each provable implication $\phi(\vec{q},\vec{p})\to\psi(\vec{p},\vec{r})$. The interpolants are unique up to provable equivalence.

Uniform interpolation for intuitionistic propositional logic has been originally proved by Pitts in [25], using proof-theoretical means. As for positive logic, the pre-interpolation property does not hold in full generality. Nevertheless, the ‘failing’ cases are of the following form. Given the formula $p\to r$, its pre-interpolant $\forall r(p\to r)$ in intuitionistic logic is equivalent to the formula $\neg p$, and there is no formula in the language of positive logic containing only $p$ that does the job: for every formula $\phi(p,q)$ in the positive language, $\phi(p,q)\to(p\to r)$ is not valid. This is a typical pathological case, and in all the other cases, the pre-interpolant exists. This result was proved in [9], where de Jongh and Zhao obtained uniform interpolation for positive logic, and for MPC (in the language with the constant $f$); the MPC uniform interpolant is obtained from the one of intuitionistic logic, by means of a clever construction of a positive content $\varphi^{+}$ associated to a formula $\varphi$.

We focus here on the possibility of proving uniform interpolation for the logic defined by the contraposition axiom. Also in this case, pre-interpolants do not always exist. In fact, the same example as in the case of positive logic does the job: if we consider again $\forall r(p\to r)$, no formula containing only the variable $p$ can work as an interpolant. Similarly to the MPC case, it is also true that $\phi(p,q)\to(p\to r)$ does not hold for any $\phi(p,q)$ in the language. One is therefore tempted to conjecture that the revised MPC version of uniform (pre-)interpolation could go through in this setting, and try to derive the uniform interpolation property for the logic CoPC (and possibly, for NeF) from that of MPC. However, some simple differences between the two cases are clear: for instance, observe that $\forall r(p\to\neg r)\leftrightarrow\neg p$ holds in MPC, while $\forall r(p\to\neg r)\leftrightarrow(p\to\neg p)$ holds only in the presence of the contraposition axiom, and moreover $p\to\neg p$ is the translation of the MPC interpolant by the $\sim$ translation: $(\neg p)^{\sim}=(p\to\neg p)$ (see the remark after Proposition 4.1). It would however be naive to hope that the uniform interpolants in the contraposition case can always be obtained by translation. In fact, a counterexample is given by the following observation: it is possible to construct a uniform pre-interpolant $\forall r(\neg p\wedge q\to\neg r)$ for the formula $(\neg p\wedge q\to\neg r)$ in the logic defined by the contraposition axiom, such interpolant being of the form $\neg p\to(q\to\neg q)$; however, the latter is not (equivalent to) the translation of the corresponding MPC interpolant $\neg p\to\neg q$.

We have not been able so far to prove or refute the uniform interpolation property for any of the logics N, NeF, and CoPC, and we leave it for further considerations, algebraic or proof-theoretic.