Normalisation for Some Infectious Logics and Their Relatives
Yaroslav Petrukhin (Department of Logic, University of Lodz)
TL;DR
This paper develops natural deduction systems for various infectious and related logics, proves their normalization, and establishes the negation subformula property, enhancing understanding of their proof-theoretic features.
Contribution
It introduces new and reformulated natural deduction systems for infectious logics, enabling normalization proofs and analysis of their logical properties.
Findings
Proof of normalization for the considered logics
Establishment of the negation subformula property
Introduction of new logics and their deduction systems
Abstract
We consider certain infectious logics (Sfde, dSfde, K3w, and PWK) and several their non-infectious modifications, including two new logics, reformulate previously constructed natural deduction systems for them (or present such systems from scratch for the case of new logics) in way such that the proof of normalisation theorem becomes possible for these logics. We present such a proof and establish the negation subformula property for the logics in question.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.