Infinitary negative translations and Glivenko logic

Abstract We study infinitary intuitionistic logic by employing both syntactic and semantic methods. First, we introduce a natural deduction system for infinitary predicate logic and study some of its basic properties. We then extend neighbourhood semantics to this setting, providing a soundness and completeness theorem for this system. Building on these tools, we derive three new conservation results connecting classical and constructive reasoning. We prove an infinitary version of Barr’s theorem using neighbourhood semantics; we define an infinitary Gentzen-style negative translation and show it yields a proper embedding of classical logic into minimal logic; and we establish an infinitary Glivenko theorem, identifying the Glivenko logic as the least extension of minimal logic validating Glivenko’s theorem. Finally, we show that the Glivenko logic is distinct from the other systems considered, thereby clarifying its place within the landscape of constructive infinitary logics.