1 Introduction
Glivenko’s theorem says that, in propositional logic, classical provability of a formula entails intuitionistic provability of the double negation of that formula [Reference Glivenko45]. This stood right at the beginning of the success story of negative translations, indeed mainly designed for converting classically derivable formulae into intuitionistically derivable ones. Typically, a negative translation is an operation on formulae in predicate logic such that each formula is classically equivalent to its translation and is classically derivable exactly when the translation is intuitionistically derivable. Negative translations have already been put into the context of nuclei [Reference Escardó and Oliva30, Reference van den Berg114] or nucleus [Reference Escardó and Oliva30], and have proved to be useful also in computer science [Reference Griffin48], set theory [Reference Aczel4], arithmetic and analysis [Reference Spector107], eventually contributing to program extraction [Reference Schwichtenberg and Wainer101] and proof mining [Reference Kohlenbach63]. Double negation over intuitionistic logic is indeed a typical instance of a nucleus [Reference Aczel5, Reference Haykazyan50, Reference Johnstone60, Reference Negri76, Reference Rosenthal93, Reference Simmons, Macintyre, Pacholski and Paris105, Reference Simmons106, Reference van den Berg114].Footnote 1
As compared to recent literature on related topics [Reference Aczel4, Reference Cignoli and Torrens15, Reference Espíndola31, Reference Fellin, Schuster and Wessel36, Reference Galatos and Ono40, Reference Griffin48, Reference Guerrieri and Naibo49, Reference Ishihara and Schwichtenberg57, Reference Litak, Polzer and Rabenstein68, Reference Negri77, Reference Negri78, Reference Ono83, Reference Pereira and Haeusler85, Reference Rump94, Reference Spector107, Reference Torrens111, Reference Zdanowski119], the main purpose of the present work is to generalise Glivenko’s theorem and the theory of negative translations: simultaneously from double negation to an arbitrary nucleus; from provability in a calculus to an abstract consequence relation; and from propositional logic to any set of objects whatsoever. As pointed out by van den Berg [Reference van den Berg114] and Escardó–Oliva [Reference Escardó, Oliva, Ferreira, Löwe, Mayordomo and Gomes29, Reference Escardó and Oliva30], a generalised version of the Gentzen negative translation for arbitrary nuclei is already known in logic [Reference Aczel4], locale theory [Reference Johnstone60] and topos theory [Reference Johnstone62]; and van den Berg himself gives a generalisation of the minimal Kuroda negative translation to nuclei in logic. We aim for a deeper insight into these generalisations, dubbed j-translations, by passing to arbitrary sets endowed with abstract consequence relations.Footnote 2
To this end we move to a nucleus j over a Hertz–Tarski consequence relation in the form of a (single-conclusion) entailment relation
$\rhd $
à la Scott [Reference Cederquist, Coquand, Buss, Hájek and Pudlák14, Reference Scott, Henkin, Addison, Chang, Craig, Scott and Vaught103]. Assuming that
$\rhd $
is inductively generated by axioms and rules, we propose two natural extensions (§2.2):
$\rhd _j$
generalises the provability of double negation, and
$\rhd ^j$
is inductively defined by adding the generalisation of double negation elimination to the inductive definition of
$\rhd $
. By their very definitions,
$\rhd ^j$
satisfies all the axioms and rules of
$\rhd $
, and
$\rhd _j$
satisfies all the axioms of
$\rhd $
. But when does
$\rhd _j$
also satisfy all the rules of
$\rhd $
? Glivenko conservation, Corollary 3.7, says that
$\rhd ^j$
extends
$\rhd _j$
, and that the two relations coincide precisely when
$\rhd _j$
is closed under the non-axiom rules used to inductively generate
$\rhd $
, which of course is the case whenever there are no such non-axiom rules (Corollary 3.8). While it may happen that this closure condition fails, and hence
$\rhd ^j$
is not conservative over
$\rhd _j$
, following Gödel one can ensure conservation by adding to
$\rhd $
suitable rules generalising the double negation shift (Theorem 3.5).
We then investigate into a different generalisation by weakening the conditions on the function: instead of a nucleus j, we consider a j-homogeneous function k and the related entailment relation
$\rhd _{(k)}$
which generalise the Kolmogorov negative translation and its provability. Similarly to the above, we notice that
$\rhd ^j$
extends
$\rhd _{(k)}$
, and that the two relations coincide precisely when
$\rhd _{(k)}$
is closed under the rules that are used to inductively generate
$\rhd $
(Theorem 3.13). A variant of this last result is shown for
$k=jJ$
—which is intended to generalise the Kuroda negative translation—where J is j-homogeneous (Corollary 3.14).
In logic, the prime instance of course is Glivenko’s theorem (Proposition 5.4) as a syntactical conservation theorem (see also [Reference Fellin, Schuster and Wessel36]):
$$\begin{align*} \Gamma\rhd_c\varphi\iff\Gamma\rhd_i\neg\neg\varphi,\end{align*}$$
where
${\rhd _c}$
and
${\rhd _i}$
denote classical and intuitionistic propositional logic. Simultaneously we re-obtain Gödel’s theorem [Reference Gödel46], otherwise ascribed to Gabbay [Reference Gabbay39] (Proposition 5.7), which says that, in predicate logic,
$$\begin{align*} \Gamma\rhd_c\varphi\iff\Gamma\rhd_*\neg\neg\varphi,\end{align*}$$
where
$\rhd _*$
is any extension (by additional axioms) of intuitionistic predicate logic that satisfies the double negation shift:
$$\begin{align*}\forall x\neg\neg\varphi\rhd\neg\neg\forall x\varphi.\end{align*}$$
Next, we regain Kolmogorov’s result [Reference Kolmogorov64] (Proposition 5.8(i)) that, in predicate logic,
$$\begin{align*}\Gamma\rhd_c\varphi\iff k\Gamma\rhd_ik\varphi,\end{align*}$$
where k is the Kolmogorov negative translation inductively defined by
$$ \begin{align*} k\top&= \neg\neg \top, & k\bot&= \neg\neg \bot, & kP&= \neg\neg P, \\ k(\varphi\wedge\psi)&= \neg\neg (k\varphi\wedge k\psi), & k(\varphi\vee\psi)&= \neg\neg (k\varphi\vee k\psi), & k(\varphi\to\psi)&= \neg\neg (k\varphi\to k\psi), \\ k(\forall x\,\varphi)&= \neg\neg \forall x\,k\varphi, & k(\exists x\,\varphi)&= \neg\neg \exists x\,k\varphi. \end{align*} $$
Analogous statements can be made for the Gentzen [Reference Gentzen41, Reference Gentzen42] and for the minimal Kuroda [Reference Kuroda66, Reference Murthy73, Reference van den Berg114] negative translation (Proposition 5.8(ii) and (iii)).
While the double negation nucleus
$j\varphi = \lnot \lnot \varphi $
is an instance of the continuation nucleus, it is tantamount to the same case
$j\varphi = \neg \varphi \to \varphi $
of the Peirce nucleus [Reference Escardó and Oliva30]. What does our main result mean for other nuclei in logic? The open nucleus
$j\varphi = A\to \varphi $
prompts a form of the deduction theorem (Proposition 5.11(i)), while the closed nucleus
$j\varphi = \varphi \vee A$
yields a variant of the reduction from intuitionistic to minimal logic going back to Johansson [Reference Johansson59] (Proposition 5.11(ii)). Last but not least, by observing that the modal operator
$\bigcirc $
in propositional lax logic is a nucleus, we get a general version of strong conservativity [Reference Fairtlough and Mendler32] (Proposition 5.13).
1.1 Preliminaries
We proceed in a constructive and predicative way, keeping the concepts elementary and the proofs direct. If a formal system is desired, our work can be placed in a suitable fragment of Aczel’s Constructive Zermelo–Fraenkel Set Theory (CZF) [Reference Aczel1–Reference Aczel3, Reference Aczel and Rathjen6, Reference Aczel and Rathjen7] based on intuitionistic first-order predicate logic.
By a finite set we understand a set that can be written as
$\{a_1, \dots , a_n\}$
for some
$n \geqslant 0$
. Given any set S, let
$\operatorname {Pow}(S)$
(respectively,
$\operatorname {Fin}(S)$
) consist of the (finite) subsets of S. We thus deviate from the terminology prevalent in constructive mathematics and set theory [Reference Aczel and Rathjen6, Reference Aczel and Rathjen7, Reference Bishop and Bridges11–Reference Bishop13, Reference Lombardi and Quitté69, Reference Mines, Richman and Ruitenburg71]: to reserve the term ‘finite’ to sets which are in bijection with
$\{1,\ldots ,n\}$
for a necessarily unique
$n\ge 0$
. Those exactly are the sets which are finite in our sense and are discrete too, i.e., have decidable equality [Reference Mines, Richman and Ruitenburg71].
2 Entailment relations
Closely following [Reference Fellin, Schuster and Sokolova35, Reference Rinaldi, Schuster and Wessel89, Reference Rinaldi, Schuster and Wessel90] we briefly recall the basics of entailment relations. Let S be a set and
$\rhd \subseteq \operatorname {Pow}(S)\times S$
. Once abstracted from the context of logical formulae, all but one of Tarski’s axioms of consequence [Reference Tarski109]Footnote
3
can be put as
where
$U,V\subseteq S$
and
$a\in S$
. These axioms also characterise a finitary covering or Stone covering in formal topology [Reference Sambin and Skordev95];Footnote
4
see further [Reference Ciraulo, Maietti and Sambin17, Reference Ciraulo and Sambin18, Reference Negri, Ursini and Aglianò75, Reference Negri76, Reference Sambin96, Reference Sambin97]. The notion of consequence has presumably been described first by Hertz [Reference Hertz51–Reference Hertz53] (see also [Reference Béziau, Pouivet and Resbuschi9, Reference Legris and Béziau67]).
Tarski has rather characterised the set of consequences of a set of propositions, which corresponds to the algebraic closure operator
$U\mapsto U^{\rhd }$
on
$\operatorname {Pow}(S)$
of a relation
$\rhd $
as above where
$$\begin{align*}U^{\rhd}=\{a\in S:U\rhd a\}\,. \end{align*}$$
Rather than with Tarski’s notion, we henceforth work with its (tantamount) restriction to finite subsets, i.e., a (single-conclusion) entailment relation.Footnote
5
This is a relation
$\rhd \subseteq \operatorname {Fin}(S)\times S$
such that
for all finite
$U,U',V,V'\subseteq S$
and
$a,b\in S$
, where as usual
$U,V= U\cup V$
and
$V,b= V\cup \{b\}$
. Our focus thus is on finite subsets of S, for which we reserve the letters
$U, V, W, \ldots $
; we sometimes write
$a_1,\ldots ,a_n$
in place of
$\{a_1,\ldots ,a_n\}$
even if
$n=0$
.
Remark 2.1. The rule Refl is equivalent, by Mono, to the axiom
$a\rhd a$
.
Redefining
$$ \begin{align*} T^{\rhd}=\{a\in S:\exists U\in\operatorname{Fin}(T)(U\rhd a)\} \end{align*} $$
for arbitrary subsets T of S gives back an algebraic closure operator on
$\operatorname {Pow}(S)$
. By writing
$T \rhd a$
in place of
$a \in T^{\rhd }$
, the entailment relations thus correspond exactly to the relations satisfying Tarski’s axioms above.
Given an entailment relation
$\rhd $
, by setting
$a \leqslant b = a \rhd b$
we get a preorder on S; whence the conjunction
$a \approx b$
of
$a \leqslant b$
and
$b \leqslant a$
is an equivalence relation.
Quite often an entailment relation
$\rhd $
is inductively generated from axioms by closing up with respect to the three structural rules Refl, Mono and Trans above [Reference Rinaldi and Wessel92]. In the present note some leeway is required by allowing for rules other than Refl, Mono and Trans in the inductive generation of
$\rhd $
. These non-structural rules have the formFootnote
6
As an axiom is nothing but a rule with no premiss, we explicitly use non-axiom rule to indicate a rule that has at least one premiss, whereas in general we do not excluded that a rule be an axiom. If the three structural rules are the only non-axiom rules employed for inductively generating an entailment relation
$\rhd $
, we stress this by saying that
$\rhd $
is generated only by axioms.
Given an inductively generated entailment relation
$\rhd $
and a set of rules
$*$
, then we call
$\rhd $
plus
$*$
the entailment relation
$\rhd _*$
inductively generated by all the rules that either are used for generating
$\rhd $
or belong to
$*$
. We also say that
$\rhd _*$
is an inductive extension of
$\rhd $
, and we call
$*$
the set of additional rules.
A main feature of inductive generation is that if
$\rhd $
is an entailment relation generated inductively by certain rules, then
${\rhd }\subseteq {\rhd '}$
for every entailment relation
${\rhd '}$
satisfying those rules. By an extension
${\rhd '}$
of an entailment relation
${\rhd }$
we mean in general an entailment relation
${\rhd '}$
such that
${\rhd }\subseteq {\rhd '}$
. We say that an extension
${\rhd '}$
of
${\rhd }$
is conservative if also
${\rhd }\supseteq {\rhd '}$
and thus
${\rhd }={\rhd '}$
altogether [Reference Fellin, Schuster and Wessel36, Reference Rinaldi, Schuster and Wessel89, Reference Rinaldi, Schuster and Wessel90].
2.1 Nuclei over entailment relations
In the context of an entailment relation, what do we mean by a nucleus?
Definition 2.2. Given a set S endowed with an entailment relation
$\rhd $
, we say that a function
$j\colon S\to S$
is a nucleus (over
$\rhd $
) if for all
$a,b\in S$
and
$U\in \operatorname {Fin}(S)$
the following hold:
Remark 2.3.
-
(i) By Refl and Trans, the rule Rj can be expressed by an axiom, viz.
(1)
$$ \begin{align} b\rhd jb. \end{align} $$
-
(ii) By Lj, from
$ja\rhd ja$
we get
$j^2a\rhd ja$
and thus
$j^2a\approx ja$
. -
(iii) The rule Rj is tantamount to the inverse of Lj. In particular, we have
where
$jU=\{ju\colon u\in U\}$
and the double line stands for equivalence. This characterisation is already known in particular cases, e.g., the following (iv).
-
(iv) If we consider a structure with a relative pseudo-complement operator, i.e., a binary function
$\to $
that satisfies then it is easy to show that nuclei are characterised by a single equivalence:(2)
$$ \begin{align} a\to jb\approx ja\to jb. \end{align} $$
This was observed, e.g., in [Reference Johnstone, Herrlich and Porst61, Reference Johnstone62, Reference Macnab70] for nuclei in locale theory. In fact, by means of Trans and RPC, (2) is another way of writing Lj and its inverse, which, as noticed in (ii), is tantamount to Rj. Moreover, the following hold by means of RPC, Lj and Rj:
(3)
$$ \begin{align} j(a\to b)&\rhd a\to jb, \end{align} $$
(4)
$$ \begin{align} j(a\to b)&\rhd ja\to jb. \end{align} $$
Note that (3) and (4) are equivalent in view of (2). As we will see in the applications (§5), the converses of (3) and (4) do not hold in general.
Example 2.4. The above notion of a nucleus includes as a special case the notion of a nucleus over a locale [Reference Aczel5, Reference Jibladze and Johnstone58, Reference Johnstone60–Reference Johnstone62, Reference Negri76, Reference Picado and Pultr86, Reference Rosenthal93, Reference Simmons, Macintyre, Pacholski and Paris105, Reference Simmons106], which is well-known as a point-free way to put subspaces. In fact, if S is a locale with partial order
$\leqslant $
, then
$$\begin{align*}U\rhd a\iff \bigwedge U\leqslant a\end{align*}$$
defines an entailment relation [Reference Coquand, Zhang, Clote and Schwichtenberg27] such that any given map
$j:S\to S$
is a nucleus over
$\rhd $
precisely when
$j$
is a nucleus over the locale S. The latter means that j satisfies
$$ \begin{align} ja\wedge jb\leqslant j(a\wedge b) \end{align} $$
on top of the conditions for j being a closure operator on S, which can be put as
$a\leqslant ja$
and
$$ \begin{align} a\leqslant jb\implies ja\leqslant jb\,. \end{align} $$
In the presence of
$a\leqslant ja$
, which corresponds to Rj in the form of (1), the conjunction of (5) and (6) is equivalent to
$$ \begin{align*} c\wedge a\leqslant jb\implies c\wedge ja\leqslant jb\,, \end{align*} $$
which in turn subsumes Lj. So the two notions of a nucleus coincide.
Example 2.5.
-
(i) Every entailment relation
$\rhd $
has the trivial nucleus
$j=\operatorname {\mathrm {id}}$
. -
(ii) Let an algebraic structure
$\mathbf {S}$
come with a unary self-inverse function j (e.g., take a group as
$\mathbf {S}$
and the inverse as j). The entailment relation
$\rhd $
of
$\mathbf {S}$
-substructures is inductively defined by (7)for every n-ary function f characteristic of
$$ \begin{align} a_1,\dots,a_n\rhd f(a_1,\dots,a_n) \end{align} $$
$\mathbf {S}$
, including j. Then j is a nucleus over
$\rhd $
. Axiom (1) is just (7) for
$f= j$
, therefore the rule Rj holds. In particular,
$j^2=\operatorname {\mathrm {id}}$
implies
$j(a)\rhd a$
, which, together with Trans, gives the rule Lj.
-
(iii) Double negation
$\neg \neg $
is a nucleus over intuitionistic logic
$\rhd _i$
as an entailment relation between propositional or first-order predicate formulae (see §5.2 for further details).
2.2 Extensions induced by nuclei
Every nucleus over
$\rhd $
induces two natural extensions of
$\rhd $
as follows.
Definition 2.6. Let j be a nucleus over an entailment relation
$\rhd $
on a set S. We understand by:
-
– the weak
$j$
-extension (or Kleisli extension) of
$\rhd $
the relation
${\rhd _j}\subseteq \operatorname {Fin}(S)\times S$
defined by
$$ \begin{align*} U\rhd_ja\iff U\rhd ja; \end{align*} $$
-
– the strong
$j$
-extension of
$\rhd $
the entailment relation
${\rhd ^j}\subseteq \operatorname {Fin}(S)\times S$
inductively generated by the rules of
$\rhd $
together with the stability axiom for j: (8)In the terminology coined before,
$$ \begin{align} ja\rhd^ja. \end{align} $$
${\rhd ^j}$
is nothing but
$\rhd $
plus the stability axiom for j.
As we will see later on (Corollary 3.7),
$$\begin{align*} {\rhd}\subseteq{\rhd_j}\subseteq{\rhd^j}.\end{align*} $$
Lemma 2.7. Let S be a set with an entailment relation
$\rhd $
and let j be a nucleus over
$\rhd $
. Then both
$\rhd ^j$
and
$\rhd _j$
are entailment relations that extend
$\rhd $
.
Proof. The statement for
$\rhd ^j$
holds by the very definition of
$\rhd ^j$
. As for
$\rhd _j$
: By (1) and Remark 2.1, Refl carries over to
$\rhd $
from
$\rhd _j$
. Mono is inherited from
$\rhd $
, and so is Trans in view of L
$j$
:
Finally, also
${\rhd }\subseteq {\rhd _j}$
is a consequence of (1).
Remark 2.8.
-
(i) Stability and Rj together give
$a\approx ^jja$
, where
$\approx ^j$
is the intersection of
$\rhd ^j$
and its converse on singletons. -
(ii) By Refl in the form of
$a\rhd a$
(Remark 2.1), stability holds for
$\rhd _j$
too, that is,
$ja\rhd _ja$
.
Under appropriate circumstances, Remark 2.8 will help to obtain
${\rhd ^j}\subseteq {\rhd _j}$
(see Corollaries 3.7 and 3.8).
Remark 2.9. The nucleus j on
$\rhd $
is a nucleus also on
$\rhd _j$
and
$\rhd ^j$
. In fact, by Lemma 2.7 both extensions inherit axiom (1) from
$\rhd $
, and actually satisfy the following strengthening of Lj:
While L
$j^+$
for
$\rhd _j$
is just
$Lj$
for
$\rhd $
, stability
$ja\rhd a$
is tantamount to L
$j^+$
for any entailment relation
$\rhd $
whatsoever.
To better understand whether and when
$\rhd _j$
coincides with
$\rhd ^j$
, we first study a concrete example.
Example 2.10. Consider deduction in minimal propositional logic
$\rhd _m$
with the closed nucleus
$c_\bot \colon \varphi \mapsto \varphi \vee \bot $
(see §5.3 for details). This
$\rhd _m$
is inductively generated by certain axioms plus the rule
which cannot be expressed as an axiom. By its very definition,
$\rhd _m^{c_{\bot }}$
too satisfies R
$\to $
. Does also
$\rhd _{mc_{\bot }}$
satisfy this rule? If this were the case, then by definition of
$\rhd _{mc_{\bot }}$
we would have
As
$\bot \rhd _m\psi \vee \bot $
, we would obtain
${}\rhd_m(\bot\to\psi)\vee\bot $
. However, since minimal logic has the disjunction property and neither disjunct is provable in general, this cannot be the case. So
$\rhd _{c_{\bot }}$
does not satisfy the rule R
$\to $
.
The moral of Example 2.10 is that
$\rhd $
may already have non-axiom rules, such as R
$\to $
, which carry over to
$\rhd ^j$
by its very definition, and thus need to hold in
$\rhd _j$
too for the former to be conservative over the latter. To deal with this issue, we introduce the following concept.
Definition 2.11. We say that a rule r that holds for
$\rhd $
is compatible with j over
$\rhd $
if r also holds for
$\rhd _j$
. We usually omit “over j” if this is clear from the context.
Remark 2.12.
-
(i) Refl, Mono, Trans are compatible with every nucleus j, by Lemma 2.7.
-
(ii) Every composition r of compatible rules is compatible. In fact, the derivation that gives r in
$\rhd $
can be translated smoothly into
$\rhd _j$
, as all the applied rules are compatible.This is very useful: to check compatibility for all the rules of an entailment relation
$\rhd $
, it suffices to check compatibility for any set of rules that generate
$\rhd $
. -
(iii) Each axiom
$a_1,\dots ,a_n\rhd b$
can be viewed as a rule with no premiss, and as such is compatible with any given nucleus j, simply by Rj. It follows that, if an entailment relation
$\rhd $
is generated only by axioms, then every rule that holds for
$\rhd $
is compatible with any nucleus j over
$\rhd $
.
2.3 Homogeneous functions and translations
Throughout this subsection, let
$j$
be a nucleus over an entailment relation
$\rhd $
on a set S.
Definition 2.13. We say that a function
$k\colon S\rightarrow S$
is:
-
– j-homogeneous (from
$\rhd ^j$
to
$\rhd $
) if
$k$
satisfies the following two conditions: (9)
$$ \begin{align} kja&\rhd ka, \end{align} $$
(10)
$$ \begin{align} a&\approx^j ka. \end{align} $$
-
– A j-translation (from
$\rhd ^j$
to
$\rhd $
) if
$k$
satisfies (10) and (11)
Remark 2.14.
-
(i) Condition (10) implies the converse of (11), that is,
In fact, since
$\rhd ^j$
extends
$\rhd $
, we have that
$kU\rhd kb$
implies
$kU\rhd ^jkb$
, which is equivalent to
$U\rhd ^jb$
by means of
$a\approx ^jka$
. -
(ii) The nucleus j is j-homogeneous: it follows immediately from
$j^2a\rhd ja$
(Remark 2.3(ii)) and
$a\approx ^jja$
(Remark 2.8). -
(iii) Every j-translation is j-homogeneous: by applying (11) to (8) we get (9).
-
(iv) The nucleus j is a j translation precisely when
-
(v) We have seen that j-translations are j-homogeneous. We want to stress that the two notions are distinct via a counterexample. The closed nucleus
$c_\bot \colon \varphi \mapsto \varphi \vee \bot $
over minimal propositional logic
$\rhd _m$
is
$c_\bot $
-homogeneous by (ii) but it is not a
$c_\bot $
-translation: this is a direct consequence of Corollary 3.7 and the fact that R
$\to $
is not compatible with
$c_\bot $
(see Example 2.10). -
(vi) Every j-translation k that satisfies Rk also satisfies Lk. In fact:
Where
$(*)$
is subsequent applications of Trans with for each
$u\in U$
. It follows that a j-translation k is a nucleus if and only if it satisfies Rk.
3 Conservation as translation
We next present a few conservation theorems for nuclei, typically giving necessary and sufficient conditions. Throughout this section, let S be a set with an entailment relation
$\rhd $
inductively generated by rules, and let
$j$
be a nucleus over
$\rhd $
.
3.1 Glivenko and Gödel conservation
Definition 3.1. Given a rule
to obtain its
$j$
-version
$r_j$
we put
$j$
in front of every consequent:
Remark 3.2.
-
(i) By definition of
$\rhd _j$
, the j-version
$r_j$
holds for
$\rhd $
if and only if the original rule r holds for
$\rhd _j$
. This means that if r holds for
$\rhd $
, then r is compatible with j over
$\rhd $
if and only if
$r_j$
holds for
$\rhd $
. -
(ii) By
$j^2a\approx ja$
(Remark 2.3(iii)),
$r_{jj}$
holds for
$\rhd $
if and only if
$r_{j}$
holds for
$\rhd $
. In particular,
$r_j$
is compatible with j over
$\rhd $
if and only if
$r_j$
holds for
$\rhd $
. -
(iii) By
$ja\approx ^ja$
(Remark 2.8), if r holds for
$\rhd $
, then
$r_j$
holds for
$\rhd ^j$
.
Definition 3.3. Given an entailment relation
$\rhd $
generated by rules, let its intermediate
$j$
-extension
$\rhd _{\langle j\rangle }$
be
$\rhd $
plus the j-version
$r_j$
of all the rules r in the inductive definition of
$\rhd $
.
Remark 3.4.
-
(i) We have
${\rhd }\subseteq {\rhd _{\langle j\rangle }}\subseteq {\rhd ^j}$
by Remark 3.2(iii). -
(ii) By Remarks 2.12 and 3.2(i), to obtain
$\rhd _{\langle j\rangle }$
it suffices to add the j-version of all the non-axiom rules in the inductive definition of
$\rhd $
that are not already compatible with j.
Theorem 3.5 (Gödel conservation).
Let
$\rhd _*$
be
$\rhd $
plus additional rules that hold for
$\rhd ^j$
and such that j is a nucleus also over
$\rhd _*$
. Then
${\rhd _*^j}={\rhd ^j}$
; in particular,
${\rhd ^j}$
extends
${\rhd _{*j}}$
, that is,
${\rhd _{*j}}\subseteq {\rhd ^j}$
. Moreover, the following are equivalent:
-
(a)
${\rhd ^j}$
is conservative over
${\rhd _{*j}}$
, that is,
${\rhd ^j}\subseteq {\rhd _{*j}}$
; -
(b) the nucleus j is a j-translation from
$\rhd ^j$
to
$\rhd _*$
; -
(c)
${\rhd _{*j}}$
is an inductive extension of
${\rhd _*}$
; -
(d) all the non-axiom rules that generate
$\rhd _*$
are compatible with j over
$\rhd _*$
, that is, they hold for
$\rhd _{*j}$
; -
(e)
${\rhd _*}$
is an extension of
${\rhd _{\langle j\rangle }}$
, that is,
${\rhd _{\langle j\rangle }}\subseteq {\rhd _*}$
.
Proof. First, note that
${\rhd }\subseteq {\rhd _*}\subseteq {\rhd ^j}$
. Since
$\rhd \subseteq \rhd _*$
, we have
${\rhd ^j}\subseteq {\rhd _*^j}$
. On the other hand, as stability and all the rules of
$\rhd _*$
hold for
$\rhd ^j$
, we also have
${\rhd _*^j}\subseteq {\rhd ^j}$
. Therefore
${\rhd _*^j}={\rhd ^j}$
.
Since
$a\approx _*^jja$
by Remark 2.8(i), (b) is tantamount to
which by the inverse of L
$j$
(see Remark 2.3(iii)) is equivalent to (a).
As
${\rhd ^j}$
is an inductive extension of
$\rhd _*$
, (c) follows from (a); and (c) trivially entails (d).
To deduce (a) from (d), assume (d) and consider one by one the rules that generate
$\rhd ^j$
: Refl, Mono, Trans hold for
$\rhd _j$
since
$\rhd _j$
is an entailment relation by Lemma 2.7; stability (8) holds for
$\rhd _j$
by Remark 2.8(i); all the rules that generate
$\rhd _*$
hold for
$\rhd _j$
since they are either compatible with
$j$
by assumption (d), or axioms and thus compatible with
$j$
by Remark 2.12(iii). As
$\rhd ^j$
is the smallest extension of
$\rhd _*$
satisfying all these rules, we obtain (a).
By Remark 3.2(ii) with
${\rhd _{\langle j\rangle }}$
in place of
${\rhd }$
, (d) and thus (a) hold with
$\langle j\rangle $
in place of
$*$
. So, if (e), then
$$\begin{align*} {\rhd^j}={\rhd_{\langle j\rangle j}}\subseteq{\rhd_{*j}}\subseteq{\rhd^j}\end{align*}$$
(see also Figure 1); whence (a).
Figure 1 Diagram of the entailment relations involved in the situation of Theorem 3.5. A solid arrow denotes a strong j-extension, a dashed arrow denotes a weak j-extension, a dotted arrow denotes a generic extension, and a double line denotes a conservative extension. The intuition is that, if the outer triangle does not satisfy the desired properties, then we can move to an inner triangle that works.
To obtain (e) from (d), suppose (d) and let
$r$
be a rule in the inductive definition of
$\rhd $
. By (d),
$r$
holds for
$\rhd _{*j}$
which, by Remark 3.2(i) with
${\rhd _{*}}$
in place of
${\rhd }$
means that
$r_j$
holds for
$\rhd _{*}$
. Hence all the rules of
$\rhd _{\langle j\rangle }$
hold for
$\rhd _*$
, and thus (e).
Remark 3.6. Let
$\rhd _*$
be an inductive extension of
$\rhd $
.
-
(i) For j to be a nucleus over
$\rhd _*$
too, it is sufficient to check Lj. In fact, Rj is tantamount to (1), which as an axiom is inherited by
$\rhd _*$
from
$\rhd $
by the very definition of extension. -
(ii) Lj is trivially satisfied whenever
$*=\emptyset $
. -
(iii) If Lj can be proved admissible for
$\rhd $
by exclusively composing the generating rules of
$\rhd $
, then the same composition equally shows that Lj is admissible for
$\rhd _*$
.
Corollary 3.7 (Glivenko conservation).
${\rhd ^j}$
extends
${\rhd _j}$
, that is,
${\rhd _j}\subseteq {\rhd ^j}$
; and the following are equivalent:
-
(a)
${\rhd ^j}$
is conservative over
${\rhd _j}$
, that is,
${\rhd ^j}\subseteq {\rhd _j}$
; -
(b) the nucleus j is a j-translation from
$\rhd ^j$
to
$\rhd $
; -
(c)
${\rhd _j}$
is an inductive extension of
${\rhd }$
; -
(d) all the non-axiom rules that generate
$\rhd $
are compatible with j, that is, they hold for
$\rhd _j$
; -
(e)
${\rhd _{\langle j\rangle }}$
is conservative over
${\rhd }$
, that is,
${\rhd _{\langle j\rangle }}\subseteq {\rhd }$
.
Proof. This is Theorem 3.5 with
${\rhd _*}={\rhd }$
.
Corollary 3.8. If
$\rhd $
is inductively generated only by axioms, then j is a j-translation and
$\rhd ^j$
is a conservative extension of
$\rhd _j$
, that is,
${\rhd ^j}={\rhd _j}$
.
3.2 Kolmogorov and Kuroda conservation
We now generalise Corollary 3.7 from the nucleus
$j$
to a
$j$
-homogeneous function.
Definition 3.9. For the given nucleus j over an entailment relation
$\rhd $
, and any function
$k\colon S\rightarrow S$
whatsoever, we define the relation
${\rhd _{(k)}}\subseteq \operatorname {Fin}(S)\times S$
by
$$\begin{align*} U\rhd_{(k)}a\iff kU\rhd ka. \end{align*} $$
Definition 3.10. Given a rule r that holds for
$\rhd $
, we say that:
-
– r is Kolmogorov compatible with
$k$
(over
$\rhd $
) if it also holds for
$\rhd _{(k)}$
, -
– r is
$j$
-Kuroda compatible with
$k$
(over
$\rhd $
) if it also holds for
$\rhd _{j(k)}$
.
We thus have an analogue of Remark 2.12:
Remark 3.11.
-
(i) Refl, Mono, Trans are trivially Kolmogorov compatible with
$k$
. This means that
$\rhd _{(k)}$
is an entailment relation; however in general it is not an extension of the original
$\rhd $
. -
(ii) Compatibility entails j-Kuroda compatibility, hence Refl, Mono, Trans are Kuroda compatible with
$k$
by Remark 2.12. -
(iii) Every composition r of Kolmogorov (resp. j-Kuroda) compatible rules is Kolmogorov (resp. j-Kuroda) compatible. In fact, the derivation that gives r in
$\rhd $
can be translated smoothly into
$\rhd _{(k)}$
(resp.
$\rhd _{j(k)}$
), as all the applied rules are Kolmogorov (resp. j-Kuroda) compatible.This means that if we want to check Kolmogorov (resp. j-Kuroda) compatibility for all the rules of an entailment relation
$\rhd $
, it suffices to check it for any set of rules that generate
$\rhd $
.
Remark 3.12. Remark 2.3(iii) yields
${\rhd _{(jk)}}={\rhd _{j(k)}}$
and
${\rhd _{(j)}}={\rhd _j}$
.
Theorem 3.13 (Kolmogorov conservation).
Let
$k\colon S\rightarrow S$
be j-homogeneous. Then
${\rhd ^j}$
extends
${\rhd _{(k)}}$
, that is,
${\rhd _{(k)}}\subseteq {\rhd ^j}$
; and the following are equivalent:
-
(a)
${\rhd ^j}$
is conservative over
${\rhd _{(k)}}$
, that is,
${\rhd ^j}\subseteq {\rhd _{(k)}}$
; -
(b) the j-homogeneous function
$k$
is a j-translation; -
(c)
${\rhd _{(k)}}$
is an inductive extension of
${\rhd }$
; -
(d) all the rules in the inductive definition of
$\rhd $
are Kolmogorov compatible with
$k$
, that is, they hold for
$\rhd _{(k)}$
.
Proof. The fact that
${\rhd _{(k)}}\subseteq {\rhd ^j}$
is just Remark 2.14(i). The implications from (a) to (c) and from (c) to (d) hold just as in Theorem 3.5. Suppose that all the non-structural rules in the inductive definition of
$\rhd $
are Kolmogorov compatible with k, and that
$U\rhd ^jb$
. We show that
$kU\rhd kb$
by induction on the derivation of
$U\rhd ^jb$
: the cases involving structural rules are trivial; the case of the stability axiom
$ja\rhd ^ja$
is tantamount to
$kja\rhd ka$
, which holds since k is
$j$
-homogeneous; consider the case in which
$U\rhd ^jb$
is derived from a non-structural rule
$r$
in the inductive definition of
$\rhd $
, i.e.,
then
where r can be applied because of the Kolmogorov compatibility. This proves that (d) implies (b). Finally, the fact that (b) implies (a) is just (11).
By setting
$k=j$
in Theorem 3.13, by Remark 3.12 we have
${\rhd _{(j)}}={\rhd _j}$
, which in particular means that compatibility and Kolmogorov compatibility are equivalent. Therefore Corollary 3.7 except for condition (e) is a special case of Theorem 3.13.
Corollary 3.14 (Kuroda conservation).
Let S be a set with an entailment relation
$\rhd $
inductively generated by rules, and let j be a nucleus over
$\rhd $
. Let
$J\colon S\rightarrow S$
be j-homogeneous. Then
${\rhd ^j}$
is an extension of
${\rhd _{j(J)}}$
, that is,
${\rhd _{j(J)}}\subseteq {\rhd ^j}$
; and the following are equivalent:
-
(a)
${\rhd ^j}$
is conservative over
${\rhd _{j(J)}}$
, that is,
${\rhd ^j}\subseteq {\rhd _{j(J)}}$
; -
(b) the function
$jJ$
is a j-translation; -
(c)
${\rhd _{j(J)}}$
is an inductive extension of
${\rhd }$
; -
(d) all the non-structural rules in the inductive definition of
$\rhd $
are Kuroda j-compatible with J, that is, they hold for
$\rhd _{j(J)}$
.
4 Logic as entailment
We now want to see how the conservation results that we have just proved apply to logic.
Throughout this section and the following one, if not stated otherwise, the overall assumption is that S is a set of propositional formulae containing
$\top ,\bot $
and closed under the connectives
$\vee ,\wedge ,\to $
.Footnote
7
By minimal (propositional) logic
$\rhd _m$
we mean the fragment of propositional intuitionistic logic without the principle of ex falso sequitur quodlibet. More precisely, we define
$\rhd _m$
as the least entailment relation
$\rhd $
that satisfies the deduction theorem
and the following axioms:
$$ \begin{align*} \varphi,\psi&\rhd\varphi\wedge\psi, &\varphi\wedge\psi&\rhd\varphi, &\varphi\wedge\psi&\rhd\psi, \\ \varphi&\rhd\varphi\vee\psi, &\psi&\rhd\varphi\vee\psi, &\varphi\vee\psi,\varphi\to\delta,\psi\to\delta&\rhd\delta, \\ \varphi,\varphi\to\psi&\rhd\psi, \\ &\rhd\top. \end{align*} $$
Of course, we understand this as an inductive definition. In this setting, negation
$\neg $
is not given as a primitive operator, but it is rather defined by
$$\begin{align*} \neg\varphi=\varphi\to\bot.\end{align*} $$
The above system for minimal logic is equivalent to the
$\mathbf {G3}$
-style calculus in Table 1; meaning that they inductively generate the same entailment relation.
Table 1 Sequent calculus-like rules for minimal propositional logic.
Figure 2 Diagram of the logics introduced in §4, mostly based on [Reference Odintsov81, figure 4.1].
We define the following inductive extensions of minimal logic
$\rhd _{m}$
:
For a discussion of these and other logics, see [Reference Odintsov81, Reference Odintsov82], from whom we took the names for
$\rhd _g$
and
$\rhd _n$
. See also Figure 2 to see how they are related.
4.1 Predicate and infinitary extensions
Let
$\rhd _*$
be an inductive extension of
$\rhd _m$
. When we say that we work in predicate logic, we mean that we add quantifiers
$\forall $
and
$\exists $
to the language, and hence require that the formulae in S are closed under
$\forall ,\exists $
as well. Moreover, we extend the inductive definition of
$\rhd _*$
by adding the rule
with the condition that y has to be fresh, and the following axioms:
$$ \begin{align*} \forall x\varphi&\rhd\varphi[t/x], \\\varphi[t/x]&\rhd\exists x\varphi, \\\exists x\varphi,\forall x(\varphi\to\delta)&\rhd\delta, \end{align*} $$
where the latter comes with the condition that x cannot be free in
$\delta $
. Over
$\rhd _*$
, these axioms and rule are equivalent to the
$\mathbf {G3}$
-style rules in Table 2.
The definition of a nucleus
$j$
given in [Reference van den Berg114] requires
$j$
to be compatible with substitution, that is,
$$\begin{align*} j(\varphi[t/x])=(j\varphi)[t/x].\end{align*} $$
We prefer not to have this as a general assumption, but to make explicit whenever we need it.
Table 2 Sequent calculus-like rules for quantifiers. Rules R
$\forall $
and L
$\exists $
come with the condition that y has to be fresh.
When we say that we work in infinitary logic, we mean that we add infinitary connectives
$\bigwedge _{i\in \mathbb {N}}$
and
$\bigvee _{i\in \mathbb {N}}$
to the language, and hence require that the formulae in S are closed under
$\bigwedge _{i\in \mathbb {N}},\bigvee _{i\in \mathbb {N}}$
as well. Moreover, we extend the inductive definition of
$\rhd _*$
by adding the rule
and the following axioms:
$$ \begin{align*} \bigwedge_{i\in\mathbb{N}}\varphi_i&\rhd\varphi_n&\text{for every }n\in\mathbb{N,} \\ \varphi_n&\rhd\bigvee_{i\in\mathbb{N}}\varphi_i&\text{for every }n\in\mathbb{N,} \\ \bigvee_{i\in\mathbb{N}}\varphi_i,\bigwedge_{i\in\mathbb{N}}(\varphi_i\to\delta)&\rhd\delta. \end{align*} $$
Over
$\rhd _*$
, these axioms and rule are equivalent to the
$\mathbf {G3}$
-style rules in Table 3.
Table 3 Sequent calculus-like rules for quantifiers. For each
$n\in \mathbb {N}$
there is one rule L
${ \bigwedge }_n$
and one rule R
${ \bigvee }_n$
.
5 Nuclei in logic
Among the logical rules seen in §4, R
$\to $
, R
$\forall $
and R
$\bigwedge $
are the only ones that cannot be expressed as axioms. Therefore, when checking compatibility of rules with
$j$
, if we do not add other rules that cannot be expressed as axioms, then the only rules we have to deal with are these three.
Lemma 5.1 (Compatibility criterion).
Let
$\rhd $
be an inductive extension of
$\rhd _m$
, and let j be a nucleus over
$\rhd $
.
-
(i) In either propositional, predicate or infinitary logic, R
$\to $
is compatible with j if and only if
$$\begin{align*} \varphi\to j\psi\rhd j(\varphi\to\psi).\end{align*}$$
-
(ii) In predicate logic, if j is compatible with substitution, that is,
then R
$$\begin{align*} j(\varphi[t/x])=(j\varphi)[t/x],\end{align*} $$
$\forall $
is compatible with j if and only if
$$\begin{align*} \forall xj\varphi\rhd j\forall x\varphi.\end{align*}$$
-
(iii) In infinitary logic, R
$\bigwedge $
is compatible with j if and only if
$$\begin{align*} \bigwedge_{i\in\mathbb{N}}j\varphi_i\rhd j\bigwedge_{i\in\mathbb{N}}\varphi_i.\end{align*}$$
Proof. We only prove (i), as the proof of (ii) and (iii) is similar. Suppose that R
$\to $
is compatible with
$j$
. Then:
Now suppose that
$\varphi \to j\psi \rhd j(\varphi \to \psi )$
. Then:
5.1 Some notable translations in logic
We now consider predicate logic. We introduce some classes of functions that generalise some well-known negative translations. Let
$\rhd $
be either
$\rhd _m$
or
$\rhd _i$
. Given a nucleus
$j$
on
$\rhd $
, we inductively define
$k,g,t,J\colon S\rightarrow S$
as follows:
$$ \begin{align*} kP&= jP, & gP&= jP, & tP&= jP, & JP&= P, \\ k\top&= j\top, & g\top&= j\top, & t\top&= j\top, & J\top&= \top, \\ k\bot&= j\bot, & g\bot&= j\bot, & t\bot&= j\bot, & J\bot&= \bot, \\ k(\varphi\wedge\psi)&= j(k\varphi\wedge k\psi), & g(\varphi\wedge\psi)&= g\varphi\wedge g\psi, & t(\varphi\wedge\psi)&= t\varphi\wedge t\psi, & J(\varphi\wedge\psi)&= J\varphi\wedge J\psi \\ k(\varphi\vee\psi)&= j(k\varphi\vee k\psi), & g(\varphi\vee\psi)&= j(g\varphi\vee g\psi), & t(\varphi\vee\psi)&= t\varphi\vee t\psi, & J(\varphi\vee\psi)&= J\varphi\vee J\psi \\ k(\varphi\to\psi)&= j(k\varphi\to k\psi), & g(\varphi\to\psi)&= g\varphi\to g\psi, & t(\varphi\to\psi)&= t\varphi\to t\psi, & J(\varphi\to\psi)&= J\varphi\to jJ\psi, \\ k(\forall x\,\varphi)&= j\forall x\,k\varphi, & g(\forall x\,\varphi)&=\forall x\,g\varphi, & t(\forall x\,\varphi)&= \forall x\,t\varphi, & J(\forall x\,\varphi)&=\forall x\,jJ\varphi, \\ k(\exists x\,\varphi)&= j\exists x\,k\varphi, & g(\exists x\,\varphi)&= j(\exists x\,g\varphi), & t(\exists x\,\varphi)&= \exists x\,t\varphi, & J(\exists x\,\varphi)&=\exists x\,J\varphi. \end{align*} $$
The Kolmogorov j-function k is named after the Kolmogorov negative translation, which is k obtained for
$j=\neg \neg $
, as seen in Proposition 5.8(i). A refined version of the Kolmogorov
$j$
-function is the Gentzen j-function g, named after the Gentzen negative translation, which is g obtained for
$j=\neg \neg $
, as seen in Proposition 5.8(ii). An even more refined version is the prime j-function t which, however, does not provide a
$j$
-translation for
$j=\neg \neg $
as the Gentzen negative translation is known to be minimal in this sense [Reference Ferreira, Oliva, Berger, Diener, Schuster and Seisenberger37]. Finally, we call J the Kuroda j-function. Its definition follows van den Berg [Reference van den Berg114], and is based on the minimal Kuroda negative translation, which is
$jJ$
for
$j=\neg \neg $
, as seen in Proposition 5.8(iii).
Remark 5.2.
-
(i) The following hold for all
$\varphi \in S$
:
$\varphi \approx ^jt\varphi ,$
$\varphi \approx ^jk\varphi ,$
$\varphi \approx ^jg\varphi ,$
$\varphi \approx ^jJ\varphi .$
It follows that
$t,k,g,J$
are j-homogenous exactly when they satisfy (9). -
(ii) Every rule in the inductive definition of
$\rhd $
is Kolmogorov compatible with
$t,k,g$
. This, together with (i) and Theorem 3.13, implies that
$t,k,g$
are j-translations exactly when they satisfy (9). -
(iii) Every rule in the inductive definition of
$\rhd $
is Kuroda j-compatible with J. This, together with (i) and Corollary 3.14, implies that
$jJ$
is a j-translation exactly when J satisfies (9).
Proof. The properties in (i) are readily seen by induction on
$\varphi $
. We refer to [Reference Fellin33, appendix A] for (ii) and (iii).Footnote
8
5.2 The continuation nucleus and the Glivenko nucleus
Let
$\rhd _*$
be an inductive extension of
$\rhd _m$
, and fix a formula
$\alpha $
. The continuation nucleus
$$\begin{align*} g_\alpha\colon\varphi\mapsto(\varphi\to\alpha)\to\alpha\end{align*}$$
has as special case the Glivenko nucleus [Reference Rosenthal93, Reference van den Berg114]
$$ \begin{align*}g_\bot\colon\varphi\mapsto\neg\neg\varphi\,. \end{align*} $$
While
$g_\alpha $
is well-known to be a nucleus whenever
$\rhd _*$
is
$\rhd _m$
,
$\rhd _i$
or
$\rhd _c$
(see, e.g., [Reference van den Berg114]), to be sure (Remark 3.6) that this is the case for every inductive extension
$\rhd _*$
of
$\rhd _m$
we give a proof in which we only use generating rules of
$\rhd _m$
; in fact, Trans and R
$\to $
suffice together with modus ponens.
Lemma 5.3.
$g_\alpha $
is a nucleus over
$\rhd _*$
for every formula
$\alpha $
.
Proof. R
$g_\alpha $
:
L
$g_\alpha $
:
5.2.1 The intuitionistic case: Glivenko’s theorem
Take propositional intuitionistic logic
$\rhd _i$
as
$\rhd $
. As stability (8) equals double negation elimination (16), the strong extension
$\rhd _i^{g_\bot }$
of intuitionistic logic
$\rhd _i$
is classical logic
$\rhd _c$
.
Proposition 5.4 (Glivenko’s theorem [Reference Glivenko44, Reference Glivenko45]).
In propositional logic,
$$\begin{align*} \Gamma\rhd_c\varphi\iff\Gamma\rhd_i\neg\neg\varphi.\end{align*}$$
Proof. Since
$\varphi \to \neg \neg \psi \rhd _i\neg \neg (\varphi \to \psi )$
holds, e.g., by [Reference van Dalen113, lemma 6.2.2], in view of Lemma 5.1(i) R
$\to $
is compatible with
$\neg \neg $
, and we get the claim as an instance of Corollary 3.7.
That
$\neg \neg $
is a
$\neg \neg $
-translation (Corollary 3.7(b)) is the alternative formulation of Glivenko’s theorem
$$\begin{align*} \Gamma\rhd_c\varphi\Longrightarrow\neg\neg\Gamma\rhd_i\neg\neg\varphi.\end{align*}$$
5.2.2 Glivenko’s theorem in general algebra
We compare our approach with some occurrences of Glivenko’s theorem in universal algebra, starting from Birkhoff’s presentation [Reference Birkhoff10, chap. IX, theorem 16]:
In any pseudo-complemented distributive lattice L, the correspondence
$a\mapsto a^{**}$
is a closure operation in L, and a lattice-homomorphism of L onto the complete Boolean algebra of “closed” elements.
As far as we see, this falls somewhat short of capturing Glivenko’s theorem: Any nucleus
$j\colon S\to S$
whatsoever on a frame S is a closure operator and induces a frame homomorphism
$S\to S_j$
onto the frame
$S_j=\{a\in S\colon ja=a\}$
in which the join of
$C\subseteq S_j$
is
$j(\bigvee C)$
, where
$\bigvee $
denotes the join in
$S_j$
, see, e.g., [Reference Johnstone60, Subsection II.2.2]. As Birkhoff has noticed, moreover,
$(a\vee a^*)^{**}=1$
for every (not necessarily closed) element a, yet we do not see any trace of Glivenko’s theorem. The situation changes with later adaptions such as Esakia’s [Reference Esakia28, Section A.2]:
Let H be a Heyting algebra and
$Rg(H)$
the set of all its regular elements, i.e.,
$$\begin{align*} Rg(H)=\{\neg a\colon a\in H\}.\end{align*} $$
It is known that
$Rg(H)$
is a Boolean algebra and that the map
$h\colon H\to Rg(H)$
, given by
$ha=\neg \neg a\ (a\in H)$
, is a surjective homomorphism of the Heyting algebra H onto the Boolean algebra
$Rg(H)$
.
Rather than that the regular elements form a Boolean algebra [Reference Bezhanishvili and Holliday8], the crucial issue for Glivenko’s theorem is that double negation is a morphism of Heyting algebras, more precisely that double negation commutes with implication:
$$ \begin{align} \neg\neg(\varphi\to\varphi)\approx_i \neg\neg\varphi\to \neg\neg\psi. \end{align} $$
We notice that by Remark 2.3(iv) the left-to-right direction of (19) is a general property of nuclei, whereas the right-to-left direction is equivalent to
$$ \begin{align} \varphi\to\neg\neg\psi\rhd_i\neg\neg(\varphi\to\psi), \end{align} $$
which is nothing but the condition that we have exhibited in Lemma 5.1 for the rule R
$\to $
to be compatible with double negation over intuitionistic provability
$\rhd _i$
.
5.2.3 The minimal case
Take propositional minimal logic
$\rhd _m$
as
$\rhd $
. As observed above, stability (8) equals double negation elimination (16); whence the strong extension
$\rhd _m^{g_\bot }$
of minimal logic
$\rhd _m$
is classical logic
$\rhd _c$
.
Lemma 5.5. Over any given extension
$\rhd _*$
of minimal logic, axiom (13), viz.
$$\begin{align*} {}\rhd_*\neg\neg(\bot\to \varphi),\end{align*} $$
is equivalent to (20) with
$\rhd _*$
in place of
$\rhd _i$
: that is,
$$ \begin{align} \varphi\to\neg\neg\psi\rhd_*\neg\neg(\varphi\to\psi)\,. \end{align} $$
Proof. We can obtain (13) from the instance
$$ \begin{align*} \bot\to\neg\neg\varphi\rhd_*\neg\neg(\bot\to\varphi), \end{align*} $$
of (21) by an application of Trans with the derivable
${}\rhd _*\bot \to \neg \neg \varphi $
.
As (20) is well-known [Reference van Dalen113], (21) follows from instances of ex falso sequitur quodlibet in minimal logic. By using L
$j$
, (21) equally follows from the same instances of (13). In the Appendix 7 we detail a direct proof.
The following statement [Reference Cignoli and Torrens15, Reference Odintsov82]Footnote 9 is a generalisation of Proposition 5.4 (Figure 3):
Figure 3 Diagram of the entailment relations involved in the situation of Propositions 5.4 and 5.6. A solid arrow denotes a strong
$\neg \neg $
-extension, a dashed arrow denotes a weak
$\neg \neg $
-extension, a dotted arrow denotes a generic extension, and a double line denotes a conservative extension.
Proposition 5.6 (General Glivenko theorem [Reference Cignoli and Torrens15, Reference Odintsov82]).
Let
$\rhd _{*}$
be an inductive extension of
$\rhd _m$
the additional rules of which hold for
${\rhd _c}$
. The following are equivalent:
-
(a)
$\Gamma \rhd _c\varphi \iff \Gamma \rhd _*\neg \neg \varphi $
for all
$\Gamma ,\varphi $
; -
(b)
${\rhd _g}\subseteq {\rhd _*}$
.
Proof. Since
$\varphi \to \neg \neg \psi \rhd _i\neg \neg (\varphi \to \psi )$
holds by 5.5, in view of Lemma 5.1(i) the rule R
$\to $
is compatible with
$\neg \neg $
, and we get the claim as an instance of Corollary 3.7.
Since in minimal logic
$\bot $
has no special role, we would get a completely analogous statement if we considered the more general continuation nucleus
$g_\alpha \colon \varphi \mapsto (\varphi \to \alpha )\to \alpha $
in place of
$\neg \neg $
and used the axiom
$$\begin{align*} {}\rhd((\alpha\to\varphi)\to\alpha)\to\alpha\end{align*} $$
in place of (13) to define
$\rhd _g$
.
5.2.4 The predicate case
Let us go back to considering intuitionistic logic
$\rhd _i$
as
$\rhd $
.
Proposition 5.7 (Gödel’s theorem [Reference Gödel46]).
Let
$\rhd _{*}$
be an inductive extension of
$\rhd _i$
the additional rules of which hold for
${\rhd _c}$
. The following are equivalent in predicate logic:
-
(a)
$\Gamma \rhd _c\varphi \iff \Gamma \rhd _*\neg \neg \varphi $
for all
$\Gamma ,\varphi $
; -
(b)
$\forall x\neg \neg \varphi \rhd _*\neg \neg \forall x\varphi $
for all
$\varphi $
.
Proof. Similar to Proposition 5.4; but apply Theorem 3.5 instead of Corollary 3.7. Lemma 5.1(ii) can be applied since the Glivenko nucleus is compatible with substitution.
Condition (b) in Proposition 5.7 is called Double Negation Shift (
$\operatorname {\mathrm {DNS}}$
) and is known to define a proper intermediate logic
$\rhd _{\operatorname {\mathrm {DNS}}}$
, that is,
$\rhd _i\subsetneq \rhd _{\operatorname {\mathrm {DNS}}}\subsetneq \rhd _c$
[Reference Espíndola31].Footnote
10
Proposition 5.8. Let
$k,g,J$
be respectively the Kolmogorov, Gentzen and Kuroda
$\neg \neg $
-functions. In predicate logic:
-
(i)
$\Gamma \rhd _c\varphi \iff k\Gamma \rhd _ik\varphi $
.In other words,
$k$
is a
$\neg \neg $
-translation, known as the Kolmogorov negative translation [Reference Ferreira, Oliva, Berger, Diener, Schuster and Seisenberger37, Reference Kolmogorov64]. -
(ii)
$\Gamma \rhd _c\varphi \iff g\Gamma \rhd _ig\varphi $
.In other words, g is a
$\neg \neg $
-translation, known as the Gentzen negative translation
Footnote
11
[Reference Ferreira, Oliva, Berger, Diener, Schuster and Seisenberger37, Reference Gentzen41, Reference Gentzen43]. -
(iii)
$\Gamma \rhd _c\varphi \iff {\neg \neg }J\Gamma \rhd _i{\neg \neg }J\varphi \iff J\Gamma \rhd _i\neg \neg J\varphi $
.In other words,
${\neg \neg } J$
is a
$\neg \neg $
-translation, known as the minimal Kuroda negative translation
Footnote
12
[Reference Ferreira, Oliva, Berger, Diener, Schuster and Seisenberger37, Reference Kuroda66, Reference Murthy73, Reference van den Berg114].
Proof. Since
$\bot \approx _i\neg \neg \bot ,$
it is easy to see that
$k,g,J$
all satisfy (9). Hence by Remark 5.2, k and g satisfy the conditions of Theorem 3.13, which shows (i) and (ii). Similarly, by Remark 5.2, J satisfies the conditions of Corollary 3.14, which shows (iii).
Theorem 3.13 gives results similar to those in Proposition 5.8 also for other negative translations, such as the Gödel negative translation [Reference Gödel, Berka and Kreiser47], the original Kuroda negative translation [Reference Kuroda66], the Krivine negative translation—which was introduced by Streicher and Reus [Reference Streicher and Reus108] based on Krivine’s work [Reference Krivine65]—and the negative translation by Ferreira and Oliva [Reference Ferreira, Oliva, Berger, Diener, Schuster and Seisenberger37]. We only point out that, unlike the ones presented here, the latter two cannot be generalised—at least not in a direct way—for an arbitrary nucleus
$j$
, and hence a counterpart of Remark 5.2 cannot be given.
5.2.5 The infinitary case
The following statement [Reference Tesi110]Footnote 13 is the counterpart of Proposition 5.7 for infinitary logic:
Proposition 5.9. Let
$\rhd _{*}$
be an inductive extension of
$\rhd _i$
the additional rules of which hold for
${\rhd _c}$
. The following are equivalent in infinitary logic:
-
(a)
$\Gamma \rhd _c\varphi \iff \Gamma \rhd _*\neg \neg \varphi $
for all
$\Gamma ,\varphi $
; -
(b)
$\bigwedge _{i\in \mathbb {N}}\neg \neg \varphi _i\rhd _*\neg \neg \bigwedge _{i\in \mathbb {N}}\varphi _i$
for all
$\{\varphi _i\colon i\in \mathbb {N}\}$
.
Proof. Similar to Proposition 5.7.
As above, condition (b) in Proposition 5.9 defines a proper intermediate logic
$\rhd _{\operatorname {\mathrm {DNS}}_{inf}}$
, that is,
$\rhd _i\subsetneq \rhd _{\operatorname {\mathrm {DNS}}_{inf}}\subsetneq \rhd _c$
.
5.2.6 The Peirce nucleus and the Clavius nucleus
Let again
$\rhd _*$
be an inductive extension of
$\rhd _m$
, and fix a formula
$\alpha $
. The Peirce nucleus [Reference Johnstone60, Reference Johnstone62, Reference Rosenthal93, Reference van den Berg114] is
$$\begin{align*} p_\alpha\colon\varphi\mapsto(\varphi\to\alpha)\to \varphi\,. \end{align*}$$
As for Lemma 5.3 one readily proves with the generating rules of
$\rhd _m$
that
$p_\alpha $
is in fact a nucleus. We are especially interested in the particular case of the Clavius nucleus:
$$\begin{align*} p_\bot\colon\varphi\mapsto\neg\varphi\to\varphi\,. \end{align*}$$
Over intuitionistic logic, it is easy to see that the Glivenko nucleus is equivalent to the Clavius nucleus, i.e.,
$\neg \neg \varphi \approx _i\neg \varphi \to \varphi $
for every
$\varphi $
, and hence Propositions 5.4 and 5.7–5.9 equally hold for the Clavius nucleus in place of the Glivenko nucleus.
If we consider minimal logic
$\rhd _m$
instead, then the Clavius nucleus is no more equivalent to the Glivenko nucleus. As stability (8) for the Clavius nucleus
$j$
equals (14), the strong extension
$\rhd _m^j$
of minimal logic
$\rhd _m$
is nothing but the Clavius logic
$\rhd _s$
. We thus get the following counterpart of Glivenko’s theorem:
Proposition 5.10. In propositional logic,
$$\begin{align*} \Gamma\rhd_s\varphi\iff\Gamma\rhd_m\neg\varphi\to\varphi.\end{align*}$$
5.3 Open and closed nuclei
Once more let
$\rhd _*$
be an inductive extension of
$\rhd _m$
, and fix a formula
$\alpha $
. The closed nucleus
$c_\alpha $
and the open nucleus
$o_\alpha $
[Reference Rosenthal93, Reference van den Berg114] are defined byFootnote
14
$$ \begin{align*} c_\alpha\colon\varphi\mapsto\varphi\vee\alpha, && o_\alpha\colon\varphi\mapsto\alpha\to\varphi. \end{align*} $$
Figure 4 Diagram of the entailment relations induced by open and closed nuclei. A solid arrow denotes a strong extension, a dashed arrow denotes a weak extension, a dotted arrow denotes a generic extension, and a double line denotes a conservative extension.
Still as for Lemma 5.3, with the generating rules of
$\rhd _m$
one easily sees that
$c_\alpha $
and
$o_\alpha $
are nuclei over
$\rhd _*$
. We notice the following facts about the extensions induced by these nuclei:
-
– Stability of the open nucleus is equivalent to
${}\rhd\alpha $
, which can be read as “
$\alpha $
is derivable”; thus the strong extension
$\rhd _*^{o_\alpha }$
is the smallest entailment relation containing
$\rhd _*$
in which “
$\alpha $
holds”. If
$\alpha =\bot $
, then stability of
$o_\bot $
becomes (18), thus the strong extension
$\rhd _m^{o_\bot }$
is nothing but negative logic
$\rhd _n$
. -
– Similarly, stability of the closed nucleus is equivalent to
$\alpha \rhd \varphi $
for every propositional formula
$\varphi $
, which can be read as “
$\alpha $
is inconsistent”; thus the strong extension
$\rhd _*^{c_\alpha }$
is the smallest entailment relation containing
$\rhd _*$
in which “
$\alpha $
is inconsistent”. If
$\alpha =\bot $
, then stability of
$c_\bot $
becomes (12), thus the strong extension
$\rhd _m^{c_\bot }$
is nothing but intuitionistic logic
$\rhd _i$
. -
– We also note that in
$(\rhd ^{o_\alpha })^{c_\alpha }$
and
$(\rhd ^{c_\alpha })^{o_\alpha }$
we have both
$\rhd \alpha $
and
$\alpha \rhd \varphi $
, which by Trans lead to
$\rhd \varphi $
for every
$\varphi $
: this means that they both equal trivial logic
$\rhd _t$
.
We can sum up the situation via the diagram in Figures 4 and 5. We now ask ourselves whether some of the strong extensions are conservative over the corresponding weak extension.
Proposition 5.11.
-
(i) Let
$\rhd _{*}$
be
$\rhd _m$
plus additional axioms. Then: for all
$$ \begin{align*} \Gamma\rhd_*^{o_\alpha}\varphi\iff\Gamma\rhd_*\alpha\to\varphi \iff\Gamma,\alpha\rhd_*\varphi, \end{align*} $$
$\Gamma ,\varphi $
. In other words,
$\varphi $
is derivable from
$\Gamma $
when assuming that
$\alpha $
is derivable, if and only if
$\alpha \to \varphi $
is derivable from
$\Gamma $
, if and only if
$\varphi $
is derivable from
$\Gamma $
and
$\alpha $
.
-
(ii) Let
$\rhd _{*}$
be
$\rhd _m$
plus additional axioms. Then for all
$$ \begin{align*} \Gamma\rhd_*^{c_\alpha}\varphi\iff\Gamma\rhd_*\varphi\vee\alpha \end{align*} $$
$\Gamma ,\varphi $
if and only if (22)
$$ \begin{align} {}\rhd_*\alpha\vee (\alpha\to\varphi). \end{align} $$
Proof.
-
(i) In view of
$\varphi \to (\alpha \to \psi )\rhd _m\alpha \to (\varphi \to \psi )$
, the first equivalence holds by means of Theorem 3.5 and Lemma 5.1. The second equivalence is the deduction theorem for
$\rhd _*$
. -
(ii) It can easily be shown that (22) is equivalent to
$\varphi \to (\psi \vee \alpha )\rhd (\varphi \to \psi )\vee \alpha $
; hence the claim follows from Theorem 3.5 and Lemma 5.1.
Corollary 5.12.
-
(i) Let
${\rhd _*}\in \{{\rhd _m},{\rhd _f},{\rhd _i}\}$
. Then
${\rhd _*^{o_\bot }}={\rhd _{*o_\bot }}$
. -
(ii) Let
${\rhd _*}\in \{{\rhd _f},{\rhd _n}\}$
. Then
${\rhd _{*c_\bot }}={\rhd _*^{c_\bot }}$
. -
(iii)
${\rhd _{mc_\bot }}\subsetneq {\rhd _c}$
.
In conclusion, all strong extensions in Figure 4 are conservative over the corresponding weak extension except for
$\rhd _c$
over
${\rhd _{mc_\bot }}$
.
Figure 5 Simplified version of Figure 4, where the weak extensions that coincide with the corresponding strong extension are omitted.
5.3.1 A few remarks about the predicate case
In predicate logic, we get an analogous situation by considering the logic
$\rhd _F$
, defined as the predicate version of the Frobenius logic
$\rhd _f$
plus the dual Frobenius rule [Reference Johnstone62]
$$ \begin{align*} \forall x(\varphi\vee\bot)&\rhd(\forall x\varphi)\vee\bot. \end{align*} $$
Functions based on the open and closed nuclei but over predicate intuitionistic logic
$\rhd _i$
are known in literature. For instance, having fixed a formula A, Friedman employed the prime
$c_A$
-functionFootnote
15
$t_\alpha ^C$
—thus known as Friedman’s A-translation—to prove Markov’s rule [Reference Friedman, Müller and Scott38]; and Ishihara and Nemoto used the prime
$o_A$
-function
$t_A^O$
to prove the independence-of-premiss rule [Reference Ishihara and Nemoto56]. Note that:
$$ \begin{align*} t_A^Oo_A\varphi&= t_A^OA\to t_A^O\varphi, & t_A^Cc_A\varphi&= t_A^C\varphi\vee t_A^CA. \end{align*} $$
This means that
$t_A^O$
satisfies (8), and hence is an
$o_A$
-translation, if and only if “
$t_A^OA$
holds” in the sense that
${}\rhd t_A^OA$
; this is the case, e.g., when A is atomic. Similarly,
$t_A^C$
satisfies (8), and thus is a
$c_A$
-translation, precisely when “
$t_A^CA$
is inconsistent” in the sense that
$t_A^CA\rhd \varphi $
for every
$\varphi $
; this is the case, e.g., when
$A=\bot $
. In the latter case, however, the strong
$c_A$
-extension is trivial.
5.4 Propositional lax logic
In propositional lax logic [Reference Fairtlough and Mendler32] the modality
$\bigcirc $
is characterised by rules corresponding [Reference Fairtlough and Mendler32, p. 2, Section 1] to the ones of a nucleus. In our setting, we define
$\rhd _L$
by adding a unary relation symbol
$\bigcirc $
to the language of
$\rhd _i$
, and the axiom
$$\begin{align*} \varphi\to\bigcirc\psi\approx\bigcirc\varphi\to\bigcirc\psi \end{align*}$$
to the inductive definition of
$\rhd _i$
. It is evident that
$j=\bigcirc $
is a nucleus over
$\rhd _L$
. This trivially extends to every inductive extension of
$\rhd _L$
since L
$\bigcirc $
is a generating rule.
The strong
$\bigcirc $
-extension
$\rhd _L^\bigcirc $
of
$\rhd _L$
is
$\rhd _i$
plus
$$\begin{align*} \varphi\approx\bigcirc\varphi, \end{align*}$$
i.e., plus an identity operator
$\bigcirc $
on formulae. We also define
$\rhd _{L*}$
as
$\rhd _L$
plus
$$\begin{align*} \varphi\to\bigcirc\psi\rhd\bigcirc(\varphi\to\psi),\end{align*} $$
i.e., the smallest extension of
$\rhd _L$
in which the nucleus
$\bigcirc $
is compatible with R
$\to $
(Theorem 3.5).
Given a formula
$\varphi $
in the language of
$\rhd _L$
, we denote by
$\varphi '$
the formula obtained from
$\varphi $
by removing all occurrences of
$\bigcirc $
. Formally, the definition of
$\varphi '$
is given inductively:
$$ \begin{align*} P'&= P, & \top'&=\top, & \bot'&=\bot, \\ (\varphi\wedge\psi)'&=\varphi'\wedge\psi', & (\varphi\vee\psi)'&=\varphi'\vee\psi', & (\varphi\to\psi)'&=\varphi'\to\psi', \\ (\forall x\varphi)'&=\forall x\varphi', & (\exists x\varphi)'&=\exists x\varphi', & (\bigcirc\varphi)'&=\varphi'. \end{align*} $$
We obtain a somewhat more general version of strong conservativity [Reference Fairtlough and Mendler32, theorem 2.4]:
Proposition 5.13. The following are equivalent:
-
(a)
$\Gamma \rhd _{L*}\bigcirc \varphi $
, -
(b)
$\Gamma \rhd _L^\bigcirc \varphi $
, -
(c)
$\Gamma '\rhd _L^\bigcirc \varphi '$
, -
(d)
$\Gamma '\rhd _i\varphi '$
.
In particular, if
$\Gamma \rhd _L\varphi $
, then
$\Gamma '\rhd _i\varphi '$
.
Proof. Items (a) and (b) are equivalent by Theorem 3.5. The fact that (d) implies (c) holds since
$\rhd _L^\bigcirc $
extends
$\rhd _i$
. The directions from (c) to (b) and from (b) to (d) are proved straightforwardly by structural induction.
6 Future work
Orevkov [Reference Orevkov and Orevkov84] has established some well-known conservativity results of classical logic over intuitionistic and minimal first-order logics with equality. In particular, he isolates seven classes of single-succedent sequents—the so-called Glivenko sequent classes—defined in terms of the absence of positive or negative occurrences of particular logical symbols (in a first-order language with equality) where classical derivability implies intuitionistic derivability. The same article also shows that these classes are optimal: any class of sequents for which classical derivability implies intuitionistic derivability is contained in one of these seven classes. In recent years simpler proofs of conservativity results for some Glivenko sequent classes have been given [Reference Ishihara55, Reference Nadathur74, Reference Schwichtenberg and Senjak100]. An extremely simple and purely logical proof of the first Glivenko class for coherent theories has been obtained by Negri [Reference Negri77] by means of
$\mathbf {G3}$
-style sequent calculi; this has been extended to geometric theories in [Reference Negri, Arieli and Zamansky79] and then to cover all other first-order Glivenko sequent classes in [Reference Fellin, Negri and Orlandelli34, Reference Negri78]. We want to investigate whether a generalisation of these results is possible in our setting.
7 Appendix Proof details
We give here a direct proof of Lemma 5.5.
Lemma 7.1. Over any given extension
$\rhd _*$
of minimal logic, the following are equivalent:
-
(a)
${}\rhd _*\neg \neg (\bot \to \varphi ),$
-
(b)
$\varphi \to \neg \neg \psi \rhd _*\neg \neg (\varphi \to \psi )\,.$
Proof. As for (b)
$\Longrightarrow $
(a):
As for (a)
$\Longrightarrow $
(b):
where
$\neg (\varphi \to \psi )\rhd _*\neg \neg \varphi $
is derived as follows:
Acknowledgements
The authors wish to thank Benno van den Berg, Ingo Blechschmidt, Hajime Ishihara, Sara Negri, Paulo Oliva, Mario Piazza, Matteo Tesi and Tarmo Uustalu for their interest and suggestions. Last but not least, the authors are grateful to Daniel Misselbeck-Wessel whose original idea set the basis for this work.
Funding
The present study was carried out within the projects “A New Dawn of Intuitionism: Mathematical and Philosophical Advances” (ID 60842) funded by the John Templeton Foundation, and “Reducing complexity in algebra, logic, combinatorics - REDCOM” belonging to the programme “Ricerca Scientifica di Eccellenza 2018” of the Fondazione Cariverona. Both authors are members of the “Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni” (GNSAGA) of the Istituto Nazionale di Alta Matematica (INdAM).
