A Unifying Conservation Theorem

Fellin, Giulio

doi:10.4230/LIPIcs.CSL.2026.19

A Unifying Conservation Theorem

Giulio Fellin

Università degli Studi di Verona, Italy

Abstract

The relationship between classical and constructive logics has long been illuminated by a series of conservation results, beginning with Kolmogorov’s negative translation and Glivenko’s double negation theorem, and later extended by Kuroda and Segerberg to first-order and minimal logics respectively. These results reveal how certain classical principles can be interpreted or recovered within weaker constructive frameworks, either via translations or through minimal extensions that satisfy specific logical properties. In this paper, we propose a unifying generalisation of these conservation theorems, that consolidates and expands the abstract methods introduced in earlier studies, offering a unified perspective on the interplay between classical provability and constructive reasoning.

Keywords and phrases:

double negation, negative translation, conservation, minimal logic, Glivenko’s theorem

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Proof theory

Acknowledgements:

The author wishes to thank Thorsten Altenkirch, Norbert Gratzl, Edi Pavlović, and Peter Schuster for their interest and valuable suggestions. The author is a member of the “Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni” (GNSAGA) of the Istituto Nazionale di Alta Matematica (INdAM).

DOI:

10.4230/LIPIcs.CSL.2026.19

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Dedicated to the memory of Krister Segerberg (1936–2025)
and to the 100th anniversary of Kolmogorov’s negative translation

1 Introduction

The relationship between classical and constructive logics has long been a central topic in proof theory and the philosophy of mathematics. Various syntactic translations and logical extensions have been developed to reconcile classical reasoning with constructive principles, leading to a rich body of conservation theorems that clarify how much of classical logic can be recovered within weaker, constructive systems. These conservation results typically rely on the mechanism of double negation.

Negative translations have already been studied in the context of nuclei [48, 8] (see Section 3.1), and have also proved useful in computer science [21], set theory [1], arithmetic and analysis [44], ultimately contributing to applications like program extraction [40] and proof mining [26]. Double negation over intuitionistic logic itself is a standard example of a nucleus [2, 22, 25, 30, 39, 42, 43, 48]. Building on this observation, significant generalisations of Glivenko’s theorem [18] were established in [12, 13, 10, 14], extending beyond propositional logic to arbitrary sets equipped with consequence relations and replacing double negation with arbitrary nuclei. These results subsume, as special cases, the classical theorems of Segerberg [41] and Kuroda [28], which concern the weakest extensions of minimal propositional and intuitionistic predicate logic satisfying conservation. In [11], this approach was further extended to the theory of negative translations, providing a unified framework that encompasses both Glivenko’s theorem and the classical negative translation results [47, 46, 15, 7] by Kolmogorov [27], Gödel [19], Gentzen [16], and Kuroda [28]. However, these two lines of generalisation remained separate in those earlier works.

The main contribution of the present article is to further generalise these results in two key directions. First, the new approach simultaneously treats both the case of moving to an extension of a logic (as in Segerberg’s claim and Kuroda’s use of the double negation shift) and the case of applying a translation (as in the negative translations of Kolmogorov and Kuroda). This unification broadens the applicability of the main theorem (Theorem 6) and deepens our understanding of the interaction between classical and constructive logics under various structural transformations. Second, unlike in the previous formulations [13, 11], we do not assume that the function under consideration is a nucleus from the outset. Rather, it suffices for it to behave as a nucleus only within the Glivenko extension itself, affording greater flexibility and generality in the construction.¹¹1A comparison with [10] is necessary here, since that work established that being a nucleus is both a necessary and sufficient condition for conservation, which may initially seem to conflict with the present results. However, the earlier paper focused exclusively on the case without extensions, corresponding precisely to our Corollary 14.

In addition to this general conceptual unification, we show that several classical conservation results – such as those of Kolmogorov, Segerberg, and others – can be derived as particular instances of our main theorem, in suitably generalised forms. Furthermore, we apply the framework, and in particular its novel capacity to handle extensions and translations simultaneously, to characterise the least logic for which Kuroda’s double negation theorem holds, thereby clarifying the logical strength required for this form of translation.

Thus, this work not only consolidates and extends the abstract framework introduced earlier but also provides a unified treatment that captures both extensions and translations of logical systems within a single, comprehensive setting.

2 A brief account of conservation results

Classical logic adheres to the principles of the excluded middle and explosion. The former asserts that every proposition must be either true or false ( $\varphi\vee\neg\varphi$ ), while the latter states that from a contradiction, any proposition can be derived ( $\bot\to\varphi$ ). In the early 20th century, L. E. J. Brouwer [5, 6] criticised the principle of the excluded middle for its nonconstructive nature: showing that the nonexistence of an object leads to a contradiction allows one to conclude that the object exists, without explicitly constructing it. Rejecting the principle of excluded middle, Brouwer introduced intuitionistic logic, later formalised by Kolmogorov [27], Glivenko [17, 18], and Heyting [23]. Intuitionistic logic satisfies two key properties: the existential property (if there exists an object satisfying a certain property, then we can explicitly provide a witness) and the disjunction property (if a disjunction $\varphi\vee\psi$ is provable, then either $\varphi$ is provable or $\psi$ is provable).

2.1 Kolmogorov

In 1925, Andrey Kolmogorov published a seminal paper [27] aimed at clarifying the logical foundations of intuitionism. Kolmogorov accepted the intuitionist critique of classical logic, especially the rejection of the principle of the excluded middle. However, he went further by also rejecting the principle of explosion, arguing that it lacks constructive meaning. His reasoning was that deriving an arbitrary conclusion from a contradiction does not correspond to constructing a proof of that conclusion, and hence explosion is epistemically and constructively illegitimate. Kolmogorov described this more restricted logical system as intuitionistic logic, but today it is known as minimal logic – a term introduced by Ingebrigt Johansson in 1937 [24], likely independently of Kolmogorov’s earlier work.

Kolmogorov then introduced a key syntactic technique, now called the Kolmogorov negative translation, which provides a faithful embedding of classical logic into minimal logic. This translation $K$ recursively transforms any formula $\varphi$ by double negating atomic formulae and systematically wrapping all logical connectives and quantifiers in double negations. By adopting more modern conventions, we can write it as follows:

$\displaystyle K(\varphi)$	$\displaystyle:\equiv\neg\neg\varphi,$	$\displaystyle\text{if }\varphi\text{ atomic},$
$\displaystyle K(\varphi_{1}*\varphi_{2})$	$\displaystyle:\equiv\neg\neg(K(\varphi_{1})*K(\varphi_{2})),$	$\displaystyle\text{if }*\in\{\wedge,\vee,\to\},$
$\displaystyle K(\mathsf{Q}x\,\varphi)$	$\displaystyle:\equiv\neg\neg\mathsf{Q}x\,K(\varphi),$	$\displaystyle\text{if }\mathsf{Q}\in\{\forall,\exists\}.$

Kolmogorov’s negative translation theorem asserts that $\varphi$ and $K(\varphi)$ are classically equivalent, and that $\varphi$ is provable in classical logic if and only if $K(\varphi)$ is provable in minimal logic.

Kolmogorov viewed minimal logic as the true logic of mathematical construction, while classical principles like excluded middle and explosion correspond to what he called pseudotruths: a formula $\varphi$ is a pseudotruth if its translation $K(\varphi)$ is provable in minimal logic. These pseudotruths behave like truths within classical reasoning but do not reflect genuine constructive knowledge. According to Kolmogorov, the reason classical reasoning avoids contradictions is that it operates on pseudotruths rather than actual constructive proofs. This radical yet elegant perspective anticipated much later developments in proof theory, realisability, and constructive mathematics.

2.2 Glivenko

In 1928–1929, Valery Glivenko published two brief but influential notes [17, 18], written largely in response to criticisms directed at intuitionistic logic by Marcel Barzin and Alfred Errera [4]. Barzin and Errera had misunderstood Brouwer’s position, suggesting that intuitionism implied the existence of a “third” truth value – something neither true nor false – for statements whose truth had not yet been established.²²2For a more detailed history of the Barzin–Errera controversy, we refer to [45].

Glivenko set out to clarify this misconception and, in doing so, gave the first formal presentation of intuitionistic logic that included the principle of explosion. He proved that the principle of excluded middle, $\varphi\vee\neg\varphi$ , is not refutable in intuitionistic logic; indeed, one can prove $\neg\neg(\varphi\vee\neg\varphi)$ . This shows that intuitionism does not deny the excluded middle outright, but merely refuses to assert it in the absence of a constructive proof. In this sense, the law of excluded middle behaves like the parallel postulate in geometry: it is independent of the other axioms, neither provable nor disprovable without additional assumptions. Thus, Glivenko’s analysis refuted the idea that intuitionistic logic admits a “third” logical value.

In the course of this work, Glivenko also established two results that would later be known collectively as Glivenko’s theorem. First, he showed that if a propositional formula is provable in classical logic, then its double negation is provable in intuitionistic logic. Second, he proved that a negated propositional formula is intuitionistically provable if and only if it is classically provable.

2.3 Gödel and Gentzen

In 1933, Kurt Gödel and Gerhard Gentzen independently introduced negative translations embedding classical arithmetic into intuitionistic arithmetic [19, 16], apparently unaware of Kolmogorov’s earlier work. Although Gentzen completed his manuscript that same year, he withdrew it during the galley proof stage upon learning of Gödel’s result. Gentzen’s translation $G$ inserts double negations in front of atomic formulae, disjunctions, and existential quantifiers, and just propagates through the other constructions, i.e.,

$\displaystyle G(\varphi)$	$\displaystyle:\equiv\neg\neg\varphi,$	$\displaystyle\text{if }\varphi\text{ atomic},$
$\displaystyle G(\varphi_{1}*\varphi_{2})$	$\displaystyle:\equiv G(\varphi_{1})*G(\varphi_{2}),$	$\displaystyle\text{if }*\in\{\wedge,\to\},$
$\displaystyle G(\varphi_{1}\vee\varphi_{2})$	$\displaystyle:\equiv\neg\neg(G(\varphi_{1})\vee G(\varphi_{2})),$
$\displaystyle G(\forall x\,\varphi)$	$\displaystyle:\equiv\forall x\,G(\varphi),$
$\displaystyle G(\exists x\,\varphi)$	$\displaystyle:\equiv\neg\neg\exists x\,G(\varphi).$

and behaves like Kolmogorov’s elsewhere. His negative translation theorem states that a formula $\varphi$ is classically provable if and only if $G(\varphi)$ is provable in intuitionistic logic, and that $\varphi$ and $G(\varphi)$ are classically equivalent. Gödel’s variant $G^{\prime}$ placed double negation also in front of implications:

G^{\prime}(\varphi_{1}\to\varphi_{2}):\equiv\neg\neg(G^{\prime}(\varphi_{1})% \to G^{\prime}(\varphi_{2})),

thus occupying a middle ground between Kolmogorov’s and Gentzen’s schemes. His result asserts that $\varphi$ is provable classically if and only if $G(\varphi)$ is provable in intuitionistic logic. Although Gödel’s and Gentzen’s translations are distinct in their original form, they are often conflated under the term Gödel–Gentzen negative translation [46, 15], typically referring to Gentzen’s version. It is also well known that, over minimal logic, the translations $K$ , $G$ , and $G^{\prime}$ are pairwise equivalent [15]: for every formula $\varphi$ , we have $\vdash\;K(\varphi)\;\leftrightarrow\;G(\varphi)\;\leftrightarrow\;G^{\prime}(% \varphi).$

Moreover, an important contribution of both Gödel and Gentzen is that their negative translations extend beyond logic to full arithmetic. In fact, already Kolmogorov had recognised the possibility of applying this approach to mathematical theories, not just logical formulae, thereby laying the groundwork for later developments in constructive interpretations of classical mathematics.

2.4 Kuroda

In 1951, Sigekatu Kuroda published a summary [28] presenting results from his earlier Japanese works. Kuroda introduced a novel negative translation and used it to generalise Glivenko’s theorem from propositional to first-order predicate logic. He observed that Glivenko’s original double negation result holds in predicate logic only for formulae free of universal quantifiers, but more generally, one obtains a conservation result by applying a translation now known as the Kuroda negative translation. This translation inserts double negations not only in front of the whole formula but also inside every occurrence of the universal quantifier within it. More precisely, we can write Kuroda’s negative translation as $\neg\neg J$ , where $J$ is defined as:

$\displaystyle J(\varphi)$	$\displaystyle:\equiv\varphi,$	$\displaystyle\text{if }\varphi\text{ atomic},$
$\displaystyle J(\varphi_{1}*\varphi_{2})$	$\displaystyle:\equiv J(\varphi_{1})*J(\varphi_{2}),$	$\displaystyle\text{if }*\in\{\wedge,\vee,\to\},$
$\displaystyle J(\exists x\,\varphi)$	$\displaystyle:\equiv\exists x\,J(\varphi),$
$\displaystyle J(\forall x\,\varphi)$	$\displaystyle:\equiv\forall x\,\neg\neg J(\varphi).$

Similar to Kolmogorov’s, Kuroda’s Negative Translation Theorem asserts that $\varphi$ and $\neg\neg J(\varphi)$ are classically equivalent, and that $\varphi$ is provable in classical logic if and only if $\neg\neg J(\varphi)$ is provable in intuitionistic logic.³³3Unlike Kolmogorov’s translation, Kuroda’s original translation does not apply to minimal logic. A modified version suitable for minimal logic was introduced by Chetan Murthy in 1990 [29] and is sometimes referred to as the minimal Kuroda negative translation [48, 15].

Kuroda further isolated a key principle needed to lift Glivenko’s result to the predicate level: the double negation shift for universal quantification, $\forall x\,\neg\neg\varphi(x)\ \to\ \neg\neg\forall x\,\varphi(x),$ a principle that intuitionistic predicate logic does not validate. Assuming this shift, he showed that classical provability of a formula entails the intuitionistic provability of its ordinary double negation – that is, of the same $\neg\neg$ -translation used in Glivenko’s original theorem and not Kuroda’s own $\neg\neg J(\varphi)$ . In Kuroda’s terminology, a formula is then “free of contradiction” exactly when its double negation is intuitionistically derivable, echoing Kolmogorov’s notion of pseudotruth.

2.5 Segerberg

In 1968, Krister Segerberg [41] introduced what is now called Glivenko’s logic, originally denoted $JP^{\prime}$ . He defined it as minimal propositional logic extended by the double negation of the principle of explosion, $\neg\neg(\bot\to\varphi)$ . Segerberg also asserted⁴⁴4Segerberg did not provide a proof or citation for this claim. A rigorous proof was given only decades later by Odintsov [35]. that $JP^{\prime}$ is the weakest logic $\mathbf{L}$ satisfying Glivenko’s theorem: a formula $\varphi$ is provable in classical logic if and only if $\neg\neg\varphi$ is provable in $\mathbf{L}$ . This establishes Glivenko’s logic as a foundational system with distinctive structural properties.

The Glivenko logic offers a novel treatment of falsity and negation, presenting a compromise between intuitionistic logic and minimal logic. It rejects the principle of explosion, aligning with the constructive nature of minimal logic, while simultaneously refusing to outright negate the principle whenever falsity is unprovable. This ensures weak but crucial consistency: not everything becomes provable. As such, the Glivenko logic strikes a balance that is both philosophically compelling and potentially foundational for alternative reasoning frameworks.

The characterisation of the Glivenko logic as the weakest logic satisfying Glivenko’s theorem underscores its remarkable strength. By enabling classical reasoning to operate under specific constraints, particularly in proofs of negated formulae, it provides a refined framework for integrating classical and constructive methods. This duality enhances its philosophical and technical relevance.

After its introduction in 1968, the Glivenko logic received limited attention. Beyond Segerberg’s foundational paper, only two brief notes in the early 1970s [49, 20] touched upon the topic, after which it vanished from the literature for nearly three decades, until it was revived by Odintsov, mainly for technical purposes [35].

The study of the Glivenko logic becomes significantly more intricate when extended to predicate logic. Combining insights from Kuroda and Segerberg shows that, to obtain the Glivenko predicate logic – the minimal extension of minimal predicate logic for which Glivenko’s theorem holds – one must incorporate both the double negation of explosion and the double negation shift. As a result, this logic is incomparable with intuitionistic predicate logic: it is neither weaker nor stronger, but rather a distinct intermediate logic lying strictly between minimal and classical predicate logics [3].

3 Entailment relations

Let $S$ be a set and $\operatorname{Fin}(S)$ be the set of finite subsets of $S$ . Intuitively, the elements of $S$ are formula-like objects. By “ $U\rhd b$ ” we mean the element $(U,b)$ of $\operatorname{Fin}(S)\times S$ . Given $\text{$\mathbf{L}$}\subseteq\operatorname{Fin}(S)\times S$ , we write “ $\text{$\mathbf{L}$}\vdash U\rhd b$ ” in place of $(U,b)\in\text{$\mathbf{L}$}$ . We often omit “ $\text{$\mathbf{L}$}\vdash$ ” if it is clear from the context.

A (single-conclusion) entailment relation is a relation $\text{$\mathbf{L}$}\subseteq\operatorname{Fin}(S)\times S$ such that

where the comma “,” is used as a shorthand for union, and a lowercase letter on the left-hand side represents a singleton. These three are the structural rules of reflexivity, monotonicity (or weakening) and transitivity (or cut), respectively. Using finite sets as contexts, also gives us contraction for free.

Quite often an entailment relation $\mathbf{L}$ is inductively generated from a given set $\mathcal{R}$ of rules by closing up with respect to the structural rules above. These non-structural rules have the form

for a finite or countable $I$ . Countable premisses are required, for example, when working with infinitary logic [3, 10, 11]. We call axioms the rules with no premiss, i.e. of the form

If $\mathbf{L}$ is inductively generated by a set $\mathcal{R}$ of rules, we write $\text{$\mathbf{L}$}=\langle\mathcal{R}\rangle$ .

By an extension ${\text{$\mathbf{L}$}^{\prime}}$ of an entailment relation $\mathbf{L}$ we mean an entailment relation such that ${\text{$\mathbf{L}$}}\subseteq{\text{$\mathbf{L}$}^{\prime}}$ . If $\text{$\mathbf{L}$}=\langle\mathcal{R}\rangle$ and $\text{$\mathbf{L}$}^{\prime}=\langle\mathcal{R},\mathcal{R}^{\prime}\rangle$ , we say that $\text{$\mathbf{L}$}^{\prime}$ is an inductive extension of $\mathbf{L}$ .

3.1 Properties of functions

Throughout this subsection, let $\mathbf{L}$ be an entailment relation on $S$ . In particular, the structural rules of reflexivity, monotonicity and transitivity are always assumed.

Let $f\colon S\to S$ be a function (intuitively represents a formula translation) and let $m\in\mathbb{N}$ . Consider the properties and their rule correspondents presented in Figure 1.

Table 1: Properties of functions.

Property

Rule

Equivalent axiom

idempotency

f^{2}(a)\rhd f(a)

progressive

monotonicity

(none)

stability

f(a)\rhd a

inflationarity

f(a)\rhd f^{2}(a)

expansivity

a\rhd f(a)

Each property, except progressive monotonicity, can be formalised as a rule, or equivalently as an axiom.⁵⁵5The conversion is carried out following the method outlined in [34, §6.3]. This is crucial: if any of these properties holds in $\mathbf{L}$ , then it is preserved in every inductive extension $\text{$\mathbf{L}$}^{\prime}$ of $\mathbf{L}$ , since derivability of the corresponding axiom is inherited by inductive extensions. In contrast, progressive monotonicity corresponds to a non-axiomatic rule; in particular, it is not automatically inherited by every inductive extension in the present setting [10].

$\blacktriangleright$ Remark 1.

It is immediate to see that:

1.

stability $\Rightarrow$ progressive monotonicity $\Rightarrow$ idempotency,
2.

expansivity $\Rightarrow$ inflationarity.

Given a rule

we define its Glivenko $f$ -variant $r_{f}$ by putting $f$ in front of every consequent, and its Kolmogorov $f, m$ -variant $r_{f}^{m}$ by putting $f^{m}$ in front of every element:

where $f^{m}U:=\{f^{m}(b)\colon b\in U\}$ . If $m=1$ , then we just call it the Kolmogorov $f$ -variant. Given a set of rules $\mathcal{R}$ , we use the obvious notations $\mathcal{R}_{f}:=\{r_{f}\colon r\in\mathcal{R}\}$ and $\mathcal{R}_{f}^{m}:=\{r_{f}^{m}\colon r\in\mathcal{R}\}$ .

If $\text{$\mathbf{L}$}=\langle\mathcal{R}\rangle$ , we define

$\blacksquare$

its Kleisli $f$ -extension $\operatorname{Kleisli}_{f}(\text{$\mathbf{L}$})$ by

$\displaystyle\operatorname{Kleisli}_{f}(\text{$\mathbf{L}$}):=\{(U,a)\colon% \text{$\mathbf{L}$}\vdash U\rhd f(a)\},$
$\blacksquare$

its $f, m$ -lifting $\operatorname{Lift}_{f}^{m}$ by

$\displaystyle\operatorname{Lift}_{f}^{m}(\text{$\mathbf{L}$}):=\{(U,a)\colon% \text{$\mathbf{L}$}\vdash f^{m}(U)\rhd f^{m}(a)\},$
$\blacksquare$

its Glivenko $f$ -extension $\operatorname{Gliv}_{f}(\text{$\mathbf{L}$})$ as

$\displaystyle\operatorname{Gliv}_{f}(\text{$\mathbf{L}$}):=\langle\mathcal{R},% \mathcal{R}_{f},\textnormal{L$f$},\textnormal{R$f$}\rangle,$
$\blacksquare$

its Kolmogorov $f, m$ -extension $\operatorname{Kol}_{f}^{m}$ as

$\displaystyle\operatorname{Kol}_{f}^{m}(\text{$\mathbf{L}$}):=\langle\mathcal{% R},\mathcal{R}_{f}^{m},\textnormal{L$f$}^{-},\textnormal{R$f$}^{-}\rangle,$
$\blacksquare$

its stable (or maximum) $f$ -extension $\operatorname{Max}_{f}(\text{$\mathbf{L}$})$ as

$\displaystyle\operatorname{Max}_{f}(\text{$\mathbf{L}$}):=\langle\mathcal{R},% \textnormal{L$f$}^{+},\textnormal{R$f$}\rangle.$

It is clear by definition that $\operatorname{Gliv}_{f}(\text{$\mathbf{L}$})$ , $\operatorname{Kol}_{f}^{m}(\text{$\mathbf{L}$})$ , and $\operatorname{Max}_{f}(\text{$\mathbf{L}$})$ are inductive extensions of $\mathbf{L}$ , while $\operatorname{Kleisli}_{f}(\text{$\mathbf{L}$})$ and $\operatorname{Lift}_{f}^{m}(\text{$\mathbf{L}$})$ are not.

These new structures are defined using the set of generating rules $\mathcal{R}$ of the original structure. However, they are in fact independent of the particular choice of generating rules. Indeed, it is straightforward to show that if a rule $r$ is derivable from $\mathcal{R}$ , then its variant $r_{f}$ is derivable from $\mathcal{R}_{f}\cup\{\mathrm{L}f,\mathrm{R}f\}$ and its variant $r_{f}^{m}$ is derivable from $\mathcal{R}_{f}^{m}$ .

Lemma 2.

Let $\text{$\mathbf{L}$}:=\langle\mathcal{R}\rangle$ . For every $r\in\mathcal{R}$ and every $m\in\mathbb{N}$ , the rule $r_{f}^{m}$ is admissible in $\operatorname{Lift}_{f}^{1}\operatorname{Kol}_{f}^{1}(\text{$\mathbf{L}$})$ .

Proof.

By definition of $\operatorname{Lift}_{f}^{1}\operatorname{Kol}_{f}^{1}(\text{$\mathbf{L}$})$ , we have that $r_{f}^{m}$ is admissible in $\operatorname{Lift}_{f}^{1}\operatorname{Kol}_{f}^{1}(\text{$\mathbf{L}$})$ if and only if $r_{f}^{m+1}$ is admissible in $\operatorname{Kol}_{f}^{1}(\text{$\mathbf{L}$})$ . By a straightforward proof by induction using L $f$ ^- and R $f$ ^-, the latter condition is show to be equivalent to admissibility of $r^{1}_{f}$ in $\operatorname{Kol}_{f}^{1}(\text{$\mathbf{L}$})$ , which holds by definition. $\hfill\blacktriangleleft$

Now consider two functions $j,k\colon S\rightarrow S$ . We say that

$\blacksquare$

$j$ is a nucleus in $\mathbf{L}$ if it is expansive and progressively monotone in $\mathbf{L}$ .
$\blacksquare$

$j$ is a stable nucleus in $\mathbf{L}$ if it is expansive and stable in $\mathbf{L}$ .
$\blacksquare$
$k$ is $j$ -homogeneous in $\mathbf{L}$ if
1. 1.
  
  $k$ is a nucleus in $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ , and
2. 2.
  
  $j$ is a stable nucleus in $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$})$ ;
$\blacksquare$
$k$ is a $j$ -translation from $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ to $\mathbf{L}$ if
1. 1.
  
  $k$ is a nucleus in $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ , and
2. 2.
  
  $\operatorname{Max}_{j}(\text{$\mathbf{L}$})\subseteq\operatorname{Lift}_{k}^{1% }(\text{$\mathbf{L}$})$ .

$\blacktriangleright$ Remark 3.

It is immediate to see that:

1.

Every function $j$ is a nucleus in $\operatorname{Gliv}_{j}(\text{$\mathbf{L}$})$ and a stable nucleus in $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ .
2.

If $j$ is a stable nucleus in $\mathbf{L}$ , then it is a nucleus in $\mathbf{L}$ .
3.

If $k$ is a $j$ -translation from $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ to $\mathbf{L}$ , then it is $j$ -homogeneous in $\mathbf{L}$ .

3.2 Minimal logic

Our motivational example is minimal predicate logic $\mathbf{Min}$ , which is an entailment relation on the set $\operatorname{Frm}$ of formulae in the first-order predicate language. To distinguish it from the general abstract case, we use lowercase Greek letters for formulae and uppercase Greek letters for sets of formulae. Its set $\mathcal{M}$ of generating rules is shown in Figure 1.

Figure 1: The set

\mathcal{M}

of rules generating

\mathbf{Min}

.

We then have the constant $\bot$ , which has no rule, and we introduce the abbreviation:

\neg\varphi:\equiv\varphi\to\bot.

Upon minimal logic, we construct

$\blacksquare$

intuitionistic predicate logic $\mathbf{Int}$ by adding the following to the set of generating rules:
$\blacksquare$

the Glivenko predicate logic $\mathbf{Gli}$ by adding the following to the set of generating rules:
$\blacksquare$

classical predicate logic $\mathbf{Cla}$ by adding the following to the set of generating rules:

It is clear that the stable $\neg\neg$ -extension of $\mathbf{Min}$ is just classical predicate logic $\mathbf{Cla}$ .

By the propositional fragment of a logic, we mean the subsystem obtained by omitting all quantifiers and the corresponding inference rules from its predicate version.

The main example – and our motivating example – of a nucleus in $\mathbf{Min}$ is double negation $\neg\neg$ , also known as the Glivenko nucleus [15, 48, 13, 11]. The proof that $\neg\neg$ forms a nucleus is straightforward and well-known, so we omit it. Consequently, we can freely use the rules L $\neg\neg$ and R $\neg\neg$ in $\mathbf{Min}$ .

Let us recall the following lemma, which will be useful later:

Lemma 4.

Over $\mathbf{Min}$ , DNX is equivalent to either of the following two formulations of DNS_→:

\displaystyle\varphi\to\neg\neg\psi

\displaystyle\rhd\neg\neg(\varphi\to\psi),

\displaystyle\text{or, equivalently},

\displaystyle\neg\neg\varphi\to\neg\neg\psi

\displaystyle\rhd\neg\neg(\varphi\to\psi).

Proof.

This fact is known in the literature. For the sake of completeness, we include a proof in Appendix A. $\hfill\blacktriangleleft$

4 Conservation

Proposition 5.

Let $\text{$\mathbf{L}$}:=\langle\mathcal{R}\rangle$ , $j\colon S\rightarrow S$ , $\text{$\mathbf{L}$}^{\prime}:=\langle\mathcal{R},\mathcal{R}^{\prime}\rangle$ such that all rules in $\mathcal{R}^{\prime}$ are derivable in $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ , and let $k\colon S\rightarrow S$ be $j$ -homogeneous in $\mathbf{L}$ . Then

1.

$\operatorname{Max}_{j}(\text{$\mathbf{L}$}^{\prime})=\operatorname{Max}_{j}(% \text{$\mathbf{L}$})$ .
2.

$k$ is $j$ -homogeneous in $\text{$\mathbf{L}$}^{\prime}$ .
3.

$\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})\subseteq% \operatorname{Max}_{j}(\text{$\mathbf{L}$})$ ;
4.

$\operatorname{Kleisli}_{j}(\text{$\mathbf{L}$}^{\prime})\subseteq\operatorname% {Max}_{j}(\text{$\mathbf{L}$})$ .

Proof.

1.

While $\operatorname{Max}_{j}(\text{$\mathbf{L}$}^{\prime})\supseteq\operatorname{Max% }_{j}(\text{$\mathbf{L}$})$ is trivial, we also have $\operatorname{Max}_{j}(\text{$\mathbf{L}$}^{\prime})\subseteq\operatorname{Max% }_{j}(\text{$\mathbf{L}$})$ since all rules in the inductive definition of $\operatorname{Max}_{j}(\text{$\mathbf{L}$}^{\prime})$ are derivable in $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ .
2.

Straightforward.
3.

We have:

where (*) denotes subsequent applications of Trans with multiple instances of expansivity and stability. This is justified by the fact that $j$ is a nucleus in $\operatorname{Max}_{j}(\text{$\mathbf{L}$}^{\prime})=\operatorname{Max}_{j}(% \text{$\mathbf{L}$})$ since $k$ is $j$ -homogeneous in $\text{$\mathbf{L}$}^{\prime}$ .
4.

Analogous.

$\hfill\blacktriangleleft$

Theorem 6 (Conservation).

Let $\text{$\mathbf{L}$}:=\langle\mathcal{R}\rangle$ , $j\colon S\rightarrow S$ , $\text{$\mathbf{L}$}^{\prime}:=\langle\mathcal{R},\mathcal{R}^{\prime}\rangle$ such that all rules in $\mathcal{R}^{\prime}$ are derivable in $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ , and let $k\colon S\rightarrow S$ be $j$ -homogeneous in $\mathbf{L}$ . Then the following are equivalent:

(a)

$\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})\supseteq% \operatorname{Max}_{j}(\text{$\mathbf{L}$})$ , i.e. $k$ is a $j$ -translation from $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ to $\text{$\mathbf{L}$}^{\prime}$ ;
(b)

all rules in $\mathcal{R}\cup\mathcal{R}^{\prime}$ are admissible in $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})$ ;
(c)

$\operatorname{Kol}_{k}^{1}(\text{$\mathbf{L}$})\subseteq\text{$\mathbf{L}$}^{\prime}$ .

Figure 2: The situation of Theorem 6.

Proof.

[(a) $\Rightarrow$ (b).]: By (a) and Proposition 5, we have $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})=\operatorname{Max}_{% j}(\text{$\mathbf{L}$})=\operatorname{Max}_{j}(\text{$\mathbf{L}$}^{\prime})$ . Then (c) directly follows from the definition of $\operatorname{Max}_{j}(\text{$\mathbf{L}$}^{\prime})$ .
[(b) $\Rightarrow$ (a).]: Suppose that $\operatorname{Max}_{j}(\text{$\mathbf{L}$})\vdash U\rhd b$ . We show that $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})\vdash U\rhd b$ by induction on the derivation of the former: the cases involving structural rules are trivial; the cases L $j$ ⁺ and R $j$ are tantamount to $j$ being a stable nucleus in $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})$ , which is the case since $k$ is $j$ -homogeneous in $\text{$\mathbf{L}$}^{\prime}$ ; lastly consider the case $r\in\mathcal{R}$
[(a)&(b) $\Rightarrow$ (c).]: We show that every rule generating $\operatorname{Kol}_{k}^{1}(\text{$\mathbf{L}$})$ is admissible in $\text{$\mathbf{L}$}^{\prime}$ : every $r\in\mathcal{R}$ is admissible in $\text{$\mathbf{L}$}^{\prime}$ by definition; by (b), we have that every $r\in\mathcal{R}$ is admissible in $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})$ , which means that $r_{k}^{1}$ is admissible in $\text{$\mathbf{L}$}^{\prime}$ ; (the axioms corresponding to) L $k$ ^- and R $k$ ^- are derivable in $\text{$\mathbf{L}$}^{\prime}$ as a direct consequence of the fact that $k$ is a nucleus in $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})$ by (a).
[(c) $\Rightarrow$ (a).]: By Lemma 2, condition (b) is fulfilled by $\operatorname{Kol}_{k}^{1}(\text{$\mathbf{L}$})$ when we take $\operatorname{Kol}_{k}^{1}(\text{$\mathbf{L}$})$ as the instance of $\text{$\mathbf{L}$}^{\prime}$ . We have already established (b) $\Rightarrow$ (a), which gives $\operatorname{Max}_{j}(\text{$\mathbf{L}$})\subseteq\operatorname{Lift}_{k}^{1% }(\operatorname{Kol}_{k}^{1}(\text{$\mathbf{L}$}))$ . On the other hand, from (c) we get $\operatorname{Lift}_{k}^{1}(\operatorname{Kol}_{k}^{1}(\text{$\mathbf{L}$}))% \subseteq\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$}^{\prime})$ . By transitivity of $\subseteq$ , we conclude $\operatorname{Max}_{j}(\text{$\mathbf{L}$})\subseteq\operatorname{Lift}_{k}^{1% }(\text{$\mathbf{L}$}^{\prime})$ .

$\hfill\blacktriangleleft$

The situation of this theorem is represented in Figure 2.

5 From the abstract to the concrete

We now show that generalised versions of all conservation results mentioned in Section 2 follow from our main theorem. Negative translation theorems – such as those by Kolmogorov, Gödel, Gentzen, and Kuroda – arise as direct applications of the main theorem in the special case where $\text{$\mathbf{L}$}=\text{$\mathbf{L}$}^{\prime}$ . Minimality theorems – such as those by Kuroda and Segerberg – correspond to the case where $k=j$ . Glivenko’s theorem emerges as the most constrained instance, where both $\text{$\mathbf{L}$}=\text{$\mathbf{L}$}^{\prime}$ and $k=j$ . Finally, we apply the full generality of our main theorem, without these simplifications, to refine Kuroda’s negative translation theorem by characterising the least logic for which it holds.

5.1 Translation theorems in the vein of Kolmogorov and Gentzen

Corollary 7.

Let $\text{$\mathbf{L}$}:=\langle\mathcal{R}\rangle$ and $j\colon S\rightarrow S$ . Now let $k\colon S\rightarrow S$ be $j$ -homogeneous. Then the following are equivalent:

(a)

$\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$})\supseteq\operatorname{Max}_{j% }(\text{$\mathbf{L}$})$ , i.e. $k$ is a $j$ -translation from $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ to $\mathbf{L}$ ;
(b)

all rules in $\mathcal{R}$ are admissible in $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{L}$})$ ;
(c)

$\operatorname{Kol}_{k}^{1}(\text{$\mathbf{L}$})\subseteq\text{$\mathbf{L}$}$ .

Proof.

This is just Theorem 6 with $\text{$\mathbf{L}$}=\text{$\mathbf{L}$}^{\prime}$ . $\hfill\blacktriangleleft$

This corollary is a version of [11, Theorem 3.13] that does not require $j$ to be a nucleus already in $\mathbf{L}$ , and it can be regarded as an abstract version of Kolmogorov’s negative translation theorem [27], as we are going to show. Proving Kolmogorov’s theorem from our general result requires only some technical checks – somewhat lengthy due to the number of cases in the inductive definitions involved, but conceptually straightforward.

Let us interpret $\mathbf{L}$ as minimal predicate logic $\mathbf{Min}$ , and let $j$ be double negation $\neg\neg$ . For $k$ , we consider two functions side by side: $K$ , corresponding to Kolmogorov’s negative translation, and $G$ , corresponding to Gentzen’s negative translation:

$\displaystyle K(\varphi)$	$\displaystyle:\equiv\neg\neg\varphi,$	$\displaystyle\quad G(\varphi)$	$\displaystyle:\equiv\neg\neg\varphi,$	$\displaystyle\text{if }\varphi\text{ atomic},$
$\displaystyle K(\varphi_{1}*\varphi_{2})$	$\displaystyle:\equiv\neg\neg\bigl(K(\varphi_{1})*K(\varphi_{2})\bigr),$	$\displaystyle G(\varphi_{1}*\varphi_{2})$	$\displaystyle:\equiv G(\varphi_{1})*G(\varphi_{2}),$	$\displaystyle\text{if }*\in\{\wedge,\to\},$
$\displaystyle K(\varphi_{1}\vee\varphi_{2})$	$\displaystyle:\equiv\neg\neg\bigl(K(\varphi_{1})\vee K(\varphi_{2})\bigr),$	$\displaystyle G(\varphi_{1}\vee\varphi_{2})$	$\displaystyle:\equiv\neg\neg\bigl(G(\varphi_{1})\vee G(\varphi_{2})\bigr),$
$\displaystyle K(\forall x\,\varphi)$	$\displaystyle:\equiv\neg\neg\forall x\,K(\varphi),$	$\displaystyle G(\forall x\,\varphi)$	$\displaystyle:\equiv\forall x\,G(\varphi),$
$\displaystyle K(\exists x\,\varphi)$	$\displaystyle:\equiv\neg\neg\exists x\,K(\varphi),$	$\displaystyle G(\exists x\,\varphi)$	$\displaystyle:\equiv\neg\neg\exists x\,G(\varphi).$

Lemma 8.

$K$ and $G$ are $\neg\neg$ -homogeneous in $\mathbf{Min}$ .

Proof.

It can be shown that $K$ and $G$ are nuclei in $\text{$\mathbf{Cla}$}=\operatorname{Max}_{\neg\neg}(\text{$\mathbf{Min}$})$ by an easy induction argument, using the fact that $\neg\neg$ is a stable nucleus in this extension and can therefore be “freely added and removed”.

We now need to show that $\neg\neg$ is a stable nucleus $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{Min}$})$ in both cases $k=K$ and $k=G$ . To do that, we prove by induction on the shape of $\varphi$ that $\operatorname{Lift}_{k}^{1}(\text{$\mathbf{Min}$})\vdash\neg\neg\varphi\rhd\varphi,$ which amounts to $\text{$\mathbf{Min}$}\vdash\neg\neg k(\varphi)\rhd k(\varphi)$ :

$\blacksquare$

If $k=K$ or $\varphi$ is either atomic, a disjunction, or existential, then $k(\varphi):\equiv\neg\neg\varphi^{\prime}$ for some $\varphi^{\prime}$ . This case then reduces to $\text{$\mathbf{Min}$}\vdash\neg\neg\neg\neg\varphi^{\prime}\rhd\neg\neg\varphi% ^{\prime},$ which is well-known.
$\blacksquare$

Suppose that $k=G$ and $\varphi:\equiv\alpha\wedge\beta$ . By the induction hypothesis, we have $\text{$\mathbf{Min}$}\vdash\neg\neg G(\alpha)\rhd G(\alpha)$ and $\text{$\mathbf{Min}$}\vdash\neg\neg G(\beta)\rhd G(\beta).$ From these, we get $\text{$\mathbf{Min}$}\vdash\neg\neg G(\alpha)\wedge\neg\neg G(\beta)\rhd G(% \alpha)\wedge G(\beta).$ Moreover, since $\text{$\mathbf{Min}$}\vdash\neg\neg(G(\alpha)\wedge G(\beta))\rhd\neg\neg G(% \alpha)\wedge\neg\neg G(\beta),$ by transitivity we obtain the desired conclusion.

The cases $\varphi:\equiv\alpha\to\beta$ and $\varphi:\equiv\forall x\,\alpha$ are handled in a similar manner by applying the induction hypothesis and standard properties of $\neg\neg$ .

$\hfill\blacktriangleleft$

Lemma 9.

$\operatorname{Kol}_{k}^{1}(\text{$\mathbf{Min}$})\subseteq\text{$\mathbf{Min}$}$ , where $k$ is either $K$ or $G$ .

Proof.

One needs to prove that all rules generating $\operatorname{Kol}_{k}^{1}(\text{$\mathbf{Min}$})$ are already admissible in $\mathbf{Min}$ . This is technical but straightforward; the details are provided in Appendix A. $\hfill\blacktriangleleft$

We can now retrieve Kolmogorov’s and Gentzen’s negative translation theorems. Gentzen originally proved that $G$ is a $\neg\neg$ -translation from $\mathbf{Cla}$ into $\mathbf{Int}$ . However, we can give a slightly stronger result, showing that it is also a $\neg\neg$ -translation from $\mathbf{Cla}$ into $\mathbf{Min}$ :

Proposition 10.

$\blacksquare$

Kolmogorov’s negative translation theorem [27]:

The function $K$ is a $\neg\neg$ -translation from $\mathbf{Cla}$ into $\mathbf{Min}$ .
$\blacksquare$

Gentzen’s negative translation theorem [16]:

The function $G$ is a $\neg\neg$ -translation from $\mathbf{Cla}$ into $\mathbf{Min}$ .

Proof.

Let $k$ be either $K$ or $G$ . Since $k$ is $\neg\neg$ -homogeneous by Lemma 8, we can apply Corollary 7. Moreover, item (d) of that corollary holds by Lemma 9; hence we obtain item (a), which gives the desired conclusion. $\hfill\blacktriangleleft$

Analogously, our result can also be used to derive other negative translation theorems, such as those established by Gödel [19] and Kuroda [28], which we introduced in Subsections 2.3–2.4. Notice that many negative translation theorems were originally formulated and proved over intuitionistic logic rather than minimal logic. As we have shown, some translations – such as Gentzen’s – can indeed be pushed down to the minimal setting, but this is not true in general. In Subsection 5.4, we apply our main result, Theorem 6, to identify the least logic for which Kuroda’s negative translation theorem holds, and we show that this logic properly extends minimal logic.

5.2 Minimality results à la Kuroda–Segerberg

Corollary 11.

Let $\text{$\mathbf{L}$}:=\langle\mathcal{R}\rangle$ , $j\colon S\rightarrow S$ , $\text{$\mathbf{L}$}^{\prime}:=\langle\mathcal{R},\mathcal{R}^{\prime}\rangle$ such that all rules in $\mathcal{R}^{\prime}$ are derivable in $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ and $j$ is a nucleus in $\text{$\mathbf{L}$}^{\prime}$ . Then the following are equivalent:

(a)

$\operatorname{Kleisli}_{j}(\text{$\mathbf{L}$}^{\prime})\supseteq\operatorname% {Max}_{j}(\text{$\mathbf{L}$})$ , i.e. $j$ is a $j$ -translation from $\operatorname{Max}_{j}(\text{$\mathbf{L}$}^{\prime})$ to $\text{$\mathbf{L}$}^{\prime}$ ;
(b)

all rules in $\mathcal{R}\cup\mathcal{R}^{\prime}$ are admissible in $\operatorname{Kleisli}_{j}(\text{$\mathbf{L}$}^{\prime})$ ;
(c)

$\operatorname{Gliv}_{j}(\text{$\mathbf{L}$})\subseteq\text{$\mathbf{L}$}^{\prime}$ .

Proof.

Let $\text{$\mathbf{L}$}^{\prime\prime}:=\langle\mathcal{R},\textnormal{L}j,% \textnormal{R}j\rangle$ . First, we observe that, $j$ is a nucleus in $\text{$\mathbf{L}$}^{\prime\prime}$ , and thus

\displaystyle\text{$\mathbf{L}$}^{\prime\prime}\vdash U\rhd ja\iff\text{$% \mathbf{L}$}^{\prime\prime}\vdash jU\rhd ja.

(

*

)

In fact, the “ $\Rightarrow$ ” direction corresponds simply to L $j$ , while the “ $\Leftarrow$ ” direction follows from repeated applications of transitivity using the instances $u\rhd ju$ for each $u\in U$ . This directly entails $\operatorname{Kleisli}_{j}(\text{$\mathbf{L}$}^{\prime\prime})=\operatorname{% Lift}_{j}^{1}(\text{$\mathbf{L}$}^{\prime\prime})$ . On the other hand, direct consequences of ( $*$ ‣ 5.2) also include that, over the rules of $\text{$\mathbf{L}$}^{\prime\prime}$ , rules $r_{j}$ and $r_{j}^{1}$ are equiadmissible, and also that $j$ is a nucleus in $\operatorname{Kol}_{j}^{1}(\text{$\mathbf{L}$}^{\prime\prime})$ . These two observations mean that $\operatorname{Kol}_{j}^{1}(\text{$\mathbf{L}$}^{\prime\prime})=\operatorname{% Gliv}_{j}(\text{$\mathbf{L}$}^{\prime\prime})$ . On the other hand, it is clear that $\operatorname{Gliv}_{j}(\text{$\mathbf{L}$}^{\prime\prime})=\operatorname{Gliv% }_{j}(\text{$\mathbf{L}$})$ . The claim now follows from Theorem 6 upon taking $k=j$ and substituting $\text{$\mathbf{L}$}^{\prime\prime}$ for $\mathbf{L}$ . $\hfill\blacktriangleleft$

This corollary is a version of [11, Theorem 3.5]⁶⁶6The original formulation appears in [13, Corollary 3.11], where it was derived as a corollary of Theorem 3.8 (corresponding here to Corollary 14). that only requires $j$ to be a nucleus in $\text{$\mathbf{L}$}^{\prime}$ (and not in $\mathbf{L}$ ), and can be regarded as an abstract formulation of several classical-to-constructive conservation results, including Kuroda’s conservation theorem [28] (based on intuitionistic predicate logic) and Segerberg’s claim [41, 35] (based on minimal propositional logic); see also Subsections 2.4 and 2.5. We now prove a version that simultaneously encompasses both, starting from minimal predicate logic.

First, we need a lemma:

Lemma 12.

$\text{$\mathbf{Gli}$}=\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{Min}$})$ .

Proof.

Let us start with the inclusion $\text{$\mathbf{Gli}$}\subseteq\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{% Min}$})$ . We need to show that both DNX and DNS are derivable in $\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{Min}$})$ .

$\blacksquare$

Since $\neg\neg\bot$ and $\bot$ are equivalent in $\mathbf{Min}$ , we have $\neg\neg\bot\rhd\neg\neg\varphi.$ By applying the rule $\mathrm{R}{\to}_{\neg\neg}$ , which is available in $\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{Min}$})$ , we conclude ${}\rhd\neg\neg(\bot\to\varphi).$
$\blacksquare$

From $\neg\neg\varphi[y/x]\rhd\neg\neg\varphi[y/x],$ we apply $\mathrm{L}\forall$ to obtain $\forall x\,\neg\neg\varphi\rhd\neg\neg\varphi[y/x].$ Then, by applying $\mathrm{R}\forall_{\neg\neg}$ , which is available in $\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{Min}$})$ , we conclude $\forall x\,\neg\neg\varphi\rhd\neg\neg\forall x\,\varphi.$

For the direction $\text{$\mathbf{Gli}$}\supseteq\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{% Min}$})$ , it suffices to show that all rules generating $\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{Min}$})$ are admissible in $\mathbf{Gli}$ . Again, this is technical but straightforward; details are provided in Appendix A. $\hfill\blacktriangleleft$

Proposition 13.

Let $\text{$\mathbf{L}$}^{\prime}$ be an inductive extension of $\mathbf{Min}$ such that all rules generating it are derivable in $\mathbf{Cla}$ . Then the following are equivalent:

(a)

$\operatorname{Kleisli}_{j}(\text{$\mathbf{L}$}^{\prime})\supseteq\text{$% \mathbf{Cla}$}$ , i.e. $\neg\neg$ is a $\neg\neg$ -translation from $\mathbf{Cla}$ to $\text{$\mathbf{L}$}^{\prime}$ ;
(b)

$\text{$\mathbf{Gli}$}\subseteq\text{$\mathbf{L}$}^{\prime}$ .

Proof.

Provided that $\text{$\mathbf{Gli}$}=\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{Min}$})$ (Lemma 12), the claim is exactly an instance of Corollary 11. $\hfill\blacktriangleleft$

5.3 Glivenko’s theorem

Corollary 14.

Let $\text{$\mathbf{L}$}:=\langle\mathcal{R}\rangle$ , $j\colon S\rightarrow S$ , such that $j$ is a nucleus in $\mathbf{L}$ . Then the following are equivalent:

(a)

$\operatorname{Kleisli}_{j}(\text{$\mathbf{L}$})\supseteq\operatorname{Max}_{j}% (\text{$\mathbf{L}$})$ , i.e. $j$ is a $j$ -translation from $\operatorname{Max}_{j}(\text{$\mathbf{L}$})$ to $\mathbf{L}$ ;
(b)

all rules in $\mathcal{R}$ are admissible in $\operatorname{Kleisli}_{j}(\text{$\mathbf{L}$})$ ;
(c)

$\operatorname{Gliv}_{j}(\text{$\mathbf{L}$})\subseteq\text{$\mathbf{L}$}$ .

Proof.

This is Corollary 11 with $\text{$\mathbf{L}$}=\text{$\mathbf{L}$}^{\prime}$ . Alternatively, it can also be deduced from Corollary 7 using the same strategy adopted in the proof of Corollary 11. $\hfill\blacktriangleleft$

This corollary is corresponds to [13, Theorem 3.8], and can be seen as an abstract formulation of Glivenko’s theorem [18].

Proposition 15 (Glivenko [18]).

In propositional logic, $\text{$\mathbf{Cla}$}\vdash\Gamma\Rightarrow\varphi$ if and only if $\text{$\mathbf{Int}$}\vdash\Gamma\Rightarrow\neg\neg\varphi$ .

Proof.

Let us interpret $\mathbf{L}$ as intuitionistic propositional logic $\mathbf{Int}$ and $j$ as double negation $\neg\neg$ . It is straightforward to verify that DNX is derivable in $\mathbf{Int}$ . Consequently, the Glivenko extension $\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{Int}$})$ – that is, intuitionistic logic augmented with DNX – coincides with $\mathbf{Int}$ itself. Then the claim follows from Corollary 14. $\hfill\blacktriangleleft$

5.4 Kuroda’s negative translation theorem with minimality

In this subsection, we want to apply our results to describe the least logic for which Kuroda’s double negation theorem holds. Consider $\mathbf{Min}$ , and define

$\displaystyle J(\varphi)$	$\displaystyle:\equiv\varphi,$	$\displaystyle\text{if }\varphi\text{ atomic},$
$\displaystyle J(\varphi_{1}*\varphi_{2})$	$\displaystyle:\equiv J(\varphi_{1})*J(\varphi_{2}),$	$\displaystyle\text{if }*\in\{\wedge,\vee,\to\},$
$\displaystyle J(\exists x\,\varphi)$	$\displaystyle:\equiv\exists x\,J(\varphi),$
$\displaystyle J(\forall x\,\varphi)$	$\displaystyle:\equiv\forall x\,\neg\neg J(\varphi).$

It is easy to see that $\neg\neg J$ is $\neg\neg$ -homogeneous in $\mathbf{Min}$ . Let us define $\mathbf{Kur}$ , by adding the following to the set of generating rules of $\mathbf{Min}$ :

Lemma 16.

$\operatorname{Kol}_{\neg\neg J}^{1}(\text{$\mathbf{Min}$})\subseteq\text{$% \mathbf{Kur}$}.$

Proof.

It suffices to prove that all rules generating $\operatorname{Kol}_{\neg\neg J}^{1}(\text{$\mathbf{Min}$})$ are admissible in $\mathbf{Kur}$ . Again, this is technical but straightforward; the details are provided in Appendix A. $\hfill\blacktriangleleft$

Proposition 17.

Let $\mathbf{L}$ be an inductive extension of $\mathbf{Min}$ such that all its generating rules are derivable in $\mathbf{Cla}$ . Then the following are equivalent:

(a)

$\neg\neg J$ is a $\neg\neg$ -translation from $\mathbf{Cla}$ to $\mathbf{L}$ ;
(b)

$\text{$\mathbf{Kur}$}\subseteq\text{$\mathbf{L}$}$ .

Proof.

We clearly have $\text{$\mathbf{Kur}$}\subseteq\operatorname{Kol}_{\neg\neg J}^{1}(\text{$% \mathbf{Min}$})$ . Since also the other inclusion holds by Lemma 16, the two logics in fact coincide. The desired result then follows from Theorem 6. $\hfill\blacktriangleleft$

In the final part of this section, we aim to show that $\mathbf{Kur}$ is distinct from the other logics introduced so far. Clearly, we have $\text{$\mathbf{Min}$}\subseteq\text{$\mathbf{Kur}$}$ , but we now show that this inclusion is strict. Consider a quantifier-free formula $\varphi$ . Then, by the definition of $J$ , we have $J(\varphi):\equiv\varphi$ . Observe that in $\mathbf{Min}$ we can easily derive:

		$\displaystyle\rhd\neg\neg(\bot\to\neg\neg\varphi),$
	$\displaystyle\neg\neg(\bot\to\neg\neg\varphi),\,\neg\neg\bot$	$\displaystyle\rhd\neg\neg\varphi.$

Now, working in $\mathbf{Kur}$ , from the latter sequent we obtain

\neg\neg(\bot\to\neg\neg\varphi)\rhd\neg\neg(\bot\to\varphi)

by an application of the rule $\mathrm{R}{\to}_{\neg\neg J}^{1}$ , which is applicable since $J(\varphi):\equiv\varphi$ and $J(\bot):\equiv\bot$ . Then, by cutting this with the former sequent, we conclude:

{}\rhd\neg\neg(\bot\to\varphi),

that is, the double negation of explosion holds for quantifier-free formulae in $\mathbf{Kur}$ , which is not the case in $\mathbf{Min}$ [41, 36]. Therefore, $\text{$\mathbf{Min}$}\subsetneq\text{$\mathbf{Kur}$}$ . Next, we show that the (unrestricted) double negation of explosion $\neg\neg(\bot\to\varphi)$ is strictly stronger than the rule $\mathrm{R}{\to}_{\neg\neg J}^{1}$ . Suppose the premiss of the rule $\mathrm{R}{\to}_{\neg\neg J}^{1}$ is derivable; that is,

\neg\neg J(\Gamma),\,\neg\neg J(\varphi)\rhd\neg\neg J(\psi).

By applying the rule $\mathrm{R}{\to}$ , we obtain:

\neg\neg J(\Gamma)\rhd\neg\neg J(\varphi)\to\neg\neg J(\psi).

On the other hand, from the double negation of explosion we can derive by Lemma 4:

\neg\neg J(\varphi)\to\neg\neg J(\psi)\rhd\neg\neg J(\varphi\to\psi).

By cutting these two sequents, we obtain the conclusion of the rule $\mathrm{R}{\to}_{\neg\neg J}^{1}$ , as required. Since the double negation of explosion is derivable both in $\mathbf{Int}$ and in $\mathbf{Gli}$ , it follows that both inclusions $\text{$\mathbf{Kur}$}\subseteq\text{$\mathbf{Int}$}$ and $\text{$\mathbf{Kur}$}\subseteq\text{$\mathbf{Gli}$}$ hold. As $\mathbf{Int}$ and $\mathbf{Gli}$ are incomparable, it follows that both these inclusions are strict as well. Thus, we have established that $\mathbf{Kur}$ is indeed distinct from all the other logics considered so far, as claimed.

The present discussion is intended only as an initial analysis: we identify $\mathbf{Kur}$ as the minimal logic validating Kuroda’s negative translation theorem and show that it is not reducible to any previously considered system. Further comparative questions – for example its precise relation to $\text{$\mathbf{Gli}$}\cap\text{$\mathbf{Int}$}$ – are left for future investigation.

6 Final remarks

In this note, we have unified and extended previous generalisations of Glivenko’s theorem by providing an abstract framework capable of simultaneously treating both extensions and translations of logical systems. Our approach relaxes prior assumptions by requiring the nucleus property only in the Glivenko extension, thereby broadening the applicability and flexibility of the framework. This generalisation subsumes and connects classical results such as those by Glivenko, Kolmogorov, Kuroda, and Segerberg in a single, comprehensive setting. In this respect, our framework resonates strongly with Fred Richman’s [38, 37] conception of intuitionistic logic as a generalisation of classical logic. First, conservation theorems show that classical results can be translated into constructive logic, supporting Richman’s claim that classical and constructive mathematics need not be developed as separate, incompatible enterprises but rather as facets of a unified mathematical practice. Second, by treating translations and extensions in a fully abstract manner, our approach reflects the same structural flexibility that, in Richman’s view, enables intuitionistic mathematics to include classical theorems as special cases while preserving their constructive content.

An interesting direction for future work would be to investigate whether this abstract approach can be further extended to encompass Orevkov’s results [36]. In 1968, Vladimir Orevkov established a series of conservativity theorems concerning classical logic over intuitionistic and minimal first-order logics with equality. Notably, he identified seven distinct classes of single-succedent sequents – the so-called Glivenko sequent classes – characterised syntactically by the absence of positive or negative occurrences of certain logical symbols in a first-order language with equality. Orevkov showed that within these classes, classical derivability implies intuitionistic derivability, and that these classes are optimal in the sense that any collection of sequents enjoying this conservativity property is contained within one of the seven classes.

In recent years, simplified proofs of conservativity for some of Orevkov’s Glivenko classes have been developed. For instance, Sara Negri [31] provided a remarkably concise, purely logical proof for the first Glivenko class for coherent theories using $\mathbf{G3}$ -style sequent calculi. This was subsequently extended to geometric theories [32] and then further generalised to cover all seven Glivenko sequent classes [33, 9]. It would be worthwhile to explore whether the abstract, nucleus-based approach presented in this work could be adapted to provide a uniform account of these sequent-level conservativity results as well.

References

[1] Peter Aczel. The Russell–Prawitz modality. Mathematical Structures in Computer Science, 11:541–554, 2001. doi:10.1017/S0960129501003309.
[2] Peter Aczel. Aspects of general topology in constructive set theory. Annals of Pure and Applied Logic, 137:3–29, 2006. doi:10.1016/j.apal.2005.05.016.
[3] Giacomo Bartoli, Giulio Fellin, and Matteo Tesi. Infinitary negative translations and Glivenko logic. Submitted, 2025.
[4] Marcel Barzin and Alfred Errera. Sur la logique de M. Brouwer. Bulletin de la Classe des Sciences. Académie royale de Belgique, 13:56–71, 1927. URL: https://dipot.ulb.ac.be/dspace/bitstream/2013/233730/4/ce95c10e-1981-4536-8077-6e2caefcaf78.txt.
[5] L. E. J. Brouwer. Over de Grondslagen der Wiskunde. Universiteit van Amsterdam, 1907. Ph.D. thesis. URL: https://eprints.illc.uva.nl/id/eprint/1852/2/HDS-20-LEJBrouwer.text.pdf.
[6] L. E. J. Brouwer. De onbetrouwbaarheid der logische principes. Noordhoff, Groningen, 1908.
[7] René David, Karim Nour, and Christophe Raffali. Introduction à la Logique. Théorie de la démonstration. Dunod, 2004.
[8] Martín Hötzel Escardó and Paulo Oliva. The Peirce translation. Annals of Pure and Applied Logic, 163(6):681–692, 2012. doi:10.1016/J.APAL.2011.11.002.
[9] Giulio Fellin, Sara Negri, and Eugenio Orlandelli. Glivenko sequent classes and constructive cut elimination in geometric logics. Archive for Mathematical Logic, 62(5-6):657–688, 2023. doi:10.1007/S00153-022-00857-Z.
[10] Giulio Fellin, Sara Negri, and Peter Schuster. Nuclear shifts for conservation. Unpublished preprint, 2025.
[11] Giulio Fellin and Peter Schuster. Conservation as translation. Review of Symbolic Logic, 18(1):316–348, 2025. doi:10.1017/S1755020324000170.
[12] Giulio Fellin, Peter Schuster, and Daniel Misselbeck-Wessel. The Jacobson radical of a propositional theory. Bulletin of Symbolic Logic, 28(2):163–181, 2022. doi:10.1017/BSL.2021.66.
[13] Giulio Fellin and Peter M. Schuster. A general Glivenko-Gödel theorem for nuclei. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 51–66, 2021. doi:10.4204/EPTCS.351.4.
[14] Giulio Fellin, Tarmo Uustalu, and Cheng-Syuan Wan. Glivenko’s theorem beyond structure. Submitted, 2025.
[15] Gilda Ferreira and Paulo Oliva. On the relation between various negative trans- lations. In Ulrich Berger, Hannes Diener, Peter Schuster, and Monika Seisenberger, editors, Logic, Construction, Computation, pages 227–258, Frankfurt, 2013. De Gruyter. doi:10.1515/9783110324921.227.
[16] Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493–565, 1936. doi:10.1007/BF01565428.
[17] Valery Glivenko. Sur la logique de M. Brouwer. Académie royale de Belgique. Bulletin de la Classe des Sciences, 14(5):225–228, 1928. URL: https://upload.wikimedia.org/wikipedia/commons/0/07/Sur_la_logique_de_M_Brouwer.pdf.
[18] Valery Glivenko. Sur quelques points de la logique de M. Brouwer. Académie royale de Belgique. Bulletin de la Classe des Sciences, 15(5):183–188, 1929. URL: https://upload.wikimedia.org/wikipedia/commons/5/5b/Sur_quelque_points_de_la_logique_de_M_Brouwer.pdf.
[19] Kurt Gödel. Zur intuitionistischen Arithmetik und Zahlentheorie (1933e). In Solomon Feferman, John W. Dawson Jr., Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay, and Jean van Heijenoort, editors, Collected Works, Volume I: Publications 1929–1936, pages 286–294. Clarendon Press / Oxford University Press, New York and Oxford, 1986. Includes English translation On intuitionistic arithmetic and number theory (pp. 287–295) and A. S. Troelstra’s introductory note (pp. 282–287). doi:10.1093/oso/9780195147209.003.0063.
[20] Robert Ian Goldblatt. Decidability of some extensions of J. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 20:203–205, 1974. doi:10.1002/malq.19740201304.
[21] Timothy G. Griffin. A formulae-as-types notion of control. In Proceedings of the Principles of Programming Languages (POPL ’90), pages 47–58, New York, NY, USA, 1989. Association for Computing Machinery. doi:10.1145/96709.96714.
[22] Levon Haykazyan. More on a curious nucleus. Journal of Pure and Applied Algebra, 224:860–868, 2020. doi:10.1016/j.jpaa.2019.06.014.
[23] Arend Heyting. Die formalen Regeln der intuitionistischen Logik I. Sitzungsberichte der Preussischen Akademie der Wissenschaften, pages 42–56, 1930.
[24] Ingebrigt Johansson. Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compositio Mathematica, 4:119–136, 1937. URL: http://eudml.org/doc/88648.
[25] Peter T. Johnstone. Stone Spaces, volume 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.
[26] Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008. doi:10.1007/978-3-540-77533-1.
[27] Andrey N. Kolmogoroff. Sur le principe de tertium non datur. Matematicheskii Sbornik, 32(4):646–667, 1925. Zbl: https://zbmath.org/?q=an:51.0048.01. URL: http://mi.mathnet.ru/sm7425.
[28] Sigekatu Kuroda. Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Mathematical Journal, 3:35–47, 1951. doi:10.1017/S0027763000010023.
[29] Chetan R. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, 1990. URL: https://ecommons.cornell.edu/items/2f12c8d8-71fd-4dbc-80ae-7b5948faaae8.
[30] Sara Negri. Continuous domains as formal spaces. Mathematical Structures in Computer Science, 12:19–52, 2002. doi:10.1017/S0960129501003450.
[31] Sara Negri. Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Archive for Mathematical Logic, 42(4):389–401, 2003. doi:10.1007/s001530100124.
[32] Sara Negri. Glivenko sequent classes in the light of structural proof theory. Archive for Mathematical Logic, 55(3–4):461–473, 2016. doi:10.1007/s00153-016-0474-y.
[33] Sara Negri. Geometric rules in infinitary logic. In Ofer Arieli and Anna Zamansky, editors, Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, pages 265–293. Springer, Cham, 2021. doi:10.1007/978-3-030-71258-7_12.
[34] Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, Cambridge, 2001. doi:10.1017/CBO9780511527340.
[35] Sergei P. Odintsov. Logic of classical refutability and extensions of minimal logic. Logic and Logical Philosophy, 9:91–107, 2004. doi:10.12775/LLP.2001.006.
[36] Vladimir P. Orevkov. On Glivenko sequent classes. Proceedings of the Steklov Institute of Mathematics, 98:147–173, 1968. Translated from the Russian original: “O glivenkovskikh klassakh sekventsii” (On Glivenko’s sequent classes), in Logical and Logical-Mathematical Calculus. Part I, Trudy Matematicheskogo Instituta Imeni V. A. Steklova, 98 (1968), 131–154. URL: http://mi.mathnet.ru/tm2930.
[37] Fred Richman. Confessions of a formalist, platonist, intuitionist. Unpublished manuscript, April 9, 1994. Formerly available at Richman’s personal website (no longer accessible).
[38] Fred Richman. Intuitionism as generalization. Philosophia Mathematica, 5(1–2):124–128, 1990. doi:10.1093/philmat/s2-5.1-2.124.
[39] Kimmo I. Rosenthal. Quantales and their Applications, volume 234 of Pitman Research Notes in Mathematics. Longman Scientific & Technical, Essex, 1990.
[40] Helmut Schwichtenberg and Stanley S. Wainer. Proofs and Computations. Perspectives in Logic. Cambridge University Press and Association for Symbolic Logic, 2012. doi:10.1017/CBO9781139031905.
[41] Krister Segerberg. Propositional logics related to Heyting’s and Johansson’s. Theoria, 34(1):26–61, 1968. doi:10.1111/j.1755-2567.1968.tb00337.x.
[42] Harold Simmons. A framework for topology. In Angus Macintyre, Leszek Pacholski, and Jeff Paris, editors, Logic Colloquium ’77, volume 96 of Studies in Logic and the Foundations of Mathematics, pages 239–251. Elsevier, 1978. doi:10.1016/S0049-237X(08)72007-X.
[43] Harold Simmons. A curious nucleus. Journal of Pure and Applied Algebra, 214:2063–2073, 2010. doi:10.1016/j.jpaa.2010.02.011.
[44] Clifford Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In Jacob C. E. Dekker, editor, Recursive Function Theory, volume 5 of Proceedings of Symposia in Pure Mathematics, pages 1–27. American Mathematical Society, Providence, RI, 1962.
[45] Christian Thiel. Die kontroverse um die intuitionistische logik vor ihrer axiomatisierung durch heyting im jahre 1930. History and Philosophy of Logic, 9(1):67–75, 1988. doi:10.1080/01445348808837126.
[46] Anne S. Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge University Press, Cambridge, 2nd edition, 2000.
[47] Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics: An Introduction, volume I and II. North-Holland, Amsterdam, 1988.
[48] Benno van den Berg. A Kuroda-style j-translation. Archive for Mathematical Logic, 58:627–634, 2019. doi:10.1007/s00153-018-0656-x.
[49] Peter W. Woodruff. A note on JP’. Theoria, 36:183–184, 1970. doi:10.1111/j.1755-2567.1970.tb00419.x.

Appendix A Technical proof details

Proof of Lemma 4.

As for $\textnormal{DNS}_{\to}\Longrightarrow\textnormal{DNX}$ :

As for $\textnormal{DNX}\Longrightarrow\textnormal{DNS}_{\to}$ :

where m.p. (modus ponens) is an easy consequence of L $\to$ , while $\neg(\varphi\to\psi)\rhd\neg\neg\varphi$ is derived as follows:

$\hfill\blacktriangleleft$

Before giving the proof of Lemma 9, we need the following:

Lemma 18.

The following is admissible in $\mathbf{Min}$ , where $k$ is either $K$ or $G$ :

Proof.

Proof by induction on the shape of $\delta$ :

$\blacksquare$

If $k=K$ or $\delta$ is either atomic, a disjunction, or existential, then $k(\delta):\equiv\neg\neg\delta^{\prime}$ for some $\delta^{\prime}$ , so rule L $\neg\neg$ can be applied.
$\blacksquare$

Suppose that $k=G$ and $\delta:\equiv\alpha\wedge\beta$ . We have $\varphi,\Gamma\rhd G(\alpha)\wedge G(\beta)$ , which is equivalent to have both $\varphi,\Gamma\rhd G(\alpha)$ and $\varphi,\Gamma\rhd G(\beta)$ . By induction hypothesis, we have $\neg\neg\varphi,\Gamma\rhd G(\alpha)$ and $\neg\neg\varphi,\Gamma\rhd G(\beta)$ , which together yield $\neg\neg\varphi,\Gamma\rhd G(\alpha)\wedge G(\beta)$ .

The cases $\delta:\equiv\alpha\to\beta$ and $\delta:\equiv\forall x\,\alpha$ are handled in a similar manner by applying the induction hypothesis.

$\hfill\blacktriangleleft$

Proof of Lemma 9.

Let $k$ be either $K$ or $G$ . We prove that all rules generating $\operatorname{Kol}_{k}^{1}(\text{$\mathbf{Min}$})$ are already admissible in $\mathbf{Min}$ .

$\blacksquare$

A straightforward proof by induction, using the fact that in $\mathbf{Min}$ a negated formula is provably equivalent to its double negation, shows that $k$ is inflationary and idempotent.
$\blacksquare$

Let us consider the rule

Assume that the two premisses are derivable in $\mathbf{Min}$ ; we aim to show that the conclusion is derivable in $\mathbf{Min}$ as well. If $k=G$ , then it is trivial, so let us focus on the case in which $k=K$ . First, observe that as an easy consequence of the rules $\mathrm{R}\wedge$ and R $\neg\neg$ , the following sequent is derivable:

$k(\varphi_{1}),k(\varphi_{2})\rhd\neg\neg(k(\varphi_{1})\wedge k(\varphi_{2})),$

which, by the definition of $k$ , is equivalent to

$k(\varphi_{1}),k(\varphi_{2})\rhd k(\varphi_{1}\wedge\varphi_{2}).$

Finally, the desired conclusion follows by applying transitivity to this last sequent together with the two premisses.

The rules $\mathrm{L}\wedge_{k}^{1}$ , $\mathrm{L}{\to}_{k}^{1}$ , and $\mathrm{L}\forall_{k}^{1}$ can be handled in a similar manner.
$\blacksquare$

Let us consider the rule

Assume that the premiss are derivable in $\mathbf{Min}$ ; we aim to show that the conclusion is derivable in $\mathbf{Min}$ as well. First, observe that as an easy consequence of the rules $\mathrm{R}\vee$ and R $\neg\neg$ , the following sequent is derivable:

$k(\varphi_{1})\rhd\neg\neg(k(\varphi_{1})\vee k(\varphi_{2})),$

which, by the definition of $k$ , is equivalent to

$k(\varphi_{1})\rhd k(\varphi_{1}\vee\varphi_{2}).$

Finally, the desired conclusion follows by applying transitivity to this last sequent together with the premiss.

The rules $\mathrm{R}\top_{k}^{1}$ , $\mathrm{R}\vee_{2k}^{1}$ , and $\mathrm{R}\exists_{k}^{1}$ can be handled in a similar manner.
$\blacksquare$

Let us consider the rule

Assume that the two premisses are derivable in $\mathbf{Min}$ ; we aim to show that the conclusion is derivable in $\mathbf{Min}$ as well.
We want to show:

$\displaystyle k(\varphi_{1}\vee\varphi_{2}),k(\varphi_{1}\to\delta),k(\varphi_% {2}\to\delta)\rhd k(\delta).$ (1)

First, observe that by applying the rules L $\to$ an L $\vee$ , we have

$\displaystyle k(\varphi_{1})\vee k(\varphi_{2}),k(\varphi_{1})\to k(\delta),k(% \varphi_{2})\to k(\delta)\rhd k(\delta).$ (2)

We now distinguish two cases:
- –
  
  Case $k=K$ . We can apply Lemma 18 thrice, and get
  
  $\neg\neg(K(\varphi_{1})\vee K(\varphi_{2})),\neg\neg(K(\varphi_{1})\to K(% \delta)),\neg\neg(K(\varphi_{2})\to K(\delta))\rhd K(\delta),$
  
  which, by the definition of $K$ , is the same as (1) for $k=K$ .
- –
  
  Case $k=G$ . We can apply Lemma 18 once, and get
  
  $\neg\neg(G(\varphi_{1})\vee G(\varphi_{2})),G(\varphi_{1})\to G(\delta),G(% \varphi_{2})\to G(\delta)\rhd G(\delta),$
  
  which, by the definition of $G$ , is the same as (1) for $k=G$ .
Therefore, we have proved (1) in both cases, as claimed.
On the other hand, we observe that by applying R $\to$ and R $\neg\neg$ to the two premisses, respectively, we get

$\displaystyle k(\Gamma)$ $\displaystyle\rhd\neg\neg(k(\varphi_{1})\to k(\delta)),$ and $\displaystyle k(\Gamma)$ $\displaystyle\rhd\neg\neg(k(\varphi_{2})\to k(\delta)).$

i.e.

$\displaystyle k(\Gamma)$ $\displaystyle\rhd k(\varphi_{1}\to\delta),$ and $\displaystyle k(\Gamma)$ $\displaystyle\rhd k(\varphi_{2}\to\delta).$

Finally, the desired conclusion follows by transitivity between the latter two and (1).

The rule $\mathrm{L}\exists_{k}^{1}$ can be handled in a similar manner.
$\blacksquare$

Let us consider the rule

Assume that the premiss is derivable in $\mathbf{Min}$ , we want to derive the conclusion. Then we can derive the conclusion by a simple application of R $\to$ , with an extra application of R $\neg\neg$ in the case $k=K$ .

The rule $\mathrm{R}\forall_{k}^{1}$ can be handled in a similar manner.

$\hfill\blacktriangleleft$

Proof of Lemma 12.

We prove that all rules generating $\operatorname{Gliv}_{\neg\neg}(\text{$\mathbf{Min}$})$ are admissible in $\mathbf{Gli}$ .

$\blacksquare$

Because the function $\neg\neg$ is already a nucleus in $\mathbf{Min}$ , it is a nucleus also in $\mathbf{Gli}$ . This means that L $\neg\neg$ and R $\neg\neg$ hold.
$\blacksquare$

Let us consider the rule

Assume that the two premisses are derivable in $\mathbf{Gli}$ ; we aim to show that the conclusion is derivable in $\mathbf{Gli}$ as well. We notice that the proof we give here is already valid in $\mathbf{Min}$ .

First, observe that as an easy consequence of the rules $\mathrm{R}\wedge$ and R $\to$ , the following sequent is derivable:

$\varphi_{1},\varphi_{2},\neg(\varphi_{1}\wedge\varphi_{2})\rhd\bot.$

Now, using the fact that $\neg\neg\bot$ and $\bot$ are equivalent, we can apply L $\neg\neg$ twice:

$\neg\neg\varphi_{1},\neg\neg\varphi_{2},\neg(\varphi_{1}\wedge\varphi_{2})\rhd\bot,$

from which we get

$\neg\neg\varphi_{1},\neg\neg\varphi_{2}\rhd\neg\neg(\varphi_{1}\wedge\varphi_{% 2})$

by an application of R $\to$ . Finally, the desired conclusion follows by applying transitivity to this last sequent together with the two premisses.

The rules $\mathrm{R}\top_{\neg\neg}$ , $\mathrm{L}\wedge_{\neg\neg}$ , $\mathrm{L}\vee_{\neg\neg}$ , $\mathrm{R}\vee_{1\neg\neg}$ , $\mathrm{R}\vee_{2\neg\neg}$ , $\mathrm{L}{\to}_{\neg\neg}$ , $\mathrm{L}\exists_{\neg\neg}$ , $\mathrm{R}\exists_{\neg\neg}$ , $\mathrm{L}\forall_{\neg\neg}$ can be handled in a similar manner.
$\blacksquare$

Let us consider the rule

Assume that the premiss is derivable in $\mathbf{Gli}$ ; we aim to show that the conclusion is derivable in $\mathbf{Gli}$ as well. First, by R $\to$ we get

$\Gamma\rhd\varphi\to\neg\neg\psi.$

On the other hand, by Lemma 4 we know that DNX entails

$\varphi\to\neg\neg\psi\rhd\neg\neg(\varphi\to\psi).$

An application of Trans gives us the desired conclusion.
$\blacksquare$

Let us consider the rule

Assume that the premiss is derivable in $\mathbf{Gli}$ . Then by R $\forall$ we get

$\Gamma\rhd\forall x\,\neg\neg\varphi.$

By cutting the latter with DNS, we get the desired conclusion.

$\hfill\blacktriangleleft$

Proof of Lemma 16.

We prove that all rules generating $\operatorname{Kol}_{\neg\neg J}^{1}(\text{$\mathbf{Min}$})$ are admissible in $\mathbf{Kur}$ .

$\blacksquare$

An easy proof by induction shows that $J$ is inflationary and idempotent already in $\mathbf{Min}$ , and these properties are immediately inherited by $\neg\neg J$ . In other words, the rules L $\neg\neg J^{-}$ and R $\neg\neg J^{-}$ are admissible in $\mathbf{Min}$ , and hence also in $\mathbf{Kur}$ .
$\blacksquare$

Let us consider the rule

Assume that the two premisses are derivable in $\mathbf{Kur}$ ; we aim to show that the conclusion is derivable in $\mathbf{Kur}$ as well. We notice that the proof we give here is already valid in $\mathbf{Min}$ .

First, observe that by applying the rule $\mathrm{R}\wedge$ , we have

$J(\varphi_{1}),J(\varphi_{2})\rhd J(\varphi_{1})\wedge J(\varphi_{2}),$

which, by the definition of $J$ , is equivalent to

$J(\varphi_{1}),J(\varphi_{2})\rhd J(\varphi_{1}\wedge\varphi_{2}).$

Now, by using the rules $\mathrm{R}\neg\neg$ and $\mathrm{L}\neg\neg$ , we obtain

$\neg\neg J(\varphi_{1}),\neg\neg J(\varphi_{2})\rhd\neg\neg J(\varphi_{1}% \wedge\varphi_{2}).$

Finally, the desired conclusion follows by applying transitivity to this last sequent together with the two premisses.

The rules $\mathrm{R}\top_{\neg\neg J}^{1}$ , $\mathrm{L}\wedge_{\neg\neg J}^{1}$ , $\mathrm{R}\vee_{1\neg\neg J}^{1}$ , $\mathrm{R}\vee_{2\neg\neg J}^{1}$ , $\mathrm{L}{\to}_{\neg\neg J}^{1}$ , $\mathrm{R}\exists_{\neg\neg J}^{1}$ , and $\mathrm{L}\forall_{\neg\neg J}^{1}$ can be handled in a similar manner.
$\blacksquare$

Let us consider the rule

Assume that the two premisses are derivable in $\mathbf{Kur}$ ; we aim to show that the conclusion is derivable in $\mathbf{Kur}$ as well.

First, observe that by applying the rules L $\to$ an L $\vee$ , we have

$J(\varphi_{1})\vee J(\varphi_{2}),J(\varphi_{1})\to J(\delta),J(\varphi_{2})% \to J(\delta)\rhd J(\delta),$

which, by the definition of $J$ , is equivalent to

$J(\varphi_{1}\vee\varphi_{2}),J(\varphi_{1}\to\delta),J(\varphi_{2}\to\delta)% \rhd J(\delta).$

Now, by using the rules $\mathrm{R}\neg\neg$ and $\mathrm{L}\neg\neg$ , we obtain

$\neg\neg J(\varphi_{1}\vee\varphi_{2}),\neg\neg J(\varphi_{1}\to\delta),\neg% \neg J(\varphi_{2}\to\delta)\rhd\neg\neg J(\delta).$

On the other hand, we observe that by applying R $\to_{\neg\neg J}^{1}$ to the two premisses, respectively, we get

$\displaystyle\neg\neg J(\Gamma)$ $\displaystyle\rhd\neg\neg J(\varphi_{1}\to\delta),$ and $\displaystyle\neg\neg J(\Gamma)$ $\displaystyle\rhd\neg\neg J(\varphi_{2}\to\delta).$

Finally, the desired conclusion follows by transitivity.

The rule $\mathrm{L}\exists_{\neg\neg J}^{1}$ can be handled in a similar manner.
$\blacksquare$

Let us consider the rule

Assume that the premiss is derivable in $\mathbf{Kur}$ ; we aim to show that the conclusion is derivable in $\mathbf{Kur}$ as well. By applying R $\forall$ to the premiss, we get

$\neg\neg J(\Gamma)\rhd\forall x\,\neg\neg J(\varphi),$

which, by definition of $J$ , is just

$\neg\neg J(\Gamma)\rhd J(\forall x\,\varphi).$

Conclude by R $\neg\neg$ .

$\hfill\blacktriangleleft$

[bib.bib1] [1] Peter Aczel. The Russell–Prawitz modality. Mathematical Structures in Computer Science, 11:541–554, 2001. doi:10.1017/S0960129501003309.

[bib.bib2] [2] Peter Aczel. Aspects of general topology in constructive set theory. Annals of Pure and Applied Logic, 137:3–29, 2006. doi:10.1016/j.apal.2005.05.016.

[bib.bib3] [3] Giacomo Bartoli, Giulio Fellin, and Matteo Tesi. Infinitary negative translations and Glivenko logic. Submitted, 2025.

[bib.bib4] [4] Marcel Barzin and Alfred Errera. Sur la logique de M. Brouwer. Bulletin de la Classe des Sciences. Académie royale de Belgique, 13:56–71, 1927. URL: https://dipot.ulb.ac.be/dspace/bitstream/2013/233730/4/ce95c10e-1981-4536-8077-6e2caefcaf78.txt.

[bib.bib5] [5] L. E. J. Brouwer. Over de Grondslagen der Wiskunde. Universiteit van Amsterdam, 1907. Ph.D. thesis. URL: https://eprints.illc.uva.nl/id/eprint/1852/2/HDS-20-LEJBrouwer.text.pdf.

[bib.bib6] [6] L. E. J. Brouwer. De onbetrouwbaarheid der logische principes. Noordhoff, Groningen, 1908.

[bib.bib7] [7] René David, Karim Nour, and Christophe Raffali. Introduction à la Logique. Théorie de la démonstration. Dunod, 2004.

[bib.bib8] [8] Martín Hötzel Escardó and Paulo Oliva. The Peirce translation. Annals of Pure and Applied Logic, 163(6):681–692, 2012. doi:10.1016/J.APAL.2011.11.002.

[bib.bib9] [9] Giulio Fellin, Sara Negri, and Eugenio Orlandelli. Glivenko sequent classes and constructive cut elimination in geometric logics. Archive for Mathematical Logic, 62(5-6):657–688, 2023. doi:10.1007/S00153-022-00857-Z.

[bib.bib10] [10] Giulio Fellin, Sara Negri, and Peter Schuster. Nuclear shifts for conservation. Unpublished preprint, 2025.

[bib.bib11] [11] Giulio Fellin and Peter Schuster. Conservation as translation. Review of Symbolic Logic, 18(1):316–348, 2025. doi:10.1017/S1755020324000170.

[bib.bib12] [12] Giulio Fellin, Peter Schuster, and Daniel Misselbeck-Wessel. The Jacobson radical of a propositional theory. Bulletin of Symbolic Logic, 28(2):163–181, 2022. doi:10.1017/BSL.2021.66.

[bib.bib13] [13] Giulio Fellin and Peter M. Schuster. A general Glivenko-Gödel theorem for nuclei. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 51–66, 2021. doi:10.4204/EPTCS.351.4.

[bib.bib14] [14] Giulio Fellin, Tarmo Uustalu, and Cheng-Syuan Wan. Glivenko’s theorem beyond structure. Submitted, 2025.

[bib.bib15] [15] Gilda Ferreira and Paulo Oliva. On the relation between various negative trans- lations. In Ulrich Berger, Hannes Diener, Peter Schuster, and Monika Seisenberger, editors, Logic, Construction, Computation, pages 227–258, Frankfurt, 2013. De Gruyter. doi:10.1515/9783110324921.227.

[bib.bib16] [16] Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493–565, 1936. doi:10.1007/BF01565428.

[bib.bib17] [17] Valery Glivenko. Sur la logique de M. Brouwer. Académie royale de Belgique. Bulletin de la Classe des Sciences, 14(5):225–228, 1928. URL: https://upload.wikimedia.org/wikipedia/commons/0/07/Sur_la_logique_de_M_Brouwer.pdf.

[bib.bib18] [18] Valery Glivenko. Sur quelques points de la logique de M. Brouwer. Académie royale de Belgique. Bulletin de la Classe des Sciences, 15(5):183–188, 1929. URL: https://upload.wikimedia.org/wikipedia/commons/5/5b/Sur_quelque_points_de_la_logique_de_M_Brouwer.pdf.

[bib.bib19] [19] Kurt Gödel. Zur intuitionistischen Arithmetik und Zahlentheorie (1933e). In Solomon Feferman, John W. Dawson Jr., Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay, and Jean van Heijenoort, editors, Collected Works, Volume I: Publications 1929–1936, pages 286–294. Clarendon Press / Oxford University Press, New York and Oxford, 1986. Includes English translation On intuitionistic arithmetic and number theory (pp. 287–295) and A. S. Troelstra’s introductory note (pp. 282–287). doi:10.1093/oso/9780195147209.003.0063.

[bib.bib20] [20] Robert Ian Goldblatt. Decidability of some extensions of J. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 20:203–205, 1974. doi:10.1002/malq.19740201304.

[bib.bib21] [21] Timothy G. Griffin. A formulae-as-types notion of control. In Proceedings of the Principles of Programming Languages (POPL ’90), pages 47–58, New York, NY, USA, 1989. Association for Computing Machinery. doi:10.1145/96709.96714.

[bib.bib22] [22] Levon Haykazyan. More on a curious nucleus. Journal of Pure and Applied Algebra, 224:860–868, 2020. doi:10.1016/j.jpaa.2019.06.014.

[bib.bib23] [23] Arend Heyting. Die formalen Regeln der intuitionistischen Logik I. Sitzungsberichte der Preussischen Akademie der Wissenschaften, pages 42–56, 1930.

[bib.bib24] [24] Ingebrigt Johansson. Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compositio Mathematica, 4:119–136, 1937. URL: http://eudml.org/doc/88648.

[bib.bib25] [25] Peter T. Johnstone. Stone Spaces, volume 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[bib.bib26] [26] Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008. doi:10.1007/978-3-540-77533-1.

[bib.bib27] [27] Andrey N. Kolmogoroff. Sur le principe de tertium non datur. Matematicheskii Sbornik, 32(4):646–667, 1925. Zbl: https://zbmath.org/?q=an:51.0048.01. URL: http://mi.mathnet.ru/sm7425.

[bib.bib28] [28] Sigekatu Kuroda. Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Mathematical Journal, 3:35–47, 1951. doi:10.1017/S0027763000010023.

[bib.bib29] [29] Chetan R. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, 1990. URL: https://ecommons.cornell.edu/items/2f12c8d8-71fd-4dbc-80ae-7b5948faaae8.

[bib.bib30] [30] Sara Negri. Continuous domains as formal spaces. Mathematical Structures in Computer Science, 12:19–52, 2002. doi:10.1017/S0960129501003450.

[bib.bib31] [31] Sara Negri. Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Archive for Mathematical Logic, 42(4):389–401, 2003. doi:10.1007/s001530100124.

[bib.bib32] [32] Sara Negri. Glivenko sequent classes in the light of structural proof theory. Archive for Mathematical Logic, 55(3–4):461–473, 2016. doi:10.1007/s00153-016-0474-y.

[bib.bib33] [33] Sara Negri. Geometric rules in infinitary logic. In Ofer Arieli and Anna Zamansky, editors, Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, pages 265–293. Springer, Cham, 2021. doi:10.1007/978-3-030-71258-7_12.

[bib.bib34] [34] Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, Cambridge, 2001. doi:10.1017/CBO9780511527340.

[bib.bib35] [35] Sergei P. Odintsov. Logic of classical refutability and extensions of minimal logic. Logic and Logical Philosophy, 9:91–107, 2004. doi:10.12775/LLP.2001.006.

[bib.bib36] [36] Vladimir P. Orevkov. On Glivenko sequent classes. Proceedings of the Steklov Institute of Mathematics, 98:147–173, 1968. Translated from the Russian original: “O glivenkovskikh klassakh sekventsii” (On Glivenko’s sequent classes), in Logical and Logical-Mathematical Calculus. Part I, Trudy Matematicheskogo Instituta Imeni V. A. Steklova, 98 (1968), 131–154. URL: http://mi.mathnet.ru/tm2930.

[bib.bib37] [37] Fred Richman. Confessions of a formalist, platonist, intuitionist. Unpublished manuscript, April 9, 1994. Formerly available at Richman’s personal website (no longer accessible).

[bib.bib38] [38] Fred Richman. Intuitionism as generalization. Philosophia Mathematica, 5(1–2):124–128, 1990. doi:10.1093/philmat/s2-5.1-2.124.

[bib.bib39] [39] Kimmo I. Rosenthal. Quantales and their Applications, volume 234 of Pitman Research Notes in Mathematics. Longman Scientific & Technical, Essex, 1990.

[bib.bib40] [40] Helmut Schwichtenberg and Stanley S. Wainer. Proofs and Computations. Perspectives in Logic. Cambridge University Press and Association for Symbolic Logic, 2012. doi:10.1017/CBO9781139031905.

[bib.bib41] [41] Krister Segerberg. Propositional logics related to Heyting’s and Johansson’s. Theoria, 34(1):26–61, 1968. doi:10.1111/j.1755-2567.1968.tb00337.x.

[bib.bib42] [42] Harold Simmons. A framework for topology. In Angus Macintyre, Leszek Pacholski, and Jeff Paris, editors, Logic Colloquium ’77, volume 96 of Studies in Logic and the Foundations of Mathematics, pages 239–251. Elsevier, 1978. doi:10.1016/S0049-237X(08)72007-X.

[bib.bib43] [43] Harold Simmons. A curious nucleus. Journal of Pure and Applied Algebra, 214:2063–2073, 2010. doi:10.1016/j.jpaa.2010.02.011.

[bib.bib44] [44] Clifford Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In Jacob C. E. Dekker, editor, Recursive Function Theory, volume 5 of Proceedings of Symposia in Pure Mathematics, pages 1–27. American Mathematical Society, Providence, RI, 1962.

[bib.bib45] [45] Christian Thiel. Die kontroverse um die intuitionistische logik vor ihrer axiomatisierung durch heyting im jahre 1930. History and Philosophy of Logic, 9(1):67–75, 1988. doi:10.1080/01445348808837126.

[bib.bib46] [46] Anne S. Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge University Press, Cambridge, 2nd edition, 2000.

[bib.bib47] [47] Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics: An Introduction, volume I and II. North-Holland, Amsterdam, 1988.

[bib.bib48] [48] Benno van den Berg. A Kuroda-style j-translation. Archive for Mathematical Logic, 58:627–634, 2019. doi:10.1007/s00153-018-0656-x.

[bib.bib49] [49] Peter W. Woodruff. A note on JP’. Theoria, 36:183–184, 1970. doi:10.1111/j.1755-2567.1970.tb00419.x.

A Unifying Conservation Theorem

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 A brief account of conservation results

2.1 Kolmogorov

2.2 Glivenko

2.3 Gödel and Gentzen

2.4 Kuroda

2.5 Segerberg

3 Entailment relations

3.1 Properties of functions

▶ Remark 1.

Lemma 2.

Proof.

▶ Remark 3.

3.2 Minimal logic

Lemma 4.

Proof.

4 Conservation

Proposition 5.

Proof.

Theorem 6 (Conservation).

Proof.

5 From the abstract to the concrete

5.1 Translation theorems in the vein of Kolmogorov and Gentzen

Corollary 7.

Proof.

Lemma 8.

Proof.

Lemma 9.

Proof.

Proposition 10.

Proof.

5.2 Minimality results à la Kuroda–Segerberg

Corollary 11.

Proof.

Lemma 12.

Proof.

Proposition 13.

Proof.

5.3 Glivenko’s theorem

Corollary 14.

Proof.

Proposition 15 (Glivenko [18]).

Proof.

5.4 Kuroda’s negative translation theorem with minimality

Lemma 16.

Proof.

Proposition 17.

Proof.

6 Final remarks

References

Appendix A Technical proof details

Proof of Lemma 4.

Lemma 18.

Proof.

Proof of Lemma 9.

Proof of Lemma 12.

Proof of Lemma 16.

$\blacktriangleright$ Remark 1.

$\blacktriangleright$ Remark 3.