Glivenko sequent classes in the light of structural proof theory (Q283115)

The results obtained by \textit{V. P. Orevkov} in his paper on Glivenko classes [Tr. Mat. Inst. Steklova 98, 131--154 (1968; Zbl 0172.29001)] are revisited. It is well known that Orevkov proved the conservativity of classical over intuitionistic and minimal predicate logic with equality in terms of 7 classes of singular sequents and their subclasses (Theorem 4.1) and 5 classes of sequents with empty succedent and their subclasses (Theorem 5.1). Orevkov has also shown that these classes are the only Glivenko classes. Orevkov's paper [loc. cit.] was published in 1968 and soon translated into English; the aim of Negri's work may be seen as to ``refresh'' its proofs, to put its results in a more modern context, and open the ways to new refinements and generalizations. For example, main results in Orevkov's paper [loc. cit.] were formulated for derivability. As Negri states in her work, ``direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the results are strengthened to height-preserving statements, and it is further shown that the constructive and minimal proofs are identical in structure to the classical proof from which they are obtained.'' The links with such themes as computational content of classical theories were not discussed in Orevkov's paper [loc. cit.] since they were not yet studied in the 1960s. Some of the lemmas in Orevkov's paper [loc. cit.] belonged to structural proof theory: for example, lemmas about ``pruning'', {i.e.}, elimination of irrelevant inferences and whole subtrees of a proof tree (term ``weeding'' used in the English translation of his paper is less precise), and about permutations of rules. The paper by Negri follows in many points Orevkov's ideas but belongs to the domain of structural proof theory to a greater degree. ``In re-establishing Orevkov's result we shall also pay attention to the height of derivations to show that stronger results are achieved when \textbf{G3} calculi are used''. Another significant difference is in the analysis of the structure of derivations in the calculus with equality. In his treatment of equality and replacement scheme, Orevkov [loc. cit.] used the method of axioms in context suggested by \textit{S. C. Kleene} in his [Introduction to metamathematics. 9th repr. Amsterdam: North-Holland (1988; Zbl 0875.03002)] for a Hilbert-style system (before the additional chapter on sequent calculi). Orevkov did not go into detail, but referred to Theorem 41 of Kleene's book. The interaction of such axioms with \textit{cut} may be complex (in relation to the question of admissibility of \textit{cut} and other structural rules), and the version of sequent calculus used by Negri that is studied in detail in her book with \textit{J. von Plato} [Proof analysis. A contribution to Hilbert's last problem. Cambridge: Cambridge University Press (2011; Zbl 1247.03001)] is more convenient for treatment of these aspects. In particular, even the \textit{axiom cuts} may be eliminated. It creates new possibilities for generalizations. As Negri writes: ``As observed by a referee, all the results in Sect. 3 continue to hold if we consider any Horn theory in place of the theory of equality.'' Overall impression is that the results about Glivenko classes are shown under a new and useful angle, and the paper proposes several bonuses to a structural proof-theorist.