First-order modal logic, in the usual formulations, is not suf- ﬁciently expressive, and as a consequence problems like Frege’s morning star/evening star puzzle arise. The introduction of predicate abstraction machinery provides a natural extension in which such diﬃculties can be addressed. But this machinery can also be thought of as part of a move to a full higher-order modal logic. In this paper we present a sketch of just such a higher-order modal logic: its formal semantics, and a proof procedure using tableaus. Naturally the tableau rules are not complete, but they are with respect to a Henkinization of the “true” semantics. We demonstrate the use of the tableau rules by proving one of the theorems involved in G¨ odel’s ontological argument, one of the rare instances in the literature where higher-order modal constructs have appeared. A fuller treatment of the material presented here is in preparation.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
First-Order Intensional Logic.Melvin Fitting - 2004 - Annals of Pure and Applied Logic 127 (1-3):171-193.
Representability in Second-Order Propositional Poly-Modal Logic.G. Aldo Antonelli & Richmond H. Thomason - 2002 - Journal of Symbolic Logic 67 (3):1039-1054.
Generalized Quantifiers and Modal Logic.Wiebe Van Der Hoek & Maarten De Rijke - 1993 - Journal of Logic, Language and Information 2 (1):19-58.
Identity in Modal Logic Theorem Proving.Francis J. Pelletier - 1993 - Studia Logica 52 (2):291 - 308.
The Translation of First Order Logic Into Modal Predicate Logic.Beomin Kim - 2008 - Proceedings of the Xxii World Congress of Philosophy 13:65-69.
Added to index2010-12-22
Total downloads28 ( #181,895 of 2,163,984 )
Recent downloads (6 months)1 ( #348,017 of 2,163,984 )
How can I increase my downloads?