Abstract
In this chapter we compare the hybrid-logical natural deduction system given in Section 2.2 to a labelled natural deduction system for modal logic. The chapter is structured as follows. In the first section of the chapter we describe the labelled natural deduction system under consideration and in the second section we define a translation from this system to the hybrid-logical natural deduction system given in Section 2.2. In the third section we compare reductions in the two systems. The material in this chapter is taken from Braüner(2007).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This is actually a generally occurring problem (with a generally applicable solution) since the same problem crops up (and is solved in the same way) in connection with normalization for intuitionistic hybrid logic, cf. Section 8.2.4, and normalization for first-order hybrid logic, cf. Section 6.2.4. In the first case the reduction rule for the connective ◊, which in intuitionistic hybrid logic is primitive, not defined, might generate new maximum formulas on the form \(@_{a} \lozenge e\), and in the second case, the reduction rule for ∀ might generate new maximum formulas on the form \(@_{a} E(t)\) where \(E(t)\), called the existence predicate, is an abbreviation for \(\exists y (y = t)\) which in turn is an abbreviation for \(\neg \forall y \neg (y = t)\).
- 2.
Melvin Fitting has pointed out that the rules for ♯ are sound with respect to models based on the integers ordered by the successor relation, where \(\sharp \phi\) is true at a point if and only if φ is true at the next point. This is a case of discrete, linear time. Note that the operator ♯ is self-dual as the dual operator \(\neg \sharp \neg\) gets the same interpretation as ♯. Actually, in such models the standard modal operators □ and ◊ collapse and get the same interpretation as ♯.
References
T. Braüner. Why does the proof-theory of hybrid logic work so well? Journal of Applied Non-Classical Logics, 17:521–543, 2007.
D. Basin, S. Matthews, and L. Viganò. Labelled propositional modal logics: Theory and practice. Journal of Logic and Computation, 7:685–717, 1997.
D. Prawitz. Natural Deduction. A Proof-Theoretical Study. Almqvist and Wiksell, Stockholm, 1965.
D. Prawitz. Ideas and results in proof theory. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and The Foundations of Mathematics, pages 235–307. North-Holland, 1971.
A. Simpson. The Proof Theory and Semantics of Intuitionistic Modal logic. PhD thesis, University of Edinburgh, 1994.
L. Viganò. Labelled Non-classical Logics. Kluwer, 2000.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2011 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Braüner, T. (2011). Labelled Versus Internalized Natural Deduction. In: Hybrid Logic and its Proof-Theory. Applied Logic Series, vol 37. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-0002-4_9
Download citation
DOI: https://doi.org/10.1007/978-94-007-0002-4_9
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-007-0001-7
Online ISBN: 978-94-007-0002-4
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)