What type of study is this?

September 10, 2025Open Access

Proof Theory for Intuitionistic Stable Theories

Key Points

The main finding reveals that cut-elimination can be effectively extended to a broader class of intuitionistic stable theories.
Key evidence shows that all structural rules remain admissible under the modified calculus, including cut.
The approach involves modifying the underlying calculus for first-order intuitionistic logic while accommodating specific rules.
This work highlights the significance of understanding these modifications for further developments in proof theory.

Abstract

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.

Read Full Paperexternally

Mark Helpful

Bookmark

Relay

View Full Paper

Cite This Study

Paolo Maffezioli (Fri,) studied this question.

synapsesocial.com/papers/68c1824b9b7b07f3a060e8ab https://doi.org/https://doi.org/10.12775/llp.2025.012