Full classical S5 in natural deduction with weak normalization

DOI10.1016/J.APAL.2007.11.007MaRDI QIDQ2478553zbMATH OpenOpenAlexFDO

Authors Ana Teresa Martins, Lilia Ramalho Martins

Publication date 28 March 2008

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2007.11.007

zbMATH Keywords

modal logicnatural deductionnormalizationS5

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Review text

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.

Recommendations

• A new S4 classical modal logic in natural deduction
• Normal derivability in classical natural deduction
• Classical natural deduction for S4 modal logic
• Normalization theorems for full first order classical natural deduction
• Normal derivability in modal logic

Cites work

• 2-Sequent Calculus: Intuitionism and Natural Deduction
• A cut-free Gentzen formulation of the modal logic S5
• A cut-free Gentzen-type system for the modal logic S5
• A new S4 classical modal logic in natural deduction
• scientific article; zbMATH DE number 3131074 (Why is no real title available?)
• scientific article; zbMATH DE number 3145226 (Why is no real title available?)
• scientific article; zbMATH DE number 4108725 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3318631 (Why is no real title available?)
• Normalization and excluded middle. I
• Normalization theorems for full first order classical natural deduction
• Proof analysis in modal logic
• Sequent Calculi for Normal Modal Propositional Logics

Cited in

(8)

• Classical natural deduction for S4 modal logic
• A normalization-procedure for the first order classical natural deduction with full logical symbols
• Formal justification of underspecification for S5
• Normal derivability in classical natural deduction
• A new S4 classical modal logic in natural deduction
• Modal functional (``Dialectica) interpretation
• scientific article; zbMATH DE number 2196584 (Why is no real title available?)
• Natural deduction calculi for classical and intuitionistic S5

This page was built for publication: Full classical S5 in natural deduction with weak normalization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2478553)