An ecumenical notion of entailment

Abstract

Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that sequent calculi are more amenable to extensive investigation using the tools of proof theory, such as cut-elimination and rule invertibility, hence allowing a full analysis of the notion of Ecumenical entailment. We then present some extensions of the Ecumenical sequent system and show that interesting systems arise when restricting such calculi to specific fragments. This approach of a unified system enabling both classical and intuitionistic features sheds some light not only on the logics themselves, but also on their semantical interpretations as well as on the proof theoretical properties that can arise from combining logical systems.

1 Introduction

In 1935 Gerhard Gentzen introduced sequent calculi for classical (${\textsf {LK}}$) and intuitionistic () first order logics [see Gentzen (1969) for the collected works] saying that this was “in order to be able to enunciate and prove the Hauptsatz in a convenient form”. Gentzen thought he had “to provide a logical calculus specially suited for this purpose”, because his favourite system, natural deduction (given by systems ${\textsf {NK}}$ and for classical and intuitionistic logics), could not be used to produce such a proof.¹ As he explains

“for although it [the natural deduction calculus] already contains the properties essential to the validity of the Hauptsatz, it does so only with respect to its intuitionistic form, in view of the fact that the law of excluded middle occupies a special position in relation to these properties”.

In the case of ${\textsf {LK}}$, Gentzen continues

“there exists complete symmetry between $\wedge$ and $\vee$, $\forall$ and $\exists$. All of the connectives $\wedge$, $\vee$, $\forall$, $\exists$ and $\lnot$ have, to a large extend, equal status in the system: no connective ranks notably above any other connective. The special position of the negation, in particular, which constituted a troublesome exception in the natural calculus [natural deduction], has been completely removed in a seemingly magical way. The manner in which this observation is expressed is undoubtedly justified since I myself was completely surprised by this property of the ‘${\textsf {LK}}$-calculus’ when first formulating that calculus. The ‘law of the excluded middle’ and the ‘elimination of double negation’ are implicit in the new inference schemata - the reader may convince himself of this by deriving both of them within the new calculus - but they have become completely harmless and no longer play the least special role in the consistency proof that follows”.

Thirty years later, Prawitz showed, in his doctoral work (Prawitz 1965), how to actually prove the Hauptsatz for natural deduction, both for intuitionistic and classical logics. Ever since, and ${\textsf {NK}}$, together with and ${\textsf {LK}}$, have been staples of proof theory. Nevertheless, every new wave of different proof systems (Schütte’s calculus, Display Calculi, Deep Inference, Nested systems, Labelled systems, etc) has improved our understanding of these basic systems. Regarding sequent systems, while in ${\textsf {LK}}$ and intuitionistic and classical behaviours are determined by a restriction on contexts, Maehara’s (Maehara 1954) is a multiple-conclusion intuitionistic sequent system with a context restriction only in the rules for right implication and right universal quantification. Interestingly, this distinction also appears when adding to sequents semantical information using labels as in Viganò (2000) and Dyckhoff and Negri (2012). On the other hand, in Fitting (2014) such labels were related with nestings and indexed tableaux, hence giving a semantical interpretation to nestings. And finally, in Pimentel (2018), we showed how the sequentialisation of nested systems transpose this interpretation back to , thus allowing a clearer view of sequent rules. With a totally different inspiration (using ideas from Girard’s linear logic and resource sensitivity), we have introduced ${\mathsf {FIL}}$—Full Intuitionistic Logic (de Paiva and Pereira 2005)—a multiple-conclusion sequent system provably equivalent to , where an indexing device allows us to keep track of dependency relations between formulae.

Common to all such systems is the need of different sets of rules and/or structures for capturing the intuitionistic behaviour. It is reasonable to ask if it is possible to naturally combine classical and intuitionistic systems, so that they can live peacefully in a single system. Citing Girard (1987)

“By the turn of this century the situation concerning logic was quite simple: there was basically one logic (classical logic) which could be used (by changing the set of proper axioms) in various situations. Logic was about pure reasoning. Brouwer’s criticism destroyed this dream of unity: classical logic was not suited for constructive features and therefore it lost its universality. Now by the end of the century we are faced with an incredible number of logics—some of them only named ‘logic’ by antiphrasis, some of them introduced on serious grounds. Is logic still about pure reasoning? In other words, could there be a way to reunify logical systems—let us say those systems with a good sequent calculus—into a single sequent calculus? Is it possible to handle the (legitimate) distinction classical/intuitionistic not through a change of system, but through a change of formulae? Is it possible to obtain classical effects by a restriction to classical formulae? ”

Several approaches have been proposed for combining intuitionistic and classical logics [see e.g. Liang and Miller (2011) and Dowek (2016)], many of them inspired by Girard’s polarised system ${\textsf {LU}}$ (Girard 1993). More recently, Prawitz chose a completely different approach by proposing a natural deduction system that we are calling the Ecumenical System (Prawitz 2015). While it also took into account meaning-theoretical considerations, it is more focused on investigating the philosophical significance of the fact that classical logic can be translated into intuitionistic logic.

We start this work by presenting a single-conclusion sequent calculus for the Ecumenical system, ${\mathsf {LEci}}$, given by a direct transformation from the natural deduction system. Using invertibility results, we show not only how to obtain a “purer” system ${\mathsf {LEci}}'$, with less introduction of negations on premises (when rules are read bottom-up), but also prove the main result of this paper:

Ecumenical entailments are intrinsically intuitionistic, but become classical for classical succedents.

Furthermore, from the standard Kripke interpretation for first-order intuitionistic logic, we present an Ecumenical nested system, where nestings correspond to worlds. Nested systems (Bull 1992; Kashima 1994; Brünnler 2009; Poggiolesi 2009) are extensions of the sequent framework where a single sequent is replaced with a tree of sequents. The logical rules then act on the nestings, possibly moving formulae from one nesting to another. This finer way of representing systems enables both locality and modularity by decomposing standard sequent rules into smaller components. Although we will not explore modularity in this work (since we will not extend the Ecumenical logic e.g. with modalities), we will use locality in order to relate ${\mathsf {LEci}}$ with ${\mathsf {mLEci}}$, a multiple-conclusion Ecumenical sequent system.

We finish this work by presenting the intuitionistic and classical fragments of ${\mathsf {mLEci}}$. It is interesting to note that, while the intuitionistic fragment is nothing else than Maehara’s , the classical fragment allows for a notion of goal directed proof search (Miller et al. 1991), where right formulae are totally decomposed before left rules are applied.

We then conclude by relating this work with some other ideas of “Ecumenical” entailments, and by presenting some future research directions.

Outline. The rest of the paper is organised as follows. In Sect. 2 we present Prawitz’ natural deduction system (NEci); the Ecumenical sequent system ${\mathsf {LEci}}$ is introduced in Sect. 3, and the cut-elimination property is proved; in Sect. 3.1 we show other proof-theoretical properties of ${\mathsf {LEci}}$, present a “purer” Ecumenical sequent system, and determine the Ecumenical concept of entailments; Sect. 4 brings the semantical interpretation of Ecumenical systems; in Sect. 5, we present a nested sequent system and a multiple-conclusion sequent system that are sound and complete with respect to the semantics presented in Sects. 4 and 6 shows non-hybrid fragments of Ecumenical systems and Sect. 7 concludes the paper.

2 Ecumenical natural deduction system

Dag Prawitz proposed a natural deduction system (Prawitz 2015) where classical and intuitionistic logic could coexist in peace. In this system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd, but they would each have their own existential quantifier, disjunction and implication, with different meanings. Prawitz’ main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. The surprising aspect of Prawitz’ system is its ability to share negations between the classical and the intuitionistic system, since many consider negation subject to the controversy between classical and intuitionistic logic, as implication is.

The language ${\mathcal {L}}$ used for Ecumenical systems is described as follows. Classical and intuitionistic n-ary predicate letters ($P_{c}^{n}, P_{i}^{n},\ldots$) co-exist in ${\mathcal {L}}$ but have different meanings. We will use a subscript c for the classical meaning and i for the intuitionistic, dropping such subscripts when formulae/connectives can have either meaning. The logical connectives $\{\bot ,\lnot ,\wedge ,\forall \}$ are common for classical and intuitionistic fragments, while $\{\rightarrow _i,\vee _i,\exists _i\}$ and $\{\rightarrow _c,\vee _c,\exists _c\}$ are restricted to intuitionistic and classical interpretations, respectively. In order to avoid clashes of variables we make use of a denumerable set $a, b,\ldots$ of special variables called parameters, which do not appear quantified.

In Fig. 1 we present ${\mathsf {NEci}}$, a natural deduction first-order Ecumenical system with the more modern sequent presentation. Sequents in ${\mathsf {NEci}}$ have the form $\varGamma \Rightarrow C$, with $\varGamma$ a set of Ecumenical formulae and C a formula. In the rules for quantifiers, the notation A[a / x] stands for the substitution of a for every (visible) instance of x in A. In the rules $\exists _i E,\forall I$, a is a fresh parameter, i.e. , it does not occur in $\varGamma ,A,B$.

Fig. 1

Ecumenical natural deduction system ${\mathsf {NEci}}$. In rules $\forall R$ and $\exists _i E$, the parameter a is fresh

The propositional fragment of the natural deduction Ecumenical system proposed by Prawitz has been proved normalising, sound and complete with respect to intuitionistic logic’s Kripke semantics in Pereira and Rodriguez (2017).

The rules for intuitionistic implication are the traditional ones, while the rules for classical implication make sure that $A\rightarrow _{c} B$ is treated as $\lnot A\vee _c B$, its classical rendering. The surprising facts are that (i) one can have a single constant for absurdity $\perp$ (instead of two, one intuitionistic and one classical, taking that absurd as the unit of disjunction, of which we have two variants) and (ii) that the intuitionistic and classical negations coincide. If negation was simply implication into false (as it is the case for intuitionistic negation) one might expect two negations, one intuitionistic and one classical. But the classical implication of the system is just a coding trick, it does not even satisfy modus ponens (see Sect. 3.1).

3 The system ${\mathsf {LEci}}$

The main difference between sequent and natural deduction systems is that, in the former, formulae in the antecedent and succedent of a sequent have the same status, being constructed top-down by introducing connectives; in the later, rules act only on the succedent of sequents, and elimination rules often produce simpler formulae, with less connectives. Hence, in order to transform a natural deduction calculus into a sequent one, it is necessary to reformulate the elimination rules so to introduce connectives for formulae in the left hand-side of sequents.

This reformulation is usually done either via direct translations, as in von Plato (2003), Englander et al. (2015) or via indirect translations, using cuts (see bellow). While direct translations have the advantage of not introducing extra steps that should later on be proved sound (via e.g. cut-elimination), the indirect ones are more natural and simpler, as we will illustrate here.

The sequent calculus ${\mathsf {cut}}$ rule expresses the fact that, if a formula A is used both as hypothesis and conclusion in two different sequents, these can be combined in a sequent without these occurrences of A

where $\varGamma _1,\varGamma _2$ are multisets of formulae.

As mentioned before, natural deduction introduction rules become sequent right rules. Hence, for example,

Now, since any natural deduction rule of the shape

can be interpreted as “A is an immediate consequence of $A_1,\ldots , A_n$”, every such a rule is equivalent to the primitive valid sequent $A_1,\ldots , A_n\Rightarrow A$. It turns out that left sequent rules can be formulated using these valid sequents and cuts (Troelstra and Schwichtenberg 1996; Negri and von Plato 2001). To illustrate the process, consider the following instance of a primitive sequent in ${\mathsf {NEci}}$: $A\vee _c B,\lnot A,\lnot B\Rightarrow \bot$. A sequent left rule for classical disjunction can be achieved as follows

Observe that the multiplicative nature of the cut rule forces a multiplicative version of the sequent rules, where contexts may split bottom-up. Hence, for guaranteeing completeness, the sequent system resulting from this process should have explicit left rules for weakening and contraction

where $\varGamma _1,\varGamma _2$ are non-empty multisets. In order to avoid that, we present, in Fig. 2, the weakening and contraction-free sequent calculus ${\mathsf {LEci}}$. Observe that all rules are additive, i.e. , with contexts copied bottom-up, e.g.

Following the same lines as in, e.g. Negri and von Plato (2001), it is easy to see that: (i) the additive and multiplicative versions of rules are equivalent; and (ii) rules $W_L$ and $C_L$ are (height-preserving—see Definition 3) admissible in ${\mathsf {LEci}}$.

Definition 1

Let ${\mathcal {S}}$ be a sequent system. An inference rule

is called admissible in ${\mathcal {S}}$ if S is derivable in ${\mathcal {S}}$ whenever $S_1,\ldots , S_n$ are derivable in ${\mathcal {S}}$.

Fig. 2

Ecumenical sequent system ${\mathsf {LEci}}$. In rules $\forall R$ and $\exists _i L$, the parameter a is fresh

Since cuts were introduced in the translation described above, it is essential to show that the cut rule does not introduce any extra power to the system, that is, that provability remains the same if we add to ${\mathsf {LEci}}$ the cut rule. This is known as the cut-elimination property.

In order to prove cut-elimination for ${\mathsf {LEci}}$, we use the following Ecumenical weight for formulae (Pereira and Rodriguez 2017).

Definition 2

The Ecumenical weight (${\mathsf {ew}}$) of a formula in ${\mathcal {L}}$ is recursively defined as

• ${\mathsf {ew}}(P^n_i)={\mathsf {ew}}(\bot )=0$;

• ${\mathsf {ew}}(A\star B)={\mathsf {ew}}(A)+{\mathsf {ew}}(B)+1$ if $\star \in \{\wedge ,\rightarrow _i,\vee _i,\exists _i,\forall \}$;

• ${\mathsf {ew}}(\lnot A)={\mathsf {ew}}(A)+1$;

• ${\mathsf {ew}}(A\circ B)={\mathsf {ew}}(A)+{\mathsf {ew}}(B)+4$ if $\circ \in \{\rightarrow _c,\vee _c\}$;

• ${\mathsf {ew}}(P^n_c)=4$;

• ${\mathsf {ew}}(\exists _c x.A)={\mathsf {ew}}(A)+4$.

Intuitively, the Ecumenical weight measures the amount of extra information needed (the negations added) in order to define the classical connectives from the intuitionistic ones (see Sects. 3.1 and 4).

The following are the usual definitions of height of derivations and cut-height.

Definition 3

The height of a derivation is the greatest number of successive applications of rules in it, where an axiom has height 0. The cut-height of an instance of the cut rule in a derivation is the sum of heights of the derivation of the two premises of ${\mathsf {cut}}$.

The admissibility of height-preserving weakening and contraction left rules in ${\mathsf {LEci}}$ allows for proving that ${\mathsf {LEci}}$ has the cut-elimination property.

Theorem 1

The rule ${\mathsf {cut}}$ is admissible in the system ${\mathsf {LEci}}$.

Proof

The proof is by the usual Gentzen method, using as inductive measure the pair (n, m), where n is the Ecumenical weight of the cut formula and m is the cut-height of the instance of ${\mathsf {cut}}$. The principal cases either eliminate the top-most cut or substitute it for cuts over formulae with smaller Ecumenical weight e.g.

Observe that, in the original cut, ${\mathsf {ew}}(A\rightarrow _c B)={\mathsf {ew}}(A)+{\mathsf {ew}}(B)+4$ while the other cuts have associated Ecumenical weights ${\mathsf {ew}}(A)$ and ${\mathsf {ew}}(B)+1$, hence being strictly smaller. For the classical existential case

Hence the Ecumenical weight on the cut formula passes from ${\mathsf {ew}}( \exists _c x.A)={\mathsf {ew}}(A)+4$ to ${\mathsf {ew}}(\forall x.\lnot A)={\mathsf {ew}}(A)+2$.

The non-principal cuts can be flipped up, generating cuts with smaller cut-height, e.g.

where $\pi _1^{\textit{w}}$ is the weakened version of $\pi _1$.

Note that applications of classical rules are restricted to having a $\perp$ in the succedent, hence they allow for more strict applications of the cut rule. In fact, if the cut-formula in the right premise is classical and principal, then C should be $\bot$, since conclusion sequents in all classical left rules have $\bot$ as the succedent. $\square$

The equivalence between additive and multiplicative rules as well as the cut-elimination result entails the equivalence between sequent and natural deduction systems.

Corollary 1

The systems ${\mathsf {NEci}}$ and ${\mathsf {LEci}}$ are equivalent.

Finally, a word about the design of the system ${\mathsf {LEci}}$. The reason for defining antecedents of sequents as multisets is that implementations using sets may generate loops on proof search. The price to pay for having an intuitionistic, contraction-free sequent system is the copy (when seen bottom-up) of the implication formula into the left premise in the rules $\rightarrow _c L,\rightarrow _i L$ and $\lnot L$, in order to guarantee completeness (try proving the theorem $\lnot \lnot (A\vee _i\lnot A)$). This also may cause loops on implementations, which could be easily avoided e.g. using the techniques in Dyckhoff (1992). Since loop checking can also be avoided with clever implementations (for example by shuffling contexts), we prefer to use the rules as proposed here for simplicity.

3.1 About provability, proofs and proof systems

Denoting by $\vdash _{{\mathsf {S}}} A$ the fact that the formula A is a theorem in the proof system ${\mathsf {S}}$, the following theorems are easily provable in ${\mathsf {LEci}}$.

• 1. $\vdash _{{\mathsf {LEci}}} (A \rightarrow _i B) \rightarrow _i (A \rightarrow _c B)$.

• 2. $\vdash _{{\mathsf {LEci}}} (A \vee _c B) \leftrightarrow _i \lnot (\lnot A \wedge \lnot B)$

• 3. $\vdash _{{\mathsf {LEci}}} (A \rightarrow _c B) \leftrightarrow _i \lnot (A \wedge \lnot B)$.

• 4. $\vdash _{{\mathsf {LEci}}} (\exists _cx.A) \leftrightarrow _i \lnot (\forall x.\lnot A)$.

These theorems are of interest since they relate the classical and the intuitionistic operators. In particular, observe that the intuitionistic implication implies the classical one, but not the converse, that is, $\not \vdash _{{\mathsf {LEci}}} (A \rightarrow _c B) \rightarrow _i (A \rightarrow _i B) \text{ in } \text{ general }$. Moreover, the classical connectives can be defined using negation, conjunction and the universal quantifier. This will be heavily exploited in the semantic definition of Ecumenical systems (see Sect. 4).

Note also that $\vdash _{{\mathsf {LEci}}} (A \rightarrow _c \bot ) \leftrightarrow _i (A \rightarrow _i \bot ) \leftrightarrow _i (\lnot A)$ which means that the Ecumenical system defined in Fig. 2 does not distinguish between intuitionistic or classical negations, thus they can be called simply $\lnot A$. We prefer to keep the negation operator in the language since the calculi presented in this work make heavy use of it.

On the other hand,

• i. $\vdash _{{\mathsf {LEci}}} A\vee _c\lnot A$ but $\not \vdash _{{\mathsf {LEci}}} A\vee _i\lnot A$

• ii. $\vdash _{{\mathsf {LEci}}} (\lnot \lnot A) \rightarrow _c A$ but $\not \vdash _{{\mathsf {LEci}}} (\lnot \lnot A) \rightarrow _i A$

• iii. $\vdash _{{\mathsf {LEci}}} (A\wedge (A \rightarrow _i B)) \rightarrow _i B$

• iv. $\not \vdash _{{\mathsf {LEci}}} (A\wedge (A \rightarrow _c B)) \rightarrow _i B$ in general.

• v. $\varGamma \Rightarrow B$ is provable in ${\mathsf {LEci}}$ iff $\vdash _{{\mathsf {LEci}}} \bigwedge \varGamma \rightarrow _i B$

Observe that (iii.) means that modus ponens is intuitionistically valid, while (iv.) implies that classical modus ponens is not intuitionistically valid, in general. But maybe more importantly, (v.) means that

Fact 1

Validity of a sequent in any semantical interpretation of ${\mathsf {LEci}}$ should correspond to provability of the corresponding intuitionistic implicational formula.

This not only corroborates the results in Avigad (2001) and Pereira and Rodriguez (2017) (see next section), but it shows a very interesting perspective on Ecumenical entailment: it is intuitionistic!

That is, even though some formulae carry with them the notion of classical truth, the logical consequence is intrinsically intuitionist. As it should be, since the ecumentical system embeds the classical behaviour into intuitionistic logic.

Moreover, observe that Fact 1 also implies that the rule $\rightarrow _iR$ is invertible.

Definition 4

Let ${\mathcal {S}}$ be a sequent system. An inference rule with premises $S_1,\ldots , S_n$ and conclusion S is called invertible in ${\mathcal {S}}$ if the rules $\frac{S}{S_1}, \ldots , \frac{S}{S_n}$ are admissible in ${\mathcal {S}}$.

Proposition 1

The only invertible rules in ${\mathsf {LEci}}$ are: $\rightarrow _iR,\rightarrow _cR,\wedge R,\wedge L,\lnot R, \vee _iL, \vee _cR,$ $\exists _cR, \exists _i L,\forall R,\forall L,R_c$.

Proof

Proving invertibility requires induction on the height of derivations, where all the possible rule applications have to be considered. For example, to prove that $\rightarrow _i R$ is invertible, the goal is to show that $\varGamma ,A\Rightarrow B$ is derivable whenever $\varGamma \Rightarrow A\rightarrow _i B$ is derivable. The result follows by a case analysis on the shape of the derivation of $\varGamma \Rightarrow A\rightarrow _i B$. Consider, e.g. , the case when $\varGamma =C\wedge D,\varGamma '$ and the last rule applied is $\wedge L$, i.e., consider the following derivation

By the inductive hypothesis, $C, D,\varGamma ',A\vdash B$ is derivable and the following holds:

as wanted. On the other hand, e.g. , $\vee _cL$ is not invertible: if $P^n_i,Q^m_i$ are different atomic propositions, the sequent $P^n_i,Q^m_i\vee _cQ^m_i\Rightarrow P^n_i$ is trivially provable, but $P^n_i,Q^m_i\Rightarrow \bot$ is not provable. $\square$

Since invertibility of rules implies that they can be eagerly applied, i.e. , they can be applied at any time without losing the provability, this result allows for a proposal of a better Ecumenical sequent system from a proof theoretical point of view. Figure 3 presents the rules of the system ${\mathsf {LEci}}'$ that differ from ${\mathsf {LEci}}$. In particular, observe that the left rules for the classical connectives in ${\mathsf {LEci}}'$ are particular instances of their intuitionistic versions, where the consequent must be $\perp$. In the sense that ${\mathsf {LEci}}'$ introduces (bottom-up) less negations, one could say that it is “purer” than ${\mathsf {LEci}}$.

Fig. 3

Some rules for the Ecumenical sequent calculus system ${\mathsf {LEci}}'$. In $\exists _c L$, the parameter a is fresh

To preserve the “classical behaviour”, i.e. , to satisfy all the principles of classical logic e.g. modus ponens and the classical reductio, it is sufficient that the main operator of the formula be classical (Pereira and Rodriguez 2017). Thus, “hybrid” formulae, i.e. , formulae that contain classical and intuitionistic operators may have a classical behaviour. Formally,

Definition 5

A formula B is called externally classical (denoted by $B^{c}$) if and only if B is a classical constant or its main operator is classical (that is: $\rightarrow _c,\vee _c,\exists _c$). A formula C is classical if it is built from classical atomic predicates using only the connectives: $\rightarrow _c,\vee _c,\exists _c,\lnot , \wedge ,\forall$ and the unit $\bot$.

For externally classical formulae we can now prove the following theorems

• 1. $\vdash _{{\mathsf {LEci}}} (A \rightarrow _c B^{c}) \rightarrow _i (A \rightarrow _i B^{c})$

• 2. $\vdash _{{\mathsf {LEci}}} (A\wedge (A \rightarrow _c B^{c})) \rightarrow _i B^{c}$

• 3. $\vdash _{{\mathsf {LEci}}} \lnot \lnot B^c\Rightarrow B^c$.

Moreover, notice that all classical right rules plus the right rules for the common connectives in ${\mathsf {LEci}}$ (or ${\mathsf {LEci}}'$) are invertible. Since invertible rules can be applied eagerly when proving a sequent, this entails that classical formulae can be eagerly decomposed. As a consequence, we have the following remarkable result.

Theorem 2

Let C be a classical formula and $\varGamma$ be a multiset of Ecumenical formulae. Then

$$\begin{aligned} \vdash _{{\mathsf {LEci}}}\bigwedge \varGamma \rightarrow _c C \text{ iff } \vdash _{{\mathsf {LEci}}}\bigwedge \varGamma \rightarrow _i C. \end{aligned}$$

Proof

We have already shown that the intuitionistic implication entails the classical one. For the other direction, consider the sequent

$$\begin{aligned} \bigwedge \varGamma \rightarrow _c C\Rightarrow \bigwedge \varGamma \rightarrow _iC. \end{aligned}$$

(1)

By Proposition 1, the rules $\rightarrow _iR$ and $\wedge _L$ can be eagerly applied so that the sequent (1) is provable iff

$$\begin{aligned} \bigwedge \varGamma \rightarrow _c C,\varGamma \Rightarrow C \end{aligned}$$

(2)

is provable. The proof now follows by a case analysis.

• i. Case $C=\bot$. This case is trivial since we have already proved that ${\mathsf {LEci}}$ does not distinguish between intuitionistic and classical negations.

• ii. Case $C=A\rightarrow _c B$. The following is a proof of sequent (2)

  

  where the double bar means possible application of various rules.

  Cases where $C=\lnot A, A\vee _cB, \exists _cx.A, P^n_c$ are analogous since the rules $\lnot R, \vee _cR, \exists _cR$ and $R_c$ introduce, bottom-up, empty succedents.

• iii. Cases $C=A\wedge B$ or $C=\forall x.A$. Since rules $\wedge R,\forall R$ are invertible and do not change the left context, C can be eagerly decomposed by applying such rules until arriving to premises of the shape $\bigwedge \varGamma \rightarrow _c C,\varGamma \Rightarrow C'$ with $C'$ of the form $A'\rightarrow _c B',\lnot A', A'\vee _cB', \exists _cx.A', P^n_c,\bot$. Hence

  

  where $\varGamma '$ is the multiset determined by the rule $\star R\in \{\rightarrow _cR,\lnot R, \vee _cR, \exists _cR,R_c\}$ (if $C'=\bot$ then no rule is applied and $\varGamma '=\emptyset$). Now, C can be decomposed on the left, with left conjunction and universal quantification rules being applied so to mimic the application of right rules for transforming C into $C'$. This process will transform C into $C'$ in the left side of the left premise as well, and hence we have the derivation

  

  Finally, since $\varGamma ',C'\Rightarrow \bot$ is provable by Cases (i.) and (ii.), the result follows. $\square$

That is, the Ecumenical entailment, when restricted to classical succedents (antecedents having an unrestricted form), is classical!

Wrapping up: entailments $\vdash _{{\mathsf {LEci}}} \varGamma \Rightarrow A$ are intrinsically intuitionistic. But when A is classical, entailments can be read classically. And this justifies the Ecumenical view of entailments in Prawitz’s original proposal.

4 A semantical view of ecumenical systems

In Avigad (2001), the negative translation was used to relate cut-elimination theorems for classical and intuitionistic logics. Since part of the argumentation was given semantically, a notion of Kripke semantics for classical logic was stated, via the respective semantics for intuitionistic logic and the double negation interpretation [see also Ilik et al. (2010)]. In Pereira and Rodriguez (2017) a similar definition was given, but under the Ecumenical approach. In the following, we will present an extension of the semantics given in Pereira and Rodriguez (2017) so as to handle also the quantifiers.

Definition 6

An Ecumenical Kripke model is a triple $\mathcal{M}_{KE}$ = $\langle W, \varSigma , D \rangle$ where (1) W is a partially ordered set, (2) D is a function that assigns to each node $w\in W$ an inhabited set D(w) of parameters such that if $w \le v$, then $D(w) \subseteq D(v)$, and (3) $\varSigma (k) \subseteq At_{k}$ such that if $w \le v$, then $\varSigma (w) \subseteq \varSigma (v)$, where $At_{k}$ is the set of atomic sentences with parameters in D(k). Let $\mathcal{M}_{KE}=\langle W, \varSigma , D \rangle$ be an Ecumenical Kripke model and $w \in W$. By induction in the construction of a formula A, we define the forcing relation $\mathcal{M}_{KE},w\Vdash A$ as follows

$$\begin{aligned} \begin{array}{l@{\qquad }c@{\qquad }l} \mathcal{M}_{KE},w\Vdash P_{i}^{n}(a_1,...,a_n) &{} \text{ iff } &{} P_{i}^{n}(a_1,...,a_n)\in \varSigma (w);\\ \mathcal{M}_{KE},w \Vdash \bot &{} &{} \text{ never } \text{ holds };\\ \mathcal{M}_{KE},w\Vdash \lnot A &{} \text{ iff } &{} \forall \, v\ge w. \mathcal{M}_{KE},v\not \Vdash A;\\ \mathcal{M}_{KE},w\Vdash A\wedge B &{} \text{ iff } &{} \mathcal{M}_{KE},w\Vdash A \text{ and } \mathcal{M}_{KE},w\Vdash B;\\ \mathcal{M}_{KE},w\Vdash \forall x.A(x) &{} \text{ iff } &{} \forall v\ge w, a\in D(v). \mathcal{M}_{KE},v\Vdash A(a).\\ \mathcal{M}_{KE},w\Vdash A\vee _i B &{} \text{ iff } &{} \mathcal{M}_{KE},w\Vdash A \text{ or } \mathcal{M}_{KE},w\Vdash B;\\ \mathcal{M}_{KE},w\Vdash A\rightarrow _i B &{} \text{ iff } &{} \forall v\ge w. \mathcal{M}_{KE},v\not \Vdash A \text{ or } \mathcal{M}_{KE},v\Vdash B;\\ \mathcal{M}_{KE},w\Vdash \exists _i x.A(x) &{} \text{ iff } &{}\exists a \in D(w). \mathcal{M}_{KE},w\Vdash A(a).\\ \mathcal{M}_{KE},w\Vdash P^n_c(a_1,...,a_n) &{} \text{ iff } &{} \mathcal{M}_{KE},w\Vdash \lnot (\lnot P^n_i(a_1,...,a_n));\\ \mathcal{M}_{KE},w\Vdash A\vee _c B &{} \text{ iff } &{} \mathcal{M}_{KE},w\Vdash \lnot (\lnot A\wedge \lnot B);\\ \mathcal{M}_{KE},w\Vdash A\rightarrow _c B &{} \text{ iff } &{} \mathcal{M}_{KE},w\Vdash \lnot (A\wedge \lnot B).\\ \mathcal{M}_{KE},w\Vdash \exists _c x.A(x) &{} \text{ iff } &{} \mathcal{M}_{KE},w\Vdash \lnot (\forall x.\lnot A(x)).\\ \end{array} \end{aligned}$$

The Ecumenical consequence relation $\Vdash _{\mathsf {E}}$ is defined as usual: $\Vdash _{\mathsf {E}}\varGamma \Rightarrow A$ iff every Ecumenical Kripke model of $\varGamma$ is also a model of A. We will omit the model from the notation when it is irrelevant or it can be inferred from the context.

The only differences between this formulation and the one presented in Pereira and Rodriguez (2017) are the explicit definition of the interpretation of classical propositional variables and the interpretation of the quantifiers. Since Definition 6 is the canonical Kripke interpretation for (first order) intuitionistic logic (Fitting 2014), and since the classical connectives are interpreted via the intuitionistic ones using the double-negation translation, the results of soundness and completeness of the semantical interpretation above w.r.t. the sequent system ${\mathsf {LEci}}$ are trivial.

Theorem 3

${{\mathsf {LEci}}}$ is sound and complete w.r.t. the Ecumenical Kripke semantics, that is, $\vdash _\mathrm{{{\mathsf {LEci}}}}\varGamma \Rightarrow A$ iff $\Vdash _{{\mathsf {E}}}\varGamma \Rightarrow A$.

We end this section by having a closer look into negation. Observe that $\lnot A\equiv A\rightarrow _c\bot \equiv A\rightarrow _i\bot$ can be interpreted in the following three different ways

• a. $\mathcal{M}_{KE},w\Vdash \lnot A$ iff $\forall \, v\ge w. \mathcal{M}_{KE},v\not \Vdash A$;

• b. $\mathcal{M}_{KE},w\Vdash A\rightarrow _i \bot$ iff $\forall v\ge w. \mathcal{M}_{KE},v\not \Vdash A \text{ or } v\Vdash \bot$;

• c. $\mathcal{M}_{KE},w\Vdash A\rightarrow _c \bot$ iff $\mathcal{M}_{KE},w\Vdash \lnot (A\wedge \lnot \bot )$;

Since $A\wedge \lnot \bot \equiv A$, (a.) and (c.) are immediately equivalent. And, since $\mathcal{M}_{KE},w \Vdash \bot$ never holds, (a.) and (b.) are also equivalent. However, although it seems that the choice of words is irrelevant, there is a philosophical difference in the statements: for establishing that (a.) and (c.) are equivalent, we used the syntactical notion of equivalence, while (a.) and (b.) express the exact same sentence, with different notations.

Nevertheless, it is interesting to note that in ${\mathsf {LEci}}$ the negation behaves classically. In fact, analysing the derivations

(a) is closer to (c) than to (b). Digging further, this is the desirable behaviour, since on proving a sequent like $\varGamma ,\lnot (A\wedge \lnot B)\Rightarrow C$ starting (bottom-up) with the $\lnot L$ rule, one should expect that C should be constrained to be $\bot$, since the semantical definition of $A\rightarrow _c B$ is given in terms of $\lnot (A\wedge \lnot B)$.

That is, although $A\rightarrow _c \bot \equiv A\rightarrow _i\bot \equiv \lnot A$, applications of the “intuitionistic negation” $A\rightarrow _i\bot$ are more permissive than $\lnot A$ and $A\rightarrow _c \bot$ in ${\mathsf {LEci}}$. These matters will disappear in the multiple-conclusion systems presented next, since they carry better, in the syntax, the semantical interpretation of the logic.

5 Towards locality

While the simplicity of the sequent framework makes it an ideal tool for proving meta-logical properties, sequent calculus is often not expressive enough for constructing cut-free calculi for many logics of interest [see e.g. Avron (1996)]. As a result, many new formalisms have been proposed over the last 30 years, including hypersequent calculi (Avron 1991), nested calculi (Brünnler 2009; Poggiolesi 2009) and labelled calculi (Gabbay 1996; Viganò 2000). All such formalisms expand the sequent framework with some notion of locality: an inference rule is called local when it does not place any restriction on side formulae in the context. Although ${\mathsf {LEci}}$ is cut-free, the classical rules are not local, since they impose restrictions on the context. Moreover, the sequent rules do not, at a first sight, reflect the semantical interpretation of the connectives. In this section, we will propose a (local) nested system for the Ecumenical logic based on the semantical description given in the last section, allowing also the proposal of a multiple-conclusion Ecumenical system.

Nested systems are extensions of the sequent framework where a single sequent is replaced with a tree of sequents. Sequents in nested sequents have the form $\varGamma \Rightarrow \varDelta$, where $\varGamma ,\varDelta$ are multi-sets of formulae.

Definition 7

A nested sequent is defined inductively as follows:

• if $\varGamma \Rightarrow \varDelta$ is a sequent, then it is a nested sequent;

• if $\varGamma \Rightarrow \varDelta$ is a sequent and $G_1,\ldots ,G_k$ are nested sequents, then $\varGamma \Rightarrow \varDelta ,[G_1],\ldots ,[G_k]$ is a nested sequent.

A nested system (${\mathsf {NS}}$) consists of a set of inference rules acting on nested sequents.

For readability, we will denote by $\varGamma ,\varDelta$ sequent contexts and by $\varLambda$ sets of nestings. In this way, every nested sequent has the shape $\varGamma \Rightarrow \varDelta , \varLambda$ where elements of $\varLambda$ have the shape $[\varGamma '\Rightarrow \varDelta ', \varLambda ']$ and so on. We will denote by $\varUpsilon$ an arbitrary nested sequent.

Rules in nested systems will be represented using holed contexts.

Definition 8

A nested-holed context is a nested sequent that contains a hole of the form $\{ \; \}$ in place of nestings. We represent such a context as ${\mathcal {S}}\left\{ \;\right\}$. Given a holed context and a nested sequent $\varUpsilon$, we write ${\mathcal {S}}\left\{ \varUpsilon \right\}$ to stand for the nested sequent where the hole $\{\;\}$ has been replaced by $\left[ \varUpsilon \right]$, assuming that the hole is removed if $\varUpsilon$ is empty and if ${\mathcal {S}}$ is empty then ${\mathcal {S}}\left\{ \varUpsilon \right\} =\varUpsilon$.

For example, $(\varGamma \Rightarrow \varDelta ,\{\;\})\{\varGamma '\Rightarrow \varDelta '\}= \varGamma \Rightarrow \varDelta ,\left[ \varGamma '\Rightarrow \varDelta '\right]$ while $\{\;\}\{\varGamma '\Rightarrow \varDelta '\}= \varGamma '\Rightarrow \varDelta '$. The idea of holes and nestings is that rules can be applied deep inside a nested structure. The calculus ${\mathsf {NS}}_{{\mathsf {LEci}}}$ is depicted in Fig. 4.

Fig. 4

Ecumenical nested sequent system ${\mathsf {NS}}_{{\mathsf {LEci}}}$. In rules $\forall R$, $\exists _c L$ and $\exists _i L$, the parameter a is fresh, while in $\exists _i R, \forall L$, a does not occur in $\varLambda$

In face of Fact 1, following Lellmann (2015) we can give an Ecumenical interpretation for nestings in terms of the intuitionistic implication.

Definition 9

The Ecumenical formula translation $\iota _{{\mathsf {E}}}$ for nested sequents is given by

• if $\varGamma \Rightarrow \varDelta$ is a sequent, then $\iota _{{\mathsf {E}}}(\varGamma \Rightarrow \varDelta )= \bigwedge \varGamma \rightarrow _i \bigvee _i\varDelta$.

• $\iota _{{\mathsf {E}}}\left( \varGamma \Rightarrow \varDelta ,\left[ \varGamma _1\Rightarrow \varDelta _1,\varLambda _1\right] ,\ldots ,\left[ \varGamma _n\Rightarrow \varDelta _n,\varLambda _n\right] \right) = \bigwedge \varGamma \rightarrow _i (\bigvee _i\varDelta \vee _i\iota _{{\mathsf {E}}}\left( \varGamma _1\Rightarrow \varDelta _1,\varLambda _1\right) \vee _i\ldots \vee _i\iota _{{\mathsf {E}}}\left( \varGamma _n\Rightarrow \varDelta _n,\varLambda _n\right)$.

The following semantical interpretation of nestings as possible worlds in intuitionistic logic was given in Fitting (2014):

“A sequent $\varGamma \Rightarrow \varDelta$ is true at a state [of a Kripke model] provided that, if all members of $\varGamma$ are forced there, so is some member of $\varDelta$. And let us say a boxed sequent, $\left[ S\right]$, is true at a state provided the sequent S is true at that state and at every state accessible from it”.

In our setting, the nested sequent $\cdot \Rightarrow \left[ \varGamma \Rightarrow \varDelta ,\varLambda \right]$ has the following Ecumenical interpretation

$$\begin{aligned} \top \rightarrow _i \iota _{\mathsf {E}}(\varGamma \Rightarrow \varDelta ,\varLambda ) \end{aligned}$$

where $\top = \bot \rightarrow _i\bot$, which is valid in a world w iff $\forall v\ge w. v\Vdash \iota _{\mathsf {E}}(\varGamma \Rightarrow \varDelta ,\varLambda )$. That is, the nested sequent $\varGamma \Rightarrow \varDelta ,\varLambda$ is evaluated in a world v such that $v\ge w$. This gives a 1-1 correspondence between nestings and worlds in an Ecumenical Kripke frame. Such a correspondence justifies the so-called indexed nestings (Fitting 2014), where nestings carry over the semantical information (in this case, we could write $\left[ \varGamma \Rightarrow \varDelta ,\varLambda \right] _v$). Moreover, by monotonicity of Kripke frames, if a formula is valid in v, it will be valid in every world u such that $u\ge v$, which is the same semantical interpretation for nestings given by Fitting.

The following fact holds for ${\mathsf {NS}}_{{\mathsf {LEci}}}$.

Fact 2

When classical left rules are applied, the right context is erased (bottom-up).

Fact 3

Universal quantifier and intuitionistic implication (hence also negation) are the sole connectives responsible for creating deeper nestings.

Fact 2 simply corroborates the evidence that, in the double negation setting, classical information must be confined to the antecedent of a sequent; moreover this implies that classical formulae should be evaluated in the world corresponding to the nesting they are in, which carries all and only the classical truth information. All further (hence intuitionistic) semantic information should be erased. This is a perfect reading of the semantics in the classical setting.

Fact 3, on the other hand, reflects the “for all” statement in the semantical description given in the last section. Observe that classical connectives are semantically described using intuitionistic implication (via negation), hence right rules on these connectives also create fresh nestings.

Using the Ecumenical interpretation of nestings, it is straightforward to prove soundness of ${\mathsf {NS}}_{{\mathsf {LEci}}}$ with respect to the Ecumenical Kripke semantics given in last section.

Theorem 4

The rules of ${\mathsf {NS}}_{{\mathsf {LEci}}}$ preserve validity in Ecumenical Kripke frames with respect to the formula interpretation $\iota _{{\mathsf {E}}}$.

Proof

The proof is a straightforward adaptation of the one presented in Lellmann (2015): for every rule in ${\mathsf {NS}}_{{\mathsf {LEci}}}$, we construct a world falsifying the interpretation of a premise from a world falsifying the interpretation of the conclusion. We will illustrate this by taking as an example the $\lnot L$ rule. By an abuse of notation, we denote by $\iota _{\mathsf {E}}(\varLambda )$ the interpretation $\iota _{\mathsf {E}}(\cdot \Rightarrow \left[ G_1\right] ,\ldots ,\left[ G_k\right] )$, where $\varLambda =\left[ G_1\right] ,\ldots ,\left[ G_k\right]$.

Suppose that the interpretation

$$\begin{aligned} \bigwedge \varGamma _1 \rightarrow _i \bigvee \nolimits _i\varDelta _1\bigvee \nolimits _i\iota _{\mathsf {E}}(\varLambda _1) \vee _i(\ldots (\bigwedge \varGamma _n\wedge (\lnot A)\rightarrow _i \bigvee \nolimits _i\varDelta _n\vee _i\iota _{{\mathsf {E}}}(\varLambda _n))\ldots ) \end{aligned}$$

of the conclusion of rule $\lnot L$ does not hold in world w in an Ecumenical Kripke frame. Then there are worlds $w_1,\ldots , w_n$ such that $w\le w_1 \le \ldots \le w_n$ with $w_j\Vdash _{\mathsf {E}}\varGamma _j$, $w_j\not \Vdash _{\mathsf {E}}\bigvee _i\varDelta _j$, $w_{j}\not \Vdash _{\mathsf {E}}\bigvee _i\iota _{\mathsf {E}}(\varLambda _j)$ and $w_n\Vdash \lnot A$. Hence, by definition, $w_n\not \Vdash \lnot A$ and thus the formula interpretation of the premise is falsified in $w_n$.

For the quantifier rules we use monotonicity of domains. For example, if the interpretation

$$\begin{aligned} \bigwedge \varGamma _1 \rightarrow _i \bigvee \varDelta _1\bigvee \nolimits _i\iota _{\mathsf {E}}(\varLambda _1) \vee _i(\ldots (\bigwedge \varGamma _n\wedge (\forall x.A)\rightarrow _i \bigvee \nolimits _i\varDelta _n\vee _i\iota _{{\mathsf {E}}}(\varLambda _n))\ldots ) \end{aligned}$$

of the conclusion of $\forall L$ does not hold at world w in an Ecumenical Kripke frame, there are worlds $w_1,\ldots , w_n$ such that $w\le w_1 \le \ldots \le w_n$ with $w_j\Vdash _{\mathsf {E}}\varGamma _j$, $w_j\not \Vdash _{\mathsf {E}}\bigvee _i\varDelta _j$, $w_{j}\not \Vdash _{\mathsf {E}}\bigvee _i\iota _{\mathsf {E}}(\varLambda _j)$ and $w_n\Vdash \forall x. A$. If $a\in D(w_j)$ for some $1\le j \le n$ then $a\in D(w_n)$ and $w_n\Vdash _{\mathsf {E}}A[a/x]$ and the interpretation of the premise of $\forall L$ is falsified at w. If $a\notin D(w_j)$ for all $1\le j <n$, we augment $D(w_n)$ with a and the result follows the same way. $\square$

Instead of proving the completeness result directly, we will do it via a multiple-conclusion Ecumenical system. This detour has a sensible explanation: nested systems are extensions of the sequent approach that are closely related to semantics, as we just saw. On the other hand, it is not clear how to get any semantic information out of the (single-conclusion) sequent system presented in Sect. 3. Multiple conclusion sequent calculi often make a bridge between sequent and nested sequent systems.

Fig. 5

Ecumenical multi-conclusion system ${\mathsf {mLEci}}$. In rules $\forall R$, $\exists _c L$ and $\exists _i L$, the parameter a is fresh

The multiple-conclusion Ecumenical sequent system ${\mathsf {mLEci}}$ is actually built from ${\mathsf {LEci}}'$ by introducing the information given by Facts 2 and 3 . More specifically, every time the “accessible worlds” information should be removed (a new world is created), the right context information is erased (frozen) in the premises. The rules for the multiple-conclusion version of ${\mathsf {LEci}}'$ are given in Fig. 5. Observe that the comma in the succedent is intuitionistic, as in the multiple conclusion intuitionistic sequent system  (Maehara 1954).

The following completeness result connects nested and multi-conclusion sequent settings.

Theorem 5

If $\varGamma \Rightarrow \varDelta$ is provable in ${\mathsf {mLEci}}$, then ${\mathcal {S}}\left\{ \varGamma \Rightarrow \varDelta \right\}$ is provable in ${\mathsf {NS}}_{{\mathsf {LEci}}}$.

Proof

It is easy to see that any derivation in ${\mathsf {mLEci}}$ can be converted, bottom-up, into a derivation in ${\mathsf {NS}}_{{\mathsf {LEci}}}$. Illustrating the rules for implication right

Regarding the quantifier rules, we have to make sure that the variable conditions hold. For $\forall R$, the conversion is the following

Since the parameter a is fresh in the left derivation, we can assume that it does not occur in $\mathcal{S}$, and the variable condition for the nested $\forall R$ rule is satisfied. $\square$

We close this section by showing that ${\mathsf {mLEci}}$ is equivalent to ${\mathsf {LEci}}$.

Theorem 6

$\vdash _\mathrm{{{\mathsf {mLEci}}}}\varGamma \Rightarrow \varDelta$ iff $\vdash _\mathrm{{{\mathsf {LEci}}}}\varGamma \Rightarrow \bigvee _i\varDelta$.

Proof

The completeness direction is trivial, since all rules in ${\mathsf {LEci}}$ are (restricted versions) of rules in ${\mathsf {mLEci}}$ and the $\vee _iR$ rule is invertible in ${\mathsf {mLEci}}$.

Soundness is proven by easy induction of the derivation $\pi$ of $\varGamma \Rightarrow \varDelta$ in ${\mathsf {mLEci}}$. For example, if $\varDelta =A\rightarrow _cB,\varDelta '$ and the last rule applied in $\pi$ is

by inductive hypothesis $\varGamma ,A\Rightarrow B$ is derivable in ${\mathsf {LEci}}$. Hence

$\square$

Wrapping up: we have shown

Hence all Ecumenical systems (single and multi conclusion sequent; and nested systems) are sound and complete with respect to the Ecumenical Kripke semantics.

6 Classical and intuitionistic fragments

Since we already saw that the entailment in Ecumenical systems is actually intuitionistic, an interesting question would be what happens if we get from any of the Ecumenical systems presented here only the pure classical or intuitionistic fragments.

In the intuitionistic case the answer is trivial: restricting any calculus presented here entails the well known calculi for intuitionistic logic. As an example, we present in Fig. 6 the rules for pure intuitionistic ${\mathsf {mLEci}}$, which collapses to (Maehara 1954). The only observation is that, in this system, weakening is admissible, so it is not shown as part of the rules.

Fig. 6

${\mathsf {mLEci}}$’s intuitionistic fragment, or system . In rules $\forall R$ and $\exists _i L$, the parameter a is fresh

The classical fragment, however, is a little more interesting, as it takes some work for it to be understood.

First of all, the following theorem comes straightforwardly, using induction.

Theorem 7

$\varGamma \Rightarrow \varDelta$ is provable in the classical fragment of ${\mathsf {mLEci}}$ iff either $\varGamma \Rightarrow \cdot$ is provable or there is $A\in \varDelta$ such that $\varGamma \Rightarrow A$ is provable in such a fragment.

This means that the single and multiple conclusion calculi collapse in the classical case, what is not at all surprising since the comma in the succedent of sequents in ${\mathsf {mLEci}}$ correspond to the intuitionistic disjunction $\vee _i$.

The system ${\mathsf {LEc}}$, the classical fragment of ${\mathsf {LEci}}$, is shown in Fig. 7, where classical and intuitionistic interpretations for atomic predicates are collapsed. Note that weakening is admissible in ${\mathsf {LEc}}$ and all the rules are invertible (thanks to Theorem 2). ${\mathsf {LEc}}$ impersonates a goal directed proof search (Miller et al. 1991), where right formulae are decomposed totally until either an axiom is applied and the proof terminates, or the succedent of the premises are bottom, in which case left rules are applied.

Fig. 7

Sequent system ${\mathsf {LEc}}$: the classical fragment of ${\mathsf {LEci}}$. In rules $\forall R$ and $\exists _c L$, the parameter a is fresh

7 Conclusion and future research directions

In this work we have analysed the Ecumenical notion of entailment proposed by Prawitz (2015). To do this analysis we moved to the sequent calculus formulation of the system, where proof-theoretical results showed that the Ecumenical entailment is, in general, intuitionistic, but it turns classical in the presence of classical succedents. We then produced a nested sequent version of the original sequent system and showed all of them sound and complete with respect to (a small extension of) the Ecumenical Kripke semantics of Pereira and Rodriguez. Finally, we analysed fragments of the systems presented, coming to well known intuitionistic calculi and a sequent system for classical logic amenable to a treatment by goal directed proof search.

Since the idea of using different signs for the different meanings attached to intuitionistic and classical operators is not new, some comparison should be done with other systems in the literature that combine intuitionistic and classical logics.

Regarding proof systems, there is the seminal work of Girard (1993), and the more recent work of Liang and Miller (2011). Their work is based on polarities and focusing, using translations into linear logic. Since the explicit use of double-negation has the effect of throttling focused proofs, the systems we obtain is essentially different from fragments of Girard’s LU or Liang-Miller’s LKF. Hence it seems that there is little or no intersection of the systems presented here and the ones inspired by linear logic. However, our Ecumenical systems seem to be amenable for a definition of focusing and normal derivations in the same lines as in Boudard and Hermant (2013). This is certainly a future work direction worth pursuing.

Prawitz’ main motivation for the introduction of the Ecumenical system was philosophical: to provide a logical framework that would make possible an inferentialist semantics for the classical logical constants. The usual Gentzen’s introduction rules for the logical constants can be taken as constitutive of their meanings from the intuitionistic point of view. On the other hand, classical logic does not seem to allow for the same semantical approach. As Prawitz puts it,

“no canonical proof of an arbitrarily chosen instance of the law of the excluded middle is known, nor any reduction that applied to a proof terminating with an application of the classical form of reductio ad absurdum gives a canonical proof of the conclusion”.

According to Prawitz, this is no reason to give up the inferentialist approach to classical logic: we just have to find the adequate introduction rules for the classical connectives.

Krauss (1992) and Dowek (2016) explored the same Ecumenical ideas. Their main motivation was mathematical: to explore the possibility of hybrid readings of axioms and proofs in mathematical theories, i.e., the occurrences of classical and intutionistic operators in mathematical axioms and proofs, in order to propose a new and original method of constructivisation of classical mathematics. Krauss applied these ideas in basic algebraic number theory and Dowek considered the example of an Ecumenical proof of a simple theorem in basic set theory.

Our motivation follows Prawitz’ suggestion: we would like to see whether we can provide an inferentialist approach to classical logic. Because, like Krauss and Dowek, we want to extend the reach of constructive proof-theory to classical and/or hybrid systems, where some operators and some formulae are classic, others intuitionistic. The criteria for success are mixed, some mathematical (the elegance of the basic proofs counts), others more philosophical (the purer the system, the better). In any case, this is a long-reaching programme, for which we have given the first steps.