Abstract
This paper is about non-labelled proof-systems for hybrid logic, that is, proof-systems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that non-labelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations.
| Original language | English |
|---|---|
| Journal | Bulletin of the Section of Logic |
| Volume | 51 |
| Issue number | 2 |
| Pages (from-to) | 143-162 |
| Number of pages | 20 |
| ISSN | 0138-0680 |
| DOIs | |
| Publication status | Published - Jun 2022 |
Keywords
- Hybrid logic
- Natural deduction systems
- Sequent systems
- Normalization
- Cut-elimination
- Analycity