Abstract
This Chapter has an introductory character. The main objective of Section 1.1. has been to recall the basic information on the language of classical propositional logic – CPL and on the quantificational logic in classical (CQL) and free version (FQL). The approach chosen here is rather informal. In case of CPL we introduce only the language and syntactical conventions applied throughout, while in case of QL, a brief outline of classical and free logic is additionaly highlighted by some comments concerning philosophical motivations. The section contains also some technical information, e.g. on relations and trees, essential in the foregoing. It should be emphasized that this section is just to establish notation and to keep the text self-contained, so much of it may be skipped in the first reading and consulted when necessary for understanding later chapters.
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.
In case we use additional functor \(\leftrightarrow \) we assume that \(\rightarrow \) binds tighter.
- 2.
Sometimes the reduct of this language without = will be considered called \({\bf L_{QL}}\).
- 3.
We will use to signal the end of the remark.
- 4.
For more information on different versions of free logic and their semantics consult e.g. Bencivenga [25].
- 5.
Sometimes logics of this sort are called inclusive, particularly in contexts where the problem of empty domains is considered separately from the problem of non-denoting terms – there are logics which are inclusive but not free.
- 6.
We assume that E is present in a language as primitive or definable by =, otherwise the axiomatization is slightly more complicated.
- 7.
More formally, the set of tautologies is not recursive but still it is recursively enumerable. In fact, undecidability of QL follows from the so called Church-Turing thesis which is not provable but commonly believed to be true. It is a claim that the set of computable functions coincides with the set of functions computable on any of the proposed mathematical models of computation, like Turing machines.
- 8.
It may seem at first sight that the separation of these two types of rules in some kind of ND systems is incoherent with our general characterization of a calculus. But it is apparent, because every proof construction rule of the form (1.6) may be also presented as an instance of a rule (1.5) with sequents \(X_i\Rightarrow Y_i\) as premises and \(Z\Rightarrow W\) as (the only) conclusion. It is just a notational convention for making clear the difference between such rules in ND L-systems using formulae and ND systems using sequents, where separation of proof construction rules does not make sense, cf. Section 2.3.
- 9.
That’s why in literature it is often said that the rule is eliminable.
- 10.
We do not introduce formally the concepts of computable functions because the questions of computability and complexity theory are not the subject of this book but cf. some elementary remarks in Section 5.5. The above informal characterization of p-simulation will do for our interests; the reader may consult e.g. D’Agostino [2] or Schmidt [242] for more information on several forms of simulation.
- 11.
This property is a generalization of the concept of L-validity of rules introduced for rules of inference which preserve the set of L-tautologies; cf. e.g. Pogorzelski ([215].
- 12.
In case of resolution calculi this claim may be disputable. But we mean here the so called direct resolution calculi for modal logics i.e. with no use of translation to e.g. first-order logic, cf. Section 3.2.
- 13.
Reference
Wójcicki, R. Theory of logical calculi. Dordrecht: Kluwer.
De Nivelle, H., R.A. Schmidt, and U. Hustadt. 2000. Resolution-based methods for modal logics. Logic Journal of the IGPL 8(3): 265–292.
Blackburn, P., M. DeRijke, and Y. Venema. 2001. Modal logic. Cambridge: Cambridge University Press.
Pogorzelski, W.A. 1973. Klasyczny rachunek zdań. Warszawa: PWN.
Prawitz, D. 1965. Natural deduction. Stockholm: Almqvist and Wiksell.
Smullyan, R. 1968. First-order logic. Berlin: Springer.
Garson, J.W. 2006. Modal logic for philosophers. Cambridge: Cambridge University Press.
D’Agostino, M. 1999. Tableau methods for classical propositional logic. In Handbook of tableau methods, eds. M. D’Agostino et al., 45–123. Dordrecht: Kluwer Academic Publishers.
Goranko, V. 1994. Refutation systems in modal logic. Studia Logica 53(2): 229–234.
Simpson, A. 1994. The Proof Theory and Semantics of Intuitionistic Modal Logic, PhD thesis, University of Edinburgh.
Church, A. 1956. Introduction to Mathematical Logic, vol I. Princeton: Princeton University Press.
Fitting, M., and R.L. Mendelsohn. 1998. First-order modal logic. Dordrecht: Kluwer.
Wallen, L.A. 1990. Automated proof search in non-classical logics. Cambridge: MIT Press.
Skura, T. 1992. Refutation rules for three modal logics. Bulletin of the Section of Logic 21(1): 31–32.
Vickers, S. 1988. Topology via logic. Cambridge: Cambridge University Press.
Bencivenga, E. 1986. Free logics. In Handbook of Philosophical Logic, eds. D. Gabbay, and F. Guenthner, vol III, 373–426. Dordrecht: Reidel Publishing Company.
Schmidt, R.A. 2006. Developing modal tableaux and resolution methods via first-order resolution. In Advances in modal logic 6, ed. M. deRijke, 107–135. Dordrecht: Kluwer.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Indrzejczak, A. (2010). Preliminaries. In: Natural Deduction, Hybrid Systems and Modal Logics. Trends in Logic, vol 30. Springer, Dordrecht. https://doi.org/10.1007/978-90-481-8785-0_1
Download citation
DOI: https://doi.org/10.1007/978-90-481-8785-0_1
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-8784-3
Online ISBN: 978-90-481-8785-0
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)