Bounded Modal Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911437236994048 |
|---|---|
| author | Murase, Yuito Maniwa, Akinori |
| author_facet | Murase, Yuito Maniwa, Akinori |
| contents | Under the Curry--Howard isomorphism, the syntactic structure of programs can be modeled using birelational Kripke structures equipped with intuitionistic and modal relations. Intuitionistic relations capture scoping through persistence, reflecting the availability of resources from outer scopes, while modal relations model resource isolation introduced for various purposes.
Traditional modal languages, however, describe only modal transitions and thus provide limited support for expressing fine-grained control over resource availability. Motivated by this limitation, we introduce \emph{Bounded Modal Logic (\textbf{BML})}, an experimental extension of constructive modal logic whose language explicitly accounts for both intuitionistic and modal transitions.
We present a natural-deduction proof system and a Kripke semantics for \textbf{BML}, together with a Curry--Howard interpretation via a corresponding typed lambda-calculus. We establish metatheoretic properties of the calculus, showing that \textbf{BML} forms a well-disciplined logical system. This provides theoretical support for our proposed perspective on fine-grained resource control in programming languages. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_09462 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Bounded Modal Logic Murase, Yuito Maniwa, Akinori Logic in Computer Science D.3.1; F.3.3 Under the Curry--Howard isomorphism, the syntactic structure of programs can be modeled using birelational Kripke structures equipped with intuitionistic and modal relations. Intuitionistic relations capture scoping through persistence, reflecting the availability of resources from outer scopes, while modal relations model resource isolation introduced for various purposes. Traditional modal languages, however, describe only modal transitions and thus provide limited support for expressing fine-grained control over resource availability. Motivated by this limitation, we introduce \emph{Bounded Modal Logic (\textbf{BML})}, an experimental extension of constructive modal logic whose language explicitly accounts for both intuitionistic and modal transitions. We present a natural-deduction proof system and a Kripke semantics for \textbf{BML}, together with a Curry--Howard interpretation via a corresponding typed lambda-calculus. We establish metatheoretic properties of the calculus, showing that \textbf{BML} forms a well-disciplined logical system. This provides theoretical support for our proposed perspective on fine-grained resource control in programming languages. |
| title | Bounded Modal Logic |
| topic | Logic in Computer Science D.3.1; F.3.3 |
| url | https://arxiv.org/abs/2602.09462 |