arxiv: 2605.02450 · v1 · submitted 2026-05-04 · 💻 cs.LO · math.LO

Recognition: 2 theorem links

· Lean Theorem

Glivenko's theorems from an ecumenical perspective

Luiz Carlos Pereira , Victor Barroso-Nascimento , Elaine Pimentel

Authors on Pith no claims yet

Pith reviewed 2026-05-08 18:24 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords Glivenko theoremsecumenical logicnatural deductionclassical logicintuitionistic logictranslations

0 comments

The pith

Glivenko's theorems relating classical and intuitionistic logic extend to ecumenical natural deduction systems.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper revisits Glivenko's theorems that link classical and intuitionistic logic through specific translations. It checks whether these links survive when the two kinds of reasoning are placed inside single combined systems. Three ecumenical natural deduction systems are examined to see if the translations stay valid and the overall systems remain consistent. A reader would care because such systems let people mix classical and intuitionistic steps in one proof while keeping the known relationships between the logics intact.

Core claim

Glivenko's theorems hold inside the ecumenical natural deduction systems, so the translations that turn classical theorems into intuitionistic ones keep their properties even when both styles of reasoning operate together.

What carries the argument

Ecumenical natural deduction systems that combine classical and intuitionistic rules while supporting the original Glivenko translations.

If this is right

The Glivenko translations continue to map classical theorems correctly into intuitionistic ones inside each system.
Merging the two logics does not create inconsistencies or erase their differences.
The systems give faithful combined versions of the original classical-intuitionistic relation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Ecumenical systems could make it easier to write proofs that switch between classical and intuitionistic steps in formal verification tools.
The same preservation check could be applied to other known translations between logics.
Proof assistants might use these systems to handle mixed reasoning without separate classical and intuitionistic modes.

Load-bearing premise

The three ecumenical systems correctly capture the classical-intuitionistic relationship without adding rules that change Glivenko's translations.

What would settle it

A classically provable formula whose image under a Glivenko translation fails to be provable in one of the ecumenical systems would show the theorems do not hold.

Figures

Figures reproduced from arXiv: 2605.02450 by Elaine Pimentel, Luiz Carlos Pereira, Victor Barroso-Nascimento.

**Figure 1.** Figure 1: Ecumenical natural deduction system NE. In rules ∀-int and ∃i-elim, the parameter a is fresh. In ∃i-int and ∀-elim, t is a term view at source ↗

**Figure 2.** Figure 2: Rules added to NE in order to obtain the system NEK. Since they are no longer neutral, intuitionistic conjunctions in NEK are also represented by ∧i instead of ∧. B ∧c C B ∧c C [B] 1 [C] 2 B ∧i C [¬(B ∧i C)]3 ⊥ 1 ¬B ⊥ 2 ¬C ⊥ 3 ¬¬(B ∧i C) Lemma 2. B ∧i C ⊢NEK B ∧c C B ∧i C B [¬B] 1 ⊥ B ∧i C C [¬C] 2 ⊥ 1, 2 B ∧c C From this lemma we can directly conclude the following: Corollary 1. ¬(B ∧c C) ⊢NEK ¬(B ∧i C) I… view at source ↗

read the original abstract

In this paper, we revisit Glivenko's theorems, foundational results relating classical and intuitionistic logic, from an ecumenical perspective. We begin by discussing the historical context and significance of Glivenko's original contributions, and then examine their extensions and reinterpretations within ecumenical logical frameworks. Our analysis focuses on three ecumenical systems: Prawitz's natural deduction system NE; the system NEK, closely related to one introduced by Krauss in an unpublished manuscript; and the ECI system proposed by Barroso-Nascimento.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper re-examines Glivenko's theorems in three ecumenical systems but stays descriptive without delivering explicit checks on whether the translations hold.

read the letter

The main takeaway is that this work takes Glivenko's classic results linking classical and intuitionistic logic and looks at them inside ecumenical frameworks that mix the two. It does not produce new theorems or frameworks; it revisits and reinterprets existing ones across three named systems: Prawitz's NE, the NEK variant, and the ECI system. That focus is narrow but coherent for the subfield. The historical setup and the choice of these particular systems are handled clearly enough to organize what was already scattered in the literature. The authors draw on prior named work without obvious circularity, which keeps the discussion grounded. The soft spot is the lack of concrete verification. The central claim requires that the Glivenko double-negation translations still map classical theorems to intuitionistic ones inside these combined systems without adding inconsistencies or dropping key properties. The abstract and description give no derivations or explicit checks, so it is not clear whether the ecumenical rules preserve the original relation or introduce new behavior. If the full paper only describes the systems and states the extensions without testing them, the soundness of the reinterpretation rests on unshown steps. This paper is for proof theorists already working on ecumenical or combined logics who want a single place to see how Glivenko fits. It will not move broader logic or computer science. I would bring it to a reading group only if the group focuses on that niche; otherwise no. I would not cite it in my own work. It deserves peer review because the topic is legitimate and the systems are well-chosen, even if the current version needs the missing verification work to stand on its own.

Referee Report

1 major / 1 minor

Summary. The manuscript revisits Glivenko's theorems relating classical and intuitionistic logic from an ecumenical perspective. It discusses the historical context and significance of Glivenko's original contributions before examining extensions and reinterpretations within ecumenical logical frameworks, with analysis focused on three systems: Prawitz's natural deduction system NE, the NEK system closely related to Krauss's unpublished manuscript, and the ECI system proposed by Barroso-Nascimento.

Significance. If the claimed extensions hold, the work would synthesize historical Glivenko results with contemporary ecumenical systems that combine classical and intuitionistic principles, potentially clarifying how double-negation translations behave in hybrid settings. The paper credits named prior systems and builds on historical results, but its significance is limited by the primarily descriptive focus without new derivations, machine-checked proofs, or falsifiable predictions.

major comments (1)

[Our analysis focuses on three ecumenical systems] The central claim that Glivenko's theorems extend to the three ecumenical systems (NE, NEK, ECI) is load-bearing but unsubstantiated in the provided description. The manuscript focuses on system introductions and historical reinterpretations rather than re-deriving or explicitly verifying that the double-negation translations map classical theorems to intuitionistic ones without introducing inconsistencies or losing key properties of the classical-intuitionistic relation (as required by the skeptic note on preservation).

minor comments (1)

The abstract would benefit from a concise statement of the specific Glivenko theorems being extended and the precise sense in which the ecumenical systems preserve them.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for identifying areas where the presentation of our central claims can be strengthened. We address the major comment below and will revise the paper accordingly.

read point-by-point responses

Referee: The central claim that Glivenko's theorems extend to the three ecumenical systems (NE, NEK, ECI) is load-bearing but unsubstantiated in the provided description. The manuscript focuses on system introductions and historical reinterpretations rather than re-deriving or explicitly verifying that the double-negation translations map classical theorems to intuitionistic ones without introducing inconsistencies or losing key properties of the classical-intuitionistic relation (as required by the skeptic note on preservation).

Authors: We agree that the explicit verification of the double-negation translations and the preservation of the classical-intuitionistic relation in the ecumenical systems NE, NEK, and ECI merits a more detailed and self-contained treatment. While the manuscript already examines the reinterpretation of Glivenko's theorems within these frameworks and discusses how the systems combine classical and intuitionistic principles, we acknowledge that the current exposition relies in part on the reader's familiarity with the underlying natural deduction rules. In the revised version we will add dedicated subsections containing explicit derivations for representative classical theorems (including the law of excluded middle and double-negation elimination) under the relevant translations, together with direct checks that no inconsistencies are introduced and that the key preservation properties hold. These additions will make the load-bearing claim fully substantiated without altering the paper's primarily logical and historical focus. revision: yes

Circularity Check

0 steps flagged

No circularity detected in the ecumenical analysis of Glivenko's theorems

full rationale

The paper revisits Glivenko's original theorems through historical discussion and then examines their behavior in three pre-existing ecumenical systems (NE from Prawitz, NEK related to Krauss, and ECI from Barroso-Nascimento). No derivation chain reduces a claimed result to a self-defined quantity, a fitted parameter renamed as a prediction, or a load-bearing self-citation whose content is unverified. The work is descriptive and referential, relying on external historical results and named prior systems whose definitions and properties are treated as independent inputs rather than constructed within the paper itself.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based on abstract only; the paper relies on standard properties of natural deduction and prior ecumenical systems without introducing new free parameters or invented entities.

axioms (1)

standard math Standard properties of natural deduction systems hold in the ecumenical setting
Invoked when discussing NE, NEK and ECI systems

pith-pipeline@v0.9.0 · 5379 in / 1052 out tokens · 38930 ms · 2026-05-08T18:24:50.362653+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

Foundation/LogicAsFunctionalEquation (RS 'Law of Logic' is a cost functional equation, not a CPL/IPL translation) washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

The first Glivenko theorem establishes that if a formula A is classically provable in CPL, then its double negation is intuitionistically provable in IPL.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

27 extracted references · 2 canonical work pages

[1]

Ecumenismo l´ ogico.Master Dissertation, PUC-Rio, Rio de Janeiro, Brasil, 2018

Victor Barroso-Nascimento. Ecumenismo l´ ogico.Master Dissertation, PUC-Rio, Rio de Janeiro, Brasil, 2018

2018
[2]

An ecumenical view of proof-theoretic semantics

Victor Barroso-Nascimento, Luiz Carlos Pereira, Elaine Pimentel. An ecumenical view of proof-theoretic semantics. InSynthese, 206, 197, 2025

2025
[3]

A modular construction of type theories

Fr´ ed´ eric Blanqui, Gilles Dowek,´Emilie Grienenberger, Gabriel Hondet, Fran¸ cois Thir´ e. A modular construction of type theories. Log. Methods Comput. Sci. 19(1), 2023

2023
[4]

On various Negative Translations

Gilda Ferreira and Paulo Oliva. On various Negative Translations. In Steffen van Bakel, Stefano Berardi, Ulrich Berger (Eds.):Classical Logic and Computation 2010 (Cl&C’10), EPTCS 47, pp. 21-33, 2010

2010
[5]

On the relation between various Negative Trans- lations

Gilda Ferreira and Paulo Oliva. On the relation between various Negative Trans- lations. In Ulrich Berger, Hannes Diener, Peter Schuster and Monika Seisenberger (eds.),Logic, Construction, Computation. De Gruyter. pp. 227-258, 2012

2012
[6]

Die Widerspruchsfreiheit der reinen Zahlentheorie

Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathema- tische Annalen, 112:493–565, 1936

1936
[7]

Amsterdam: North- Holland Pub

Gerhard Gentzen.The Collected Papers of Gerhard Gentzen. Amsterdam: North- Holland Pub. Co., 1969

1969
[8]

¨Uber das Verh¨ altnis zwischen intuitionistischer und klassischer Arithmetik

Gerhard Gentzen. ¨Uber das Verh¨ altnis zwischen intuitionistischer und klassischer Arithmetik. Arch math Logik 16, 119–132 (1974).https://doi.org/10.1007/ BF02015371

1974
[9]

A New Constructive Logic: Classical Logic In Math

Jean-Yves Girard. A New Constructive Logic: Classical Logic In Math. Struct. Comput. Sci., vol 1(3), pp. 255-296, 1991

1991
[10]

Sur quelques points de la logique de M

Valery Glivenko. Sur quelques points de la logique de M. Brouwer.Acad. Royale Belg. Bull. Cl. Sci., 15:183-188, 1929

1929
[11]

Zur intuitionistischen Arihmetik und Zahlentheorie.Ergebnisse eines mathematischen Kolloquiums, Heft 4, pp.34-38, 1933

Kurt G¨ odel. Zur intuitionistischen Arihmetik und Zahlentheorie.Ergebnisse eines mathematischen Kolloquiums, Heft 4, pp.34-38, 1933

1933
[12]

InStudia Logica: An International Journal for Symbolic Logic, Vol

Giulio Guerrieri and Alberto Naibo Postponement of raa and Glivenko’s Theorem, Revisited. InStudia Logica: An International Journal for Symbolic Logic, Vol. 107, No. 1, Pages109-144, 2019

2019
[13]

Sur le principe de tertium non datur.Mat

Andrei Kolmogorov. Sur le principe de tertium non datur.Mat. Sbornik, 32:646- 667, 1925

1925
[14]

A constructive interpretation of classical mathematicsMathematis- che Schriften Kassel, preprint No

Peter Krauss. A constructive interpretation of classical mathematicsMathematis- che Schriften Kassel, preprint No. 5/92, 1992

1992
[15]

Op´ erateurs de mise en m´ emoire et traduction de G¨ odel

Jean-Louis Krivine. Op´ erateurs de mise en m´ emoire et traduction de G¨ odel. In Archive for Mathematical Logic, 30(4): 241–267, 1990

1990
[16]

Intuitionistische Untersuchungen der formalistischen Logik

Sigetaku Kuroda. Intuitionistische Untersuchungen der formalistischen Logik. In Nagoyan Mathematical Journal, 3:35–47, 1951

1951
[17]

Turner, J

Chuck Liang, Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics, Theor. Comput. Sci. 410 (46) (2009) 4747–4768.doi:10.1016/j. tcs.2009.07.041

work page doi:10.1016/j 2009
[18]

A New Normalization Strategy for the Implicational Frag- ment of Classical Propositional Logic InStudia Logica, Vol

Luiz Carlos Pereira, Edward Hermann Haeusler, Vaston Gon¸ calves da Costa, Wag- ner de Campos Sanz. A New Normalization Strategy for the Implicational Frag- ment of Classical Propositional Logic InStudia Logica, Vol. 96, No. 1, October 2010

2010
[19]

Normalization, Soundness and Completeness for the Propositional Fragment of Prawitz’ Ecumenical System

Luiz Carlos Pereira, Ricardo Oscar Rodriguez. Normalization, Soundness and Completeness for the Propositional Fragment of Prawitz’ Ecumenical System. In Revista Portuguesa de Filosofia, Formal Sciences and Philosophy: Logic and Math- ematics, pages 1153-1168, 2017

2017
[20]

Translations and Prawitz’s Ecumenical System

Luiz Carlos Pereira, Elaine Pimentel, Valeria de Paiva. Translations and Prawitz’s Ecumenical System. InStudia Logica, 113, 523–538, 2025

2025
[21]

A Tour on Ecumenical Systems

Elaine Pimentel, Luiz Carlos Pereira. A Tour on Ecumenical Systems. InPro- ceedings of the 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023), pages 3:1-3:15, Dagstuhl, Germany, 2023

2023
[22]

Almqvist and Wiksell, 1965

Dag Prawitz.Natural Deduction, volume 3 of Stockholm Studies in Philosophy. Almqvist and Wiksell, 1965

1965
[23]

Classical versus intuitionistic logic

Dag Prawitz. Classical versus intuitionistic logic. In Bruno Lopes Edward Her- mann Haeusler, Wagner de Campos Sanz, editors,Why is this a Proof?, Festschrift for Luiz Carlos Pereira, volume 27, pages 15–32. College Publications, 2015

2015
[24]

A survey of some connections between classical, intuitionistic and minimal logic

Dag Prawitz, Per-Erik Malmn¨ as. A survey of some connections between classical, intuitionistic and minimal logic. In H. Arnold Schmidt, K. Sch¨ utte & H. J. Thiele (eds.), Contributions to mathematical logic. Amsterdam,: North-Holland. pp. 215- 229, 1968

1968
[25]

Gentzen’s Hauptsatz for the systems NI and NK

Andr´ es Raggio. Gentzen’s Hauptsatz for the systems NI and NK. InLogique et Analyse, vol. 8, n o 30, Pages 91-100, June 1965

1965
[26]

From translations to non-collapsing logic combi- nations

Jo˜ ao Rasga, Cristina Sernadas. From translations to non-collapsing logic combi- nations. InBulletin of the Section of Logic, 54(3), 407–446,https://doi.org/10. 18778/0138-0680.2025.14, 2025

work page arXiv 2025
[27]

Normalization and excluded middle

Jonathan Seldin. Normalization and excluded middle. I. InStudia Logica, Volume 48, pages 193–217, June 1989

1989