Proof Theory for Intuitionistic Stable Theories
DOI:
https://doi.org/10.12775/LLP.2025.012Keywords
stable logic, intuitionistic logic, proof theoryAbstract
In this paper we show how to extend the standard cut-elimination procedure from first-order intuitionistic stable logic to a class of intuitionistic stable theories. Building on previous works by Negri and von Plato, we aptly modify the underlying calculus for first-order intuitionistic logic so as to preserve the admissibility of all the structural rules, including cut, in the presence of a restricted version of the rule of classical reductio ad absurdum and of a special case of universal rules.
References
Dragalin, A., Mathematical Intutionism: Introduction to Proof Theory, vol. 67 of Translations of Mathematical Monographs, American Mathematical Society, 1988.
Dyckhoff, R., “Dragalin’s proofs of cut-admissibility for the intuitionistic sequent calculi G3i and G3i′ ”, University of St Andrews Report CS/97/8, 1997.
Gherardi, G., P. Maffezioli and E. Orlandelli, “Interpolation in extensions of first-order logic”, Studia Logica, 108(3): 619–648, 2020. DOI: https://doi.org/10.1007/s11225-019-09867-0
Heyting, A., “Zur intuitionistischen axiomatik der projektiven geometrie”, Mathematische Annalen, 98: 491–538, 1928.
Negri, S., “Sequent calculus proof theory of intuitionistic apartness and order relations”, Archive for Mathematical Logic, 38(8): 521–547, 1999. DOI: https://doi.org/10.1007/s001530050137
Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, 2001. DOI: https://doi.org/10.1017/CBO9780511527340
Negri, S., and J. von Plato, “Cut elimination in the presence of axioms”, The Bulletin of Symbolic Logic, 4(4): 418–435, 1998. DOI: https://doi.org/10.2307/420956
Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, 1996. DOI: https://doi.org/10.1017/CBO9781139168717
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2025 Paolo Maffezioli
This work is licensed under a Creative Commons Attribution-NoDerivatives 4.0 International License.
Stats
Number of views and downloads: 10
Number of citations: 0
