Provability in BI's Sequent Calculus is Decidable
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929312326746112 |
|---|---|
| author | Gheorghiu, Alexander Docherty, Simon Pym, David |
| author_facet | Gheorghiu, Alexander Docherty, Simon Pym, David |
| contents | Warning: This paper contains a mistake, rendering the proof of the main theorem invalid. The logic of Bunched Implications (BI) combines both additive and multiplicative connectives, which include two primitive intuitionistic implications. As a consequence, contexts in the sequent presentation are not lists, nor multisets, but rather tree-like structures called bunches. This additional complexity notwithstanding, the logic has a well-behaved metatheory admitting all the familiar forms of semantics and proof systems. However, the presentation of an effective proof-search procedure has been elusive since the logic's debut. We show that one can reduce the proof-search space for any given sequent to a primitive recursive set, the argument generalizing Gentzen's decidability argument for classical propositional logic and combining key features of Dyckhoff's contraction-elimination argument for intuitionistic logic. An effective proof-search procedure, and hence decidability of provability, follows as a corollary. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2103_02343 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Provability in BI's Sequent Calculus is Decidable Gheorghiu, Alexander Docherty, Simon Pym, David Logic in Computer Science Symbolic Computation Logic 03B25 (Primary) 03D99, 68W68, 68Q68 (Secondary) F.0; I.1; F.3 Warning: This paper contains a mistake, rendering the proof of the main theorem invalid. The logic of Bunched Implications (BI) combines both additive and multiplicative connectives, which include two primitive intuitionistic implications. As a consequence, contexts in the sequent presentation are not lists, nor multisets, but rather tree-like structures called bunches. This additional complexity notwithstanding, the logic has a well-behaved metatheory admitting all the familiar forms of semantics and proof systems. However, the presentation of an effective proof-search procedure has been elusive since the logic's debut. We show that one can reduce the proof-search space for any given sequent to a primitive recursive set, the argument generalizing Gentzen's decidability argument for classical propositional logic and combining key features of Dyckhoff's contraction-elimination argument for intuitionistic logic. An effective proof-search procedure, and hence decidability of provability, follows as a corollary. |
| title | Provability in BI's Sequent Calculus is Decidable |
| topic | Logic in Computer Science Symbolic Computation Logic 03B25 (Primary) 03D99, 68W68, 68Q68 (Secondary) F.0; I.1; F.3 |
| url | https://arxiv.org/abs/2103.02343 |