Twist Sequent Calculi for S4 and its Neighbors
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909446130630656 |
|---|---|
| author | Kamide, Norihiro |
| author_facet | Kamide, Norihiro |
| contents | Two Gentzen-style twist sequent calculi for the normal modal logic S4 are introduced and investigated. The proposed calculi, which do not employ the standard logical inference rules for the negation connective, are characterized by several twist logical inference rules for negated logical connectives. Using these calculi, short proofs can be generated for provable negated modal formulas that contain numerous negation connectives. The cut-elimination theorems for the calculi are proved, and the subformula properties for the calculi are also obtained. Additionally, Gentzen-style twist (hyper)sequent calculi for other normal modal logics including S5 are considered.
|
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_00483 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Twist Sequent Calculi for S4 and its Neighbors Kamide, Norihiro Logic in Computer Science F.4.1 Two Gentzen-style twist sequent calculi for the normal modal logic S4 are introduced and investigated. The proposed calculi, which do not employ the standard logical inference rules for the negation connective, are characterized by several twist logical inference rules for negated logical connectives. Using these calculi, short proofs can be generated for provable negated modal formulas that contain numerous negation connectives. The cut-elimination theorems for the calculi are proved, and the subformula properties for the calculi are also obtained. Additionally, Gentzen-style twist (hyper)sequent calculi for other normal modal logics including S5 are considered. |
| title | Twist Sequent Calculi for S4 and its Neighbors |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2501.00483 |