Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
Author(s): Torben BraünerSubject(s): Logic
Published by: Wydawnictwo Uniwersytetu Łódzkiego
Keywords: hybrid logic; natural deduction systems; sequent systems; normalization; cut-elimination; analycity
Summary/Abstract: This paper is about non-labelled proof-systems for hybrid logic, that is, proofsystems 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 nonlabelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations.
Journal: Bulletin of the Section of Logic
- Issue Year: 51/2022
- Issue No: 2
- Page Range: 143-162
- Page Count: 20
- Language: English