The proof theory and semantics of second-order (intuitionistic) tense logic
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866918325136654336 |
|---|---|
| author | Becker, Justus Das, Anupam Marin, Sonia Padhiar, Paaras |
| author_facet | Becker, Justus Das, Anupam Marin, Sonia Padhiar, Paaras |
| contents | We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the negative fragment. Duly we are able to recover the diamond (and its associated theory) using only boxes, as long as we include both forward and backward modalities (`tense' modalities).
We propose axiomatic, proof theoretic and model theoretic definitions of `second-order intuitionistic tense logic', and ultimately prove that they all coincide. In particular we establish completeness of a labelled sequent calculus via a proof search argument, yielding at the same time a cut-admissibility result. Our methodology also applies to the classical version of second-order tense logic, which we develop in tandem with the intuitionistic case. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_06253 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | The proof theory and semantics of second-order (intuitionistic) tense logic Becker, Justus Das, Anupam Marin, Sonia Padhiar, Paaras Logic in Computer Science Logic We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the negative fragment. Duly we are able to recover the diamond (and its associated theory) using only boxes, as long as we include both forward and backward modalities (`tense' modalities). We propose axiomatic, proof theoretic and model theoretic definitions of `second-order intuitionistic tense logic', and ultimately prove that they all coincide. In particular we establish completeness of a labelled sequent calculus via a proof search argument, yielding at the same time a cut-admissibility result. Our methodology also applies to the classical version of second-order tense logic, which we develop in tandem with the intuitionistic case. |
| title | The proof theory and semantics of second-order (intuitionistic) tense logic |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2602.06253 |