Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2510.25394 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914121959604224 |
|---|---|
| author | Su, Youan |
| author_facet | Su, Youan |
| contents | Uniform interpolation property (UIP) is a strengthening of Craig interpolation property. It was first established by Pitts(1992) based on a pure proof-theoretic method. UIP in multi-modal $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$ logic have been established by semantic approaches, however, a proof-theoretic approach is still lacking. Bílková (2007) develops the method in Pitts (1992) to show UIP in classical modal logic $\mathbf{K}$ and $\mathbf{KT}$. This paper further extends Bílková (2007)'s systems to establish the UIP in multi-agent modal logic $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$. A purely syntactic algorithm is presented to determine a uniform interpolant formula. It is also shown that quantification over propositional variables can be modeled by UIP in these systems. Furthermore, a direct argument to establish UIP without using second-order quantifiers is also presented. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_25394 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A proof-theoretic approach to uniform interpolation property of multi-agent modal logic Su, Youan Logic in Computer Science Uniform interpolation property (UIP) is a strengthening of Craig interpolation property. It was first established by Pitts(1992) based on a pure proof-theoretic method. UIP in multi-modal $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$ logic have been established by semantic approaches, however, a proof-theoretic approach is still lacking. Bílková (2007) develops the method in Pitts (1992) to show UIP in classical modal logic $\mathbf{K}$ and $\mathbf{KT}$. This paper further extends Bílková (2007)'s systems to establish the UIP in multi-agent modal logic $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$. A purely syntactic algorithm is presented to determine a uniform interpolant formula. It is also shown that quantification over propositional variables can be modeled by UIP in these systems. Furthermore, a direct argument to establish UIP without using second-order quantifiers is also presented. |
| title | A proof-theoretic approach to uniform interpolation property of multi-agent modal logic |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2510.25394 |