May 04, 2026
In this paper, we revisit Glivenko’s theorems, foundational results relating classical and intuitionistic logic, from an ecumenical perspective. We begin by discussing the historical context and significance of Glivenko’s original contributions, and then examine their extensions and reinterpretations within ecumenical logical frameworks. Our analysis focuses on three ecumenical systems: Prawitz’s natural deduction system \(\mathsf{NE}\); the system \(\mathsf{NE_{K}}\), closely related to one introduced by Krauss in an unpublished manuscript; and the \(\mathsf{ECI}\) system proposed by Barroso-Nascimento.
In the late twenties and early thirties of last century, several results were obtained concerning some relations between classical logic (\(\mathsf{CL}\)) and intuitionistic logic (\(\mathsf{IL}\)), as well as between classical arithmetic (\(\mathsf{PA}\)) and intutionistic arithmetic (\(\mathsf{HA}\)). In 1925, Kolmogorov proved that classical propositional logic (\(\mathsf{CPL}\)) could be translated into intuitionistic propositional logic (\(\mathsf{IPL}\)) [1]. In 1933, Gödel defined an interpretation of \(\mathsf{PA}\) into \(\mathsf{HA}\) [2] and in the same year Gentzen defined a different interpretation of \(\mathsf{PA}\) into \(\mathsf{HA}\) [3]. These interpretations/translations1 were defined as functions from the language of \(\mathsf{PA}\) (or \(\mathsf{CL}\), \(\mathsf{CPL}\)) into some fragment of the language of \(\mathsf{HA}\) (\(\mathsf{IL}\), \(\mathsf{IPL}\)) that aimed to preserve some important properties, like theoremhood or derivability. What is known as Glivenko’s theorems in the area of logic belongs to this group of important results.
Valery Glivenko’s results were published in 1929, in French, in the Bulletins de la Classe des Sciences de la Académie Royale de Belgique, under the title Sur quelques points de la logique de M. Brouwer [8]. The first Glivenko theorem establishes that if a formula \(A\) is classically provable in \(\mathsf{CPL}\), then its double negation is intuitionistically provable in \(\mathsf{IPL}\)2.
Theorem 1. If \(\vdash_{\mathsf{CPL}} A\), then \(\vdash_{\mathsf{IPL}} \neg \neg A\).
In all of the logics considered in this paper, \(\neg A\) is defined as \(A \to \bot\), a convention we may also adopt in classical and intuitionistic logic.
This theorem is known to hold in full generality only for propositional logic. However, an immediate corollary of Seldin’s normalization strategy for first-order classical logic3 [10], [11], together with its translation into intuitionistic first-order logic due to Kuroda [4], [6], is that the theorem also holds for first-order formulas that do not contain universal quantifiers. Moreover, Andrés Raggio derived the normalization theorem for Gentzen’s classical Natural Deduction system \(\mathsf{NK}\) as a consequence of Glivenko’s first theorem [12]. This shows that the theorem is closely tied both to translation techniques and to normalization strategies.
The second Glivenko theorem establishes that if a formula \(\neg A\) is provable \(\mathsf{CPL}\), then the same formula is provable in \(\mathsf{IPL}\):
Theorem 2. If \(\vdash_{\mathsf{CPL}} \neg A\), then \(\vdash_{\mathsf{IPL}} \neg A\).
The second theorem is a trivial consequence of the first: by the first theorem, \(\vdash_{\mathsf{CPL}} \neg A\) implies \(\vdash_{\mathsf{IPL}} \neg \neg \neg A\), and \(\vdash_{\mathsf{IPL}} \neg \neg \neg A\) intuitionistically implies \(\vdash_{\mathsf{IPL}} \neg A\).
In a way, Glivenko’s theorems allow classical validities to be sought constructively. This allows us to conceive propositional classical logic as a part of propositional intuitionistic logic, the latter being capable of making more fine-grained distinctions than the former.
This paper examines Glivenko’s theorems through the lens of ecumenical logic, focusing on their implications and extensions within a unified logical framework. We begin by revisiting Glivenko’s original results and their historical context, emphasizing their significance in bridging the gap between classical and intuitionistic logic. Building on this idea, we explore the application of ecumenical systems, such as those proposed by Prawitz, Krauss, and Barroso-Nascimento, to formalize and generalize Glivenko-type results. Finally, we argue that the ecumenical perspective sheds light on the interplay between classical and intuitionistic reasoning, offering a deeper understanding of their coexistence within a single system while respecting their distinct inferential principles.
In 2015, Dag Prawitz proposed a natural deduction system where classical logic and intuitionistic logic could both be codified [13]. Prawitz’s system is an example of what nowadays is called an ecumenical system [14]. Ecumenical systems allow two or more logics, even rival ones, to coexist peacefully. This peaceful coexistence means that the combination will not produce a collapse of a weaker logic into a stronger one, thus naturally preserving the essential characteristics of the logics involved in the combination4.
In Prawitz’s system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd (the so-called neutral operators), but they would each have their own existential quantifier, disjunction and implication, with different meanings (\(\exists_j,\vee_j,\to_j\), where \(j\in\{i,c\}\) for the intuitionistic and classical versions, respectively). Also, classical and intuitionistic \(n\)-ary predicate letters (\(P_{c}^{n}, P_{i}^{n},\ldots\)) co-exist but have different meanings. Prawitz’s main idea is that these different meanings are given by a semantical framework that can be accepted by both parties5. Prawitz’s ecumenical system, here called \(\mathsf{NE}\), is shown in Fig. 1.
None
Figure 1: Ecumenical natural deduction system \(\mathsf{NE}\). In rules \(\forall-int\) and \(\exists_i-elim\), the parameter \(a\) is fresh. In \(\exists_i-int\) and \(\forall-elim\), \(t\) is a term..
It is obvious that we cannot have Glivenko’s theorems in Prawitz’s ecumenical system for the plain reason that we do not have two systems, the intuitionistic system and the classical system, but only one, the ecumenical system. However, we can have a kind of internal Glivenko, which establishes Glivenko-type relations between classical operators and intuitionistic operators.
Theorem 3. For any formula \(C\) such that the main operator of \(C\) is a classical operator, we have that \(C \vdash_{\mathsf{NE}} \neg \neg C^{*}\), where \(C^{*}\) is the result of replacing the classical operator by the corresponding intutionistic operator.
Proof. We examine below the case of each classical operator:
\(C\) is \(A \vee_{c} B\). We can prove that \(A \vee_{c} B \vdash_{\mathsf{NE}} \neg \neg (A \vee_{i} B)\) as follows:
\(C\) is \(A \to_{c} B\). We can prove that \(A \vee B \vdash_{\mathsf{NE}} \neg \neg (A \to_{i} B)\) as follows:
\(C\) is \(\exists_{c} xA(x)\). We can prove that \(\exists_{c} xA(x) \vdash_{\mathsf{NE}} \neg \neg \exists_{i} xA(x)\) as follows:
◻
We can also have an internal result corresponding to Glivenko’s second theorem:
Theorem 4. For any formula \(C\) such that the main operator of \(C\) is a classical operator, we have that \(\neg C \vdash_{\mathsf{NE}} \neg C^{*}\), where \(C^{*}\) is the result of replacing the classical operator by the corresponding intutionistic operator.
Proof. The result follows directly from the fact that \(C^{*} \vdash_{\mathsf{NE}} C\).
For example:
◻
Another ecumenical system, the system \(\mathsf{ECI}\), was introduced by Victor Barroso-Nascimento, and its main idea is:
[\(\ldots\)] the generalist approach consists of adding general rules which allow the introduction of ecumenical versions of any formula. Thus, instead of directly defining assertion conditions for specific ecumenical connectives, the generalist approach aims to define assertion conditions for ecumenical formulas in general, so as we can introduce the remaining ecumenical operators as special cases of the general rule [18]).
Instead of the ecumenical operators of Prawitz’s “inferentialist" approach6, we have ecumenical formulas, \(A\) and \(A^{c}\)7. The system \(\mathsf{ECI}\) is obtained from Prawitz’s natural deduction system for intuitionistic logic by adding the following rules:
We can immediately see that Glivenko-type results are somehow trivial in \(\mathsf{ECI}\)8:
Theorem 5. \(A^{c} \vdash_{\mathsf{ECI}} \neg \neg A\)
Proof. Immediate by the following derivation
◻
Theorem 6. \((\neg A)^{c} \vdash_{\mathsf{ECI}} \neg A\)9
Proof. Direct from Theorem 5 and by the fact that \(\neg \neg \neg A \vdash_{\mathsf{ECI}} \neg A\). ◻
We have shown that \(A^{c} \vdash_{\mathsf{ECI}} \neg \neg A\), but we can trivially also show that
\(\neg \neg A \vdash_{\mathsf{ECI}} A^{c}\):
In a certain sense, the equivalence between \(\neg \neg A\) and \(A^{c}\) provides a justification for the translation presented on page 52 of [18], here reformulated in a recursive manner.
Definition 1. \(t\mathsf{ECI}[A]\) is defined as follows, where A is a formula of \(\mathsf{ECI}\):
\(t\mathsf{ECI}[p] = p\), for atomic \(p\);
\(t\mathsf{ECI}[\bot] = \bot\);
\(t\mathsf{ECI}[A \star B] = t\mathsf{ECI}[A] \star t\mathsf{ECI}[B]\), for \(\star \in \{\land, \lor, \to\};\)
\(t\mathsf{ECI}[A^{c}] = \neg \neg \; t\mathsf{ECI}[A]\).
This translation is used to reduce the problem of normalization (and other proof-theoretical results) for \(\mathsf{ECI}\) to normalization in intuitionistic logic. However, if we are interested in identifying the effects of classical reasoning within a derivation, there is another aspect of this translation that deserves attention.
Assume that we have a derivation in classical propositional logic with several applications of the classical reductio.
Suppose now that we replace each such application by an application of \(\to\)-int:
It is easy to see that the resulting derivation need not be intuitionistically valid. Consider, for instance, the following derivation:
Under the above transformation, this derivation becomes
which is not a legitimate intuitionistic derivation.
The same problem would arise if we take into consideration the translation \(t\mathsf{ECI}\). The derivation would be be transformed into:
But this derivation is also not a legitimate derivation. However, we can replace this derivation by:
And now we can see that the formula \(B\) that is derived depending on an application of classical reasoning has a classical nature too. This shows that the system \(\mathsf{ECI}\) can, in a precise way, support Krauss’ insight [19] that an ecumenical perspective helps us identify where classical reasoning is actually needed (and, importantly, that we need not be classical everywhere, nor all the time). It also allows us to make explicit the consequences of invoking classical principles within a given derivation. We turn to this point next.
The first ecumenical system for \(\mathsf{CL}\) and \(\mathsf{IL}\) was proposed and studied in 1992 by Peter Krauss [19], although he did not use the terminology “ecumenical”10. In addition to three rules for equality, a classical disjunction, a classical implication, and a classical existential quantifier, Krauss’ system also has a classical conjunction \(\wedge_{c}\)11 and a classical universal quantifier \(\forall_{c}\), retaining only negation and \(\bot\) as a neutral operator12.
In what follows we define a system \(\mathsf{NE_{K}}\), which is essentially the same system presented in [23] (the only difference being the inclusion of classical atoms) and can be proven to be equivalent to Krauss’ original system (modulo inclusion of equality and removal of classical atoms). This system is obtained by adding the rules in Fig. 2 to Prawitz’s \(\mathsf{NE}\).
None
Figure 2: Rules added to \(\mathsf{NE}\) in order to obtain the system \(\mathsf{NE_{K}}\). Since they are no longer neutral, intuitionistic conjunctions in \(\mathsf{NE_{K}}\) are also represented by \(\land_{i}\) instead of \(\land\)..
We can easily show that classical conjunction \(\wedge_{c}\) satisfies our internal Glivenko theorems.
Lemma 1. \(B \wedge_{c} C\vdash_{\mathsf{NE_{K}}} \neg \neg (B \wedge_{i} C)\)
Lemma 2. \(B \wedge_{i} C \vdash_{\mathsf{NE_{K}}} B \wedge_{c} C\)
From this lemma we can directly conclude the following:
Corollary 1. \(\neg (B \wedge_{c} C)\vdash_{\mathsf{NE_{K}}} \neg (B \wedge_{i} C)\)
It turns out that, when we restrict attention to the propositional fragment of \(\mathsf{ECI}\), we can emulate the behavior of the rules \(I_{c}\) and \(E_{c}\) of \(\mathsf{ECI}\) with respect to conjunction by means of applications of \(\wedge_{c}\)-int and \(\wedge_{c}\)-elim\(_j\) respectively. This will be addressed in the next section.
In this section we prove that, in first-order logic without universal quantification, \(\mathsf{NE_{K}}\) and \(\mathsf{ECI}\) are deductively equivalent. Equivalence results for \(\mathsf{ECI}\) and Prawitz’s \(\mathsf{NE}\) in the common fragment of their languages are established in Theorem 4 of [18]. Since \(\mathsf{NE_{K}}\) is obtained from \(\mathsf{NE}\) by adding classical conjunction, it therefore suffices to consider the induction steps corresponding to \(\land_{c}\). For reasons discussed in the next section, this equivalence does not hold for \(\mathsf{NE_{K}}\) and \(\mathsf{ECI}\) in the presence of universal quantification.
There are at least two standard approaches to comparing two (or more) ecumenical logics. In the first approach, one shows that for every natural deduction rule \(R\) of \(L_1\) whose formulation uses only a fragment of the language shared by \(L_1\) and \(L_2\), whenever the premises of \(R\) are derivable in \(L_2\), so is its conclusion (and symmetrically, the same is shown for the rules of \(L_2\) in \(L_1\)). This is the strategy adopted in [18] to establish proof-theoretic equivalence between \(\mathsf{ECI}\) and \(\mathsf{NE}\). In the second approach, rather than restricting attention to the shared fragment of the language, one defines a translation mapping each formula of the stronger logic to a formula of the weaker one. This strategy is used, for instance, in [16] to obtain certain semantic results. Since the choice between these approaches is largely a matter of convenience, we adopt the second one here.
Definition 2. \(t\mathsf{NE_{K}}\) is defined as follows, where \(A\) is a formula and \(\Gamma\) a set of formulas of \(\mathsf{ECI}\) not containing any universal quantifiers:
\(t\mathsf{NE_{K}}[p ^{i}] = p ^{i}\), for atomic \(p\) and \(i \in \{ i, c\}\);
\(t\mathsf{NE_{K}}[\bot] = t\mathsf{NE_{K}}[(\bot)^{c}] = \bot\);
\(t\mathsf{NE_{K}}[A \star B] = t\mathsf{NE_{K}}[A] \star t\mathsf{NE_{K}}[B]\), for \(\star \in \{\land, \lor, \to \};\)
\(t\mathsf{NE_{K}}[(A \star B)^{c}] = t\mathsf{NE_{K}}[A] \star_{c} t\mathsf{NE_{K}}[B]\), for \(\star \in \{\land, \lor, \to \};\)
\(t\mathsf{NE_{K}}[\exists x A] = \exists_{i} x \;t\mathsf{NE_{K}}[A]\);
\(t\mathsf{NE_{K}}[(\exists x A)^{c}] = \exists_{c} x \;t\mathsf{NE_{K}}[A]\);
\(t\mathsf{NE_{K}}[\Gamma] = \{t\mathsf{NE_{K}}[A] \; | \;A \in \Gamma \}\).
Theorem 7. \(\Gamma \vdash_{\mathsf{ECI}} A\) iff \(t\mathsf{NE_{K}}[\Gamma] \vdash t\mathsf{NE_{K}}[A]\).
Proof. By induction on the length of the derivations, in which we consider the last rule applied in the deduction (if any). The bases case is trivial, as are the cases including introduction and elimination rules for \(\neg A\), \(A \land B\), \(A \lor B\), \(A \to B\), \(\exists x A\) and classical atoms \(P^n_c(t_{1},...,t_{n})\). The step for \((\bot)^{c}\) is also trivial (since \(\neg \bot\) is a theorem of \(\mathsf{ECI}\)). This means that we only have to deal with classical operators. The proofs for \((A \to B)^{c}\), \((A \lor B)^{c}\) and \((\exists x A)^{c}\) can be found in [18] and are thus omitted – with the exception of the case of applications of \(E_{c}\) with one premise of shape \((A \to_{c} B)\), which we simplify here.
\((\Longrightarrow)\) We show that \(\Gamma \vdash_{\mathsf{NE}} A\) implies \(t\mathsf{NE_{K}}[\Gamma] \vdash_{\mathsf{NE}} t\mathsf{NE_{K}}[A]\).
In order to ease the notation, we simply write \(A\) instead of \(t\mathsf{NE_{K}}[A]\) when dealing with deductions in \(\mathsf{NE_{K}}\). This results in an ambiguity in the case of \(\bot\), so we explicitly stipulate that occurrences of \(\bot\) specifically stand for \(t\mathsf{NE_{K}}[\bot]\).
The derivation ends with an application of \(I_{C}\) with conclusion \(A \land_{c} B\). Then it has the following shape:
The inductive hypothesis yields a deduction \(\Pi^{*}\) of \(\bot\) possibly depending on \(\neg(A \land_{i} B)\). We can construct the following derivation of \(A \land_{c} B\) in \(\mathsf{NE_{K}}\):
The derivation ends with an application of \(E_{C}\) which has one premise of shape \((A \land B)^{c}\). Then it has the following shape:
The inductive hypothesis yields a deduction \(\Pi^{*}_{1}\) of \(A \land_{c} B\) and a deduction \(\Pi^{*}_{2}\) of \(\neg(A \land_{i} B)\). We can construct the following derivation of \(\bot\) in \(\mathsf{NE_{K}}\):
The derivation ends with an application of \(E_{C}\) with a premise \((A \to B)^{c}\). Then we do the following:
This is a simplification of the reduction in [18].
\((\Longleftarrow)\) We show that \(t\mathsf{NE_{K}}{[\Gamma]} \vdash_{\mathsf{NE_{K}}} t\mathsf{NE_{K}}[A]\) implies \(\Gamma \vdash_{\mathsf{ECI}} A\). Once again we only prove the inductive step for \(A \land_{c} B\); the remaining cases are proved in [18].
The derivation ends with an application of \(I \lor_{c}\). Then it has the following shape:
The inductive hypothesis yields two deductions \(\Pi^{*}_{1}\) and \(\Pi^{*}_{2}\). We can construct the following derivation of \((A \land B)^{c}\) in \(\mathsf{ECI}\):
The derivation ends with an application of \(E \land_{c}\). Then it has the following shape:
The inductive hypothesis yields two deductions \(\Pi^{*}_{1}\) and \(\Pi^{*}_{2}\). We can construct the following derivation in \(\mathsf{ECI}\):
◻
This means that, in the propositional fragment, \(\mathsf{ECI}\) and \(\mathsf{NE_{K}}\) are essentially the same logic, especially since \((\bot)^{c}\) and \(\bot\) are equivalent [18].
It is usually said that, from an ecumenical perspective, classical logicians and intuitionistic logicians would both recognize themselves in the ecumenical system, in the sense that everything they would like to accept is accepted in the ecumenical system. Although true for the intuitionistic logician, obviously this is not completely true in the case of the classical logician; for example, classical implication in \(\mathsf{NE}\) system does not satisfy the rule modus ponens: \(A , A \to_c B\vdash_{\mathsf{NE}} B\). In the case of first-order logic, we know we can prove an ecumenical result corresponding to \(\neg \forall x\neg A(x) \vdash \exists xA(x)\). But what about \(\neg \forall x\;A(x) \vdash \exists x\neg A(x)\)? In \(\mathsf{NE_{K}}\), the introduction and elimination rules for the classical universal quantifier \(\forall_{c}\) (see Fig. 2) are clearly harmonic:
Moreover, we can easily prove \(\neg \forall_{c} x A(x) \vdash_{\mathsf{NE_{K}}} \exists_{c} x\neg A(x)\):
However, as expected, we do not have a Glivenko-type result for the classical universal quantifier \(\forall_{c}\): \(\vdash_{\mathsf{NE_{K}}} \forall_{c} xA(x)\) does not imply \(\vdash_{\mathsf{NE_{K}}} \neg \neg \forall_{i} xA(x)\) (and \(\forall_{c} xA(x) \nvdash_{\mathsf{NE_{K}}} \neg \neg \forall_{i} xA(x)\)). It is interesting to observe that we do have a Glivenko-type result for the classical universal quantifier that corresponds to Glivenko’s second theorem, \(\neg \forall_{c} xA(x) \vdash_{\mathsf{NE_{K}}} \neg \forall_{i} xA(x)\):
But, as we saw, the Glivenko-type of results are somehow trivial in the system \(\mathsf{ECI}\)! Even for a universal formula we have that \((\forall xA(x))^{c} \vdash_{\mathsf{ECI}} \neg \neg \forall_{i} xA(x)\) and \(\neg (\forall xA(x))^{c} \vdash_{\mathsf{ECI}} \neg \forall_{i} xA(x)\)! If we now assume that in the formula \(A(x)\) we have no occurrences of the label/constant \(c\), we do have something that looks like a full Glivenko’s first theorem! But we know that Glivenko’s first theorem does not extend to universal formulas! What’s the trick here?
In order to understand the real meaning of the Glivenko-type of results we can prove in \(\mathsf{ECI}\) we will have a look at some relations between the behavior of the classical operator \(\forall_{c}\) and the behavior of the label/constant \(c\) applied to a universal formula.
We can emulate an application of the \(I_{c}\) rule of \(\mathsf{ECI}\) with conclusion \(\forall_{c} xA(x)\) by an application of the \(\forall_{c}\)-Introduction rule in \(\mathsf{NE_{K}}\), as well as an application of the \(\forall_{c}\)-elim rule by an application of the \(E_{c}\) rule of \(\mathsf{ECI}\).
Theorem 8. The following hold:
If \(\neg \forall x A(x) \vdash_{\mathsf{NE_{K}}} \bot\) then \(\vdash_{\mathsf{NE_{K}}} \forall_{c}x A(x)\)
If \(\vdash_{\mathsf{ECI}} (\forall x A(x))^{c}\) then \(\vdash_{\mathsf{ECI}} \neg \neg A(t/x)\).
Proof. We can construct the following derivation in \(\mathsf{NE_{K}}\):
We can also construct the following derivation in \(\mathsf{ECI}\):
◻
But we cannot emulate the rule \(E_{c}\) of \(\mathsf{ECI}\) by means of the rule \(\forall_{c}\)-elim, and the rule \(\forall_{c}\)-int by means of the rule \(I_{c}\) of \(\mathsf{ECI}\), and this means that the deductive behavior of the classical operator is different from the deductive behavior of the labeled formula. In a certain sense, a formula \(\forall_{c} xA(x)\) can be interpreted as \(\neg \exists x\neg A(x)\), whereas a formula \((\forall xA(x))^{c}\) can be interpreted as \(\neg \neg \forall xA(x)\) (see the translation \(t\mathsf{ECI}\) in Definition 1), and these interpretations are not intuitionistically equivalent! This peculiar behaviour is only observed in the universal quantifier, which is entirely expected because Glivenko’s theorems hold for the \(\forall\)-free fragments of \(\mathsf{CL}\) and \(\mathsf{IL}\). And now it is possible to explain in which sense the Glivenko-type results are trivial in \(\mathsf{ECI}\): what the theorem \(A^{c} \vdash_{\mathsf{ECI}} \neg \neg A^{i}\) says can be interpreted simply as \(\neg \neg A \vdash_{\mathsf{ECI}} \neg \neg A\), and in the particular case of universal formulas, as \(\neg \neg \forall xA(x) \vdash_{\mathsf{ECI}} \neg \neg \forall xA(x)\). Mystery solved!
Natural deduction allows us to fix the meaning of a logical connective by specifying the rules governing its use. The non-interdefinability of intuitionistic operators makes it so that intuitionistic specifications are expected to be independent of each other, but the same does not hold for classical specifications due to the similarity of grounds for classical use. Consequently, classical logic can be obtained by adding to intuitionistic logic autonomous rules permitting the use of classical proof principles (such as the classical reductio), which modify the meaning of connectives by uniformly supplying them with indirect (classical) means of proof. As such, to obtain classical logic from intuitionistic logic it suffices to change the notion of proof by adding a rule which allows classical reasoning.
From a different perspective, it could be argued that the possibility of defining an autonomous classical rule is a byproduct of the uniformity of changes in the meaning of connectives, but this does not imply the existence of a change in the concept of proof. The classical grounds for use must be included in the individual definition of each connective, but since they must be included in every connective it is also possible to implement this through the definition of a single autonomous rule. This means that classical proof rules are merely technical tools for changing the definition of all connectives at once, but that a conceptually faithful classical definition would have to include classical grounds for use directly into each of the introduction and elimination rules for operators instead.
The differences between \(\mathsf{ECI}\)-type systems and Prawitz-type systems (which includes \(\mathsf{NE}\) and \(\mathsf{NE_{K}}\)) seem to be explained by the differences between both perspectives. In the first one, just like in \(\mathsf{ECI}\), the change operates at the level of proofs, so classical connectives are obtained by equipping intuitionistic logic with classical means of proof that indirectly change the meaning of connectives when used. In the second one, just like in \(\mathsf{NE}\) and \(\mathsf{NE_{K}}\), the changes are made directly at the level of connectives, so we only have one notion of proof but are now allowed to use it together with connectives that are explicitly defined in terms of classical grounds for use. The difference is subtle but, as our study shows, not without consequence. In particular, the principles of each path lead us to distinct versions of logical ecumenism.
In a certain sense, we can summarize the differences between both approaches in the following way: while Prawitz’s and Krauss’ systems have actual classical operators, the system \(\mathsf{ECI}\) distinguish by means of the constant \(c\) a classical behavior from an intuitionistic behavior of the same operator (remember that in \(\mathsf{ECI}\) we have just one set of logical operators and formulas can be labeled with the constant \(c\) to indicate this classical behavior). If we restrict the two approaches to the propositional or \(\forall\)-free fragment, it is indifferent whether we use \(\mathsf{ECI}\) or \(\mathsf{NE_{K}}\). But this is not true when we add the universal quantifier, and the question now of which approach corresponds more faithfully to a classical universal quantifier is everything but negligible.
First of all, we would like to thank Marcelo Coniglio for being such an inspiration and a good friend.
Barroso-Nascimento was supported in part by the Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Brasil (CAPES) - Finance Code 001. Pereira is supported by the following projects: CAPES/COFECUB 88881.878969/2023-01, CNPq-313400/2021-0, and CNPq-Gaps and Gluts. Pimentel has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant agreement Number 101007627. Pimentel and Barroso-Nascimento are supported by the Leverhulme Trust grant RPG-2024-196.
This work has benefitted from Dagstuhl Seminar 24341 “Proof Representations: From Theory to Applications.”
The authors are grateful for the useful suggestions from the anonymous referee.
See [4], [5] for illuminating presentations and discussions of these translations, as well as their relation to two other translations due to Kuroda and Krivine [6], [7].↩︎
It is both interesting and important to observe (although it has not been frequently noted!) that when an intuitionistic logician proves, for example, \(\neg \neg (A \vee B)\) while a classical logician proves \((A \vee B)\), the connective \(\vee\) in \(\neg \neg (A \vee B)\) does not carry the same meaning as the connective \(\vee\) in \((A \vee B)\). The proof of \(\neg \neg (A \vee B)\) belongs to the intuitionistic system and, although we use the same symbol \(\vee\), within that system it has an intuitionistic interpretation rather than a classical one. The same observation applies to the familiar double-negation translations: the operators in the image-language inherit their meaning from the semantics of the image-language. This general point motivates the practice of distinguishing between classical and intuitionistic operators by means of different symbols, as is done in ecumenical systems. For instance, in Prawitz’s ecumenical system one finds both a classical disjunction \(\vee_{c}\) and an intuitionistic disjunction \(\vee_{i}\).↩︎
For an insightful presentation and discussion of Seldin’s normalization strategy, see [9].↩︎
An abstract study of non-collapsing combinations of logics can be found in [15].↩︎
From a semantic perspective, this can be done either by defining clauses for operators of stronger logics in a semantic framework for the weaker logic [16] or by also defining distinct semantic notions that co-exist peacefully [17].↩︎
For reasons discussed in the last section of this paper and pointed out by Luiz Carlos Pereira in other contexts, using “inferentialist" and”generalist" to refer to the two approaches is rather misleading.↩︎
For easing the notation, we will omit the superscript of the intuitionistic formulas, marking only the classical ones.↩︎
The system \(\mathsf{ECI}\) is defined over a language that does not have any explicit sign that would mark a formula as being intuitionistic. It is implicit that if the formula is not labeled with the sign/constant \(c\), then it is an intuitionistic formula. A formula without any occurrence of the label \(c\) is a full intuitionistic formula.↩︎
It is interesting to observe that \((\neg A)^{c} \dashv \vdash_{\mathsf{ECI}} \neg (A^{c})\).↩︎
Krauss obtains this system by first defining an ecumenical system for \(\mathsf{CL}\) and minimal logic (\(\mathsf{ML}\)), then extending it to a system for \(\mathsf{IL}\) and \(\mathsf{CL}\) by adding the rule \(\bot\)-elim. He proceeds to prove results for both ecumenical systems. Two ecumenical systems containing rules for \(\mathsf{IL}\) and \(\mathsf{ML}\) are presented by Barroso-Nascimento in [18], one defining rules for operators (as in \(\mathsf{NE}\)) and one defining rules for formulas (as in \(\mathsf{ECI}\)).↩︎
Although he accepts the existence of two conjunctions, Krauss claims that the classical mathematician seldom uses the classical one. In fact, he observes that the classical conjunction is not idempotent: from a proof of \(A \wedge_c A\) one can derive only \(\neg\neg A\), which always entails \(A\) in classical logic, but not in the ecumenical setting.↩︎
We observe that the idea of having two conjunctions appears in several works, such as Girard’s Constructive Classical Logic [20], Liang and Miller’s focused systems [21], as well as in ecumenical approaches to automated deduction [22].↩︎