Full classical S5 in natural deduction with weak normalization (Q2478553)

The paper investigates natural deduction systems for the classical first-order modal logic S5. Several natural deduction systems for S4 were presented in the literature, but none of them admits normalization in the full language including \(\lor\), \(\exists\), and \(\lozenge\). In the present paper a new natural deduction system is introduced, based on a system investigated by \textit{D. Prawitz} [Natural deduction. A proof-theoretic study. Stockholm-Göteborg-Uppsala: Almqvist and Wiksell (1965; Zbl 0173.00205)], but using a new version of the \(\lozenge\text{E}\) rule involving the notion of modally independent formulas. The authors present reduction rules for the system, including a detailed proof of correctness. The main result is a proof of weak normalization for the system, and the subformula property for normal deductions.