Timothy Williamson has argued that in the debate on modal ontology, the familiar distinction between actualism and possibilism should be replaced by a distinction between positions he calls contingentism and necessitism. He has also argued in favor of necessitism, using results on quantified modal logic with plurally interpreted second-order quantifiers showing that necessitists can draw distinctions contingentists cannot draw. Some of these results are similar to well-known results on the relative expressivity of quantified modal logics with so-called inner and outer (...) quantifiers. The present paper deals with these issues in the context of quantified modal logics with generalized quantifiers. Its main aim is to establish two results for such a logic: Firstly, contingentists can draw the distinctions necessitists can draw if and only if the logic with inner quantifiers is at least as expressive as the logic with outer quantifiers, and necessitists can draw the distinctions contingentists can draw if and only if the logic with outer quantifiers is at least as expressive as the logic with inner quantifiers. Secondly, the former two items are the case if and only if all of the generalized quantifiers are first-order definable, and the latter two items are the case if and only if first-order logic with these generalized quantifiers relativizes. (shrink)

The aim of this paper is to initiate a systematic exploration of the model theory of epistemic plausibility models (EPMs). There are two subtly different definitions in the literature: one by van Benthem and one by Baltag and Smets. Because van Benthem's notion is the most general, most of the paper is dedicated to this notion. We focus on the notion of bisimulation, and show that the most natural generalization of bisimulation to van Benthem-type EPMs fails. We then introduce parametrized (...) bisimulations, and prove various bisimulationimplies- equivalence theorems, a Hennessy-Milner theorem, and several (un)definability results. We discuss the problems arising from the fact that these bisimulations are syntax-dependent (and thus not fully structural), and we present and compare two different ways of coping with this issue: adding a modality to the language, and putting extra constraints on the models. We argue that the most successful solution involves restricting to uniform and locally connected (van Benthem-type) EPMs: for this subclass the intuitively most natural notion of bisimulation and the technically sound notion coincide. Such EPMs turn out to correspond exactly with Baltag/Smets-type EPMs, which can be interpreted as constituting a methodological argument, favoring Baltag and Smets's definition of EPM over that of van Benthem. (shrink)

Like modal logic, temporal logic, and description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoare-style proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we (...) propose a selection of landmark results about decidability, complexity and expressive power. (shrink)

This paper studies Aumann’s agreeing to disagree theorem from the perspective of dynamic epistemic logic. This was first done by Dégremont and Roy (J Phil Log 41:735–764, 2012) in the qualitative framework of plausibility models. The current paper uses a probabilistic framework, and thus stays closer to Aumann’s original formulation. The paper first introduces enriched probabilistic Kripke frames and models, and various ways of updating them. This framework is then used to prove several agreement theorems, which are natural formalizations of (...) Aumann’s original result. Furthermore, a sound and complete axiomatization of a dynamic agreement logic is provided, in which one of these agreement theorems can be derived syntactically. These technical results are used to show the importance of explicitly representing the dynamics behind the agreement theorem, and lead to a clarification of some conceptual issues surrounding the agreement theorem, in particular concerning the role of common knowledge. The formalization of the agreement theorem thus constitutes a concrete example of the so-called dynamic turn in logic. (shrink)

Building on Ben-Avi and Winter’s (2007) work, this paper provides a general “intensionalization” procedure that turns an extensional semantics for a language into an intensionalized one that is capable of accommodating “truly intensional” lexical items without changing the compositional semantic rules. We prove some formal properties of this procedure and clarify its relation to the procedure implicit in Montague’s (1973) PTQ.

We study finitely generated free Heyting algebras from a topological and from a model theoretic point of view. We review Bellissima’s representation of the finitely generated free Heyting algebra; we prove that it yields an embedding in the profinite completion, which is also the completion with respect to a naturally defined metric. We give an algebraic interpretation of the Kripke model used by Bellissima as the principal ideal spectrum and show it to be first order interpretable in the Heyting algebra, (...) from which several model theoretic and algebraic properties are derived. In particular, we prove that a free finitely generated Heyting algebra has only one set of free generators, which is definable in it. As a consequence its automorphism group is the permutation group over its generators. (shrink)

The paper introduces a first-order theory in the language of predicate tense logic which contains a single simple axiom. It is shewn that this theory enables times to be referred to and sentences involving ‘now’ and ‘then’ to be formalised. The paper then compares this way of increasing the expressive capacity of predicate tense logic with other mechanisms, and indicates how to generalise the results to other modal and tense systems.

In a number of publications A.N. Prior considered the use of what he called ‘metric tense logic’. This is a tense logic in which the past and future operators P and F have an index representing a temporal distance, so that Pnα means that α was true n -much ago, and Fn α means that α will be true n -much hence. The paper investigates the use of metric predicate tense logic in formalising phenomena ormally treated by such devices as (...) multiple indexing or quantification over times. (shrink)

We provide syntactic necessary and sufficient conditions on the formulae reducible by the second-order quantifier elimination algorithm DLS. It is shown that DLS is compete for all modal Sahlqvist and Inductive formulae, and that all modal formulae in a single propositional variable on which DLS succeeds are canonical.

In a previous work we introduced the algorithm \SQEMA\ for computing first-order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of (...) \SQEMA\ where that syntactic condition is replaced by a semantic one, viz. downward monotonicity. For the first, and most general, extension \SSQEMA\ we prove correctness for a large class of modal formulae containing an extension of the Sahlqvist formulae, defined by replacing polarity with monotonicity. By employing a special modal version of Lyndon's monotonicity theorem and imposing additional requirements on the Ackermann rule we obtain restricted versions of \SSQEMA\ which guarantee canonicity, too. (shrink)

Supervaluationism is a well known theory of vagueness. Subvaluationism is a less well known theory of vagueness. But these theories cannot be taken apart, for they are in a relation of duality that can be made precise. This paper provides an introduction to the subvaluationist theory of vagueness in connection to its dual, supervaluationism. A survey on the supervaluationist theory can be found in the Compass paper of Keefe (2008); our presentation of the theory in this paper will be short (...) to get rapidly into the logical issues. This paper is relatively self-contained. A modest background on propositional modal logic is, though not strictly necessary, advisable. The reader might find useful the Compass papers Kracht (2011) and Negri (2011) (though these papers cover issues of more complexity than what is demanded to follow this paper). (shrink)

Paraconsistent approaches have received little attention in the literature on vagueness (at least compared to other proposals). The reason seems to be that many philosophers have found the idea that a contradiction might be true (or that a sentence and its negation might both be true) hard to swallow. Even advocates of paraconsistency on vagueness do not look very convinced when they consider this fact; since they seem to have spent more time arguing that paraconsistent theories are at least as (...) good as their paracomplete counterparts, than giving positive reasons to believe on a particular paraconsistent proposal. But it sometimes happens that the weakness of a theory turns out to be its mayor ally, and this is what (I claim) happens in a particular paraconsistent proposal known as subvaluationism. In order to make room for truth-value gluts subvaluationism needs to endorse a notion of logical consequence that is, in some sense, weaker than standard notions of consequence. But this weakness allows the subvaluationist theory to accommodate higher-order vagueness in a way that it is not available to other theories of vagueness (such as, for example, its paracomplete counterpart, supervaluationism). (shrink)

Basic hybrid logic extends modal logic with the possibility of naming worlds by means of a distinguished class of atoms (called nominals) and the so-called satisfaction operator, that allows one to state that a given formula holds at the world named a, for some nominal a. Hence, in particular, hybrid formulae include “equality” assertions, stating that two nominals are distinct names for the same world. The treatment of such nominal equalities in proof systems for hybrid logics may induce many redundancies. (...) This paper introduces an internalized tableau system for basic hybrid logic, significantly reducing such redundancies. The calculus enjoys a strong termination property: tableau construction terminates without relying on any specific rule application strategy, and no loop-checking is needed. The treatment of nominal equalities specific of the proposed calculus is briefly compared to other approaches. Its practical advantages are demonstrated by empirical results obtained by use of implemented systems. Finally, it is briefly shown how to extend the calculus to include the global and converse modalities. (shrink)

In this paper, we review three influential theories of imagination in order to understand how the dynamics of imagination acts could be modeled using formal languages. While reviewing them, we notice that they are not detailed enough to account for all the mechanisms involved in creating and developing imaginary worlds. We claim those theories could be further refined into what we call the Common Frame for Imagination Acts, which defines a framework that can be used to study the dynamics of (...) imagination using formal languages, and we support our claim by showing how the framework allows to model certain imagination acts step by step. Then, we introduce the Rhombus of Imagination, which is a visual tool that can be used in conjunction with our framework to study the procedural structure of different kinds of imagination acts and identify their dynamic properties. (shrink)

A number of significant contributions in the last four decades show that non-normal modal logics can be fruitfully employed in several applied fields. Well-known domains are epistemic logic, deontic logic, and systems capturing different aspects of action and agency such as the modal logic of agency, concurrent propositional dynamic logic, game logic, and coalition logic. Semantics for such logics are traditionally based on neighbourhood models. However, other model-theoretic semantics can be used for this purpose. Here, we systematically study multi-relational structures, (...) whose investigation is still relatively underdeveloped. After a brief introduction to two different versions of multi-relational semantics – which we call strong and weak multi-relational semantics – we proceed to study several modal schemata. Special attention is paid to the schemata CON and D. Finally we offer completeness proofs for several systems using both strong and weak semantic tools: The proofs thus cover both classical system.. (shrink)

This paper offers a semantic study in multi-relational semantics of quantified N-Monotonic modal logics with varying domains with and without the identity symbol. We identify conditions on frames to characterise Barcan and Ghilardi schemata and present some related completeness results. The characterisation of Barcan schemata in multi-relational frames with varying domains shows the independence of BF and CBF from well-known propositional modal schemata, an independence that does not hold with constant domains. This fact was firstly suggested for classical modal systems (...) by Stolpe, 557–575, 2003), but unfortunately that work used only models and not frames. (shrink)

The aim of the work is to provide a language to reason about Closed Interactions, i.e. all those situations in which the outcomes of an interaction can be determined by the agents themselves and in which the environment cannot interfere with they are able to determine. We will see that two different interpretations can be given of this restriction, both stemming from Pauly Representation Theorem. We will identify such restrictions and axiomatize their logic. We will apply the formal tools to (...) reason about games and their regulation. (shrink)

We investigate an aspect of defeasibility that has somewhat been overlooked by the non-monotonic reasoning community, namely that of defeasible modes of reasoning. These aim to formalise defeasibility of the traditional notion of necessity in modal logic, in particular of its different readings as action, knowledge and others in specific contexts, rather than defeasibility of conditional forms. Building on an extension of the preferential approach to modal logics, we introduce new modal osperators with which to formalise the notion of defeasible (...) necessity and distinct possibility, and that can be used to represent expected effects, refutable knowledge, and so on. We show how KLM-style conditionals can smoothly be integrated with our richer language. We also propose a tableau calculus which is sound and complete with respect to our modal preferential semantics, and of which the computational complexity remains in the same class as that of the underlying classical modal logic. (shrink)

There are various contexts in which it is not pertinent to generate and attend to all the classical consequences of a given premiss—or to trace all the premisses which classically entail a given consequence. Such contexts may involve limited resources of an agent or inferential engine, contextual relevance or irrelevance of certain consequences or premisses, modelling everyday human reasoning, the search for plausible abduced hypotheses or potential causes, etc. In this paper we propose and explicate one formal framework for a (...) whole spectrum of consequence relations, flexible enough to be tailored for choices from a variety of contexts. We do so by investigating semantic constraints on classical entailment which give rise to a family of infra-classical logics with appealing properties. More specifically, our infra-classical reasoning demands (beyond ${\alpha\models\beta}$ ) that Mod(β) does not run wild, but lies within the scope (whatever that may mean in some specific context) of Mod(α), and which can be described by a sentence ${\bullet\alpha}$ with ${\beta\models\bullet\alpha}$ . Besides being infra-classical, the resulting logic is also non-monotonic and allows for non-trivial reasoning in the presence of inconsistencies. (shrink)

It is well known that the convex hull of the classical truth value functions contains all and only the probability functions. Work by Paris and Williams has shown that this also holds for various kinds of nonclassical logics too. This note summarises the formal details of this topic and extends the results slightly.

We introduce quantificational modal operators as dynamic modalities with (extensions of) Henkin quantifiers as indices. The adoption of matrices of indices (with action identifiers, variables and/or quantified variables as entries) gives an expressive formalism which is here motivated with examples from the area of multi-agent systems. We study the formal properties of the resulting logic which, formally speaking, does not satisfy the normality condition. However, the logic admits a semantics in terms of (an extension of) Kripke structures. As a consequence, (...) standard techniques for normal modal logic become available. We apply these to prove completeness and decidability, and to extend some standard frame results to this logic. (shrink)

The paper aims at studying, in full generality, logics defined by imposing a variable inclusion condition on a given logic \. We prove that the description of the algebraic counterpart of the left variable inclusion companion of a given logic \ is related to the construction of Płonka sums of the matrix models of \. This observation allows to obtain a Hilbert-style axiomatization of the logics of left variable inclusion, to describe the structure of their reduced models, and to locate (...) them in the Leibniz hierarchy. (shrink)

This paper supersedes an ealier version, entitled "A Non-Standard Semantics for Inexact Knowledge with Introspection", which appeared in the Proceedings of "Rationality and Knowledge". The definition of token semantics, in particular, has been modified, both for the single- and the multi-agent case.

In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity).We show that hybrid logic offers a genuinely first-order perspective on Kripke semantics: it is possible to define base logics which extend automatically to a (...) wide variety of frame classes and to prove completeness using the Henkin method. In the weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic. (shrink)

The title reflects my conviction that, viewed semantically,modal logic is fundamentally dialogical; this conviction is based on the key role played by the notion of bisimulation in modal model theory. But this dialogical conception of modal logic does not seem to apply to modal proof theory, which is notoriously messy. Nonetheless, by making use of ideas which trace back to Arthur Prior (notably the use of nominals, special proposition symbols which ‘name’ worlds) I will show how to lift the dialogical (...) conception to modal proof theory. I argue that this shift to hybrid logic has consequences for both modal and dialogical logic, and I discuss these in detail. (shrink)

Contemporary hybrid logic is based on the idea of using formulas as terms, an idea invented and explored by Arthur Prior in the mid-1960s. But Prior’s own work on hybrid logic remains largely undiscussed. This is unfortunate, since hybridisation played a role that was both central to and problematic for his philosophical views on tense. In this paper I introduce hybrid logic from a contemporary perspective, and then examine the role it played in Prior’s work.

Within ZFC, we develop a general technique to topologize trees that provides a uniform approach to topological completeness results in modal logic with respect to zero-dimensional Hausdorff spaces. Embeddings of these spaces into well-known extremally disconnected spaces then gives new completeness results for logics extending S4.2.

We show that subspaces of the space ${\mathbb{Q}}$ of rational numbers give rise to uncountably many d-logics over K4 without the finite model property.

We introduce the concept of a connected logic (over S4) and show that each connected logic with the finite model property is the logic of a subalgebra of the closure algebra of all subsets of the real line R, thus generalizing the McKinsey-Tarski theorem. As a consequence, we obtain that each intermediate logic with the finite model property is the logic of a subalgebra of the Heyting algebra of all open subsets of R.

We establish the dichotomy property for stable canonical multi-conclusion rules for IPC, K4, and S4. This yields an alternative proof of existence of explicit bases of admissible rules for these logics.

In this paper we show a duality between two approaches to represent quantum structures abstractly and to model the logic and dynamics therein. One approach puts forward a “quantum dynamic frame” :2267–2282, 2005), a labelled transition system whose transition relations are intended to represent projections and unitaries on a Hilbert space. The other approach considers a “Piron lattice”, which characterizes the algebra of closed linear subspaces of a Hilbert space. We define categories of these two sorts of structures and show (...) a duality between them. This result establishes, on one direction of the duality, that quantum dynamic frames represent quantum structures correctly; on the other direction, it gives rise to a representation of dynamics on a Piron lattice. (shrink)

Issues about information spring up wherever one scratches the surface of logic. Here is a case that raises delicate issues of 'factual' versus 'procedural' information, or 'statics' versus 'dynamics'. What does intuitionistic logic, perhaps the earliest source of informational and procedural thinking in contemporary logic, really tell us about information? How does its view relate to its 'cousin' epistemic logic? We discuss connections between intuitionistic models and recent protocol models for dynamic-epistemic logic, as well as more general issues that emerge.

We make a proposal for formalizing simultaneous games at the abstraction level of player's powers, combining ideas from dynamic logic of sequential games and concurrent dynamic logic. We prove completeness for a new system of 'concurrent game logic' CDGL with respect to finite non-determined games. We also show how this system raises new mathematical issues, and throws light on branching quantifiers and independence-friendly evaluation games for first-order logic.

Taking Backward Induction as its running example, this paper explores avenues for a logic of information-driven social action. We use recent results on limit phenomena in knowledge updating and belief revision, procedural rationality, and a ‘Theory of Play’ analyzing how games are played by different agents.

This paper presents a new modal logic for ceteris paribus preferences understood in the sense of "all other things being equal". This reading goes back to the seminal work of Von Wright in the early 1960's and has returned in computer science in the 1990' s and in more abstract "dependency logics" today. We show how it differs from ceteris paribus as "all other things being normal", which is used in contexts with preference defeaters. We provide a semantic analysis and (...) several completeness theorems. We show how our system links up with Von Wright's work, and how it applies to game-theoretic solution concepts, to agenda setting in investigation, and to preference change. We finally consider its relation with infinitary modal logics. (shrink)

One of the most dominant approaches to semantics for relevant (and many paraconsistent) logics is the Routley-Meyer semantics involving a ternary relation on points. To some (many?), this ternary relation has seemed like a technical trick devoid of an intuitively appealing philosophical story that connects it up with conditionality in general. In this paper, we respond to this worry by providing three different philosophical accounts of the ternary relation that correspond to three conceptions of conditionality. We close by briefly discussing (...) a general conception of conditionality that may unify the three given conceptions. (shrink)

We introduce a propositional many-valued modal logic which is an extension of the Continuous Propositional Logic to a modal system. Otherwise said, we extend the minimal modal logic to a Continuous Logic system. After introducing semantics, axioms and deduction rules, we establish some preliminary results. Then we prove the equivalence between consistency and satisfiability. As straightforward consequences, we get compactness, an approximated completeness theorem, in the vein of Continuous Logic, and a Pavelka-style completeness theorem.

This paper introduces an axiomatisation for equational hybrid logic based on previous axiomatizations and natural deduction systems for propositional and first-order hybrid logic. Its soundness and completeness is discussed. This work is part of a broader research project on the development a general proof calculus for hybrid logics.

The main aim of this paper is to present a way to improve the e.ciency of an intelligent alarm correlation module by means of an abductive reasoner. The alarm correlation module is integrated in a more complex system that performs monitoring and control tasks over a tract of a highway. On the basis of a specific theory on the domain, explanations of anomalous traffic patterns can be provided taking into account those situations not directly detected by data acquisition technology. The (...) integration of the comprehensive view obtained by means of a correlation phase with additional domain knowledge allows to abduce from the observed anomalous traffic patterns other significant situations. The experience of traffic operators allows to build a theory of abducible explanations that exploits the knowledge of the use context of the system. The correlation module of SAMOT has been modelled within a propositional modal language, named ST-Logic, which will be adopted for the abductive reasoner as well. Finally, some remarks about stratified interpretative cycles made possible within such a formal framework will be addressed. (shrink)

We formalize what it means to have permission to say something. We adapt the dynamic logic of permission by van der Meyden (J Log Comput 6(3):465–479, 1996 ) to the case where atomic actions are public truthful announcements. We also add a notion of obligation. Our logic is an extension of the logic of public announcements introduced by Plaza ( 1989 ) with dynamic modal operators for permission and for obligation. We axiomatize the logic and show that it is decidable.

The probabilization of a logic system consists of enriching the language (the formulas) and the semantics (the models) with probabilistic features. Such an operation is said to be exogenous if the enrichment is done on top, without internal changes to the structure, and is called endogenous otherwise. These two different enrichments can be applied simultaneously to the language and semantics of a same logic. We address the problem of studying the transference of metaproperties, such as completeness and decidability, to the (...) exogenous probabilization of an abstract logic system. First, we setup the necessary framework to handle the probabilization of a satisfaction system by proving transference results within a more general context. In this setup, we define a combination mechanism of logics through morphisms and prove sufficient condition to guarantee completeness and decidability. Then, we demonstrate that probabilization is a special case of this exogenous combination method, and that it fulfills the general conditions to obtain transference of completeness and decidability. Finally, we motivate the applicability of our technique by analyzing the probabilization of the linear temporal logic over Markov chains, which constitutes an endogenous probabilization. The results are obtained first by studying the exogenous semantics, and then by establishing an equivalence with the original probabilization given by Markov chains. (shrink)

Public announcement logic is an extension of multiagent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. We propose an extension of public announcement logic with a dynamic modal operator that expresses what is true after any announcement: after which , does it hold that Kφ? We give various semantic results and show completeness for a Hilbert-style axiomatization of this logic. There is a natural generalization to a logic for arbitrary events.

We investigate the process of truth-seeking by iterated belief revision with higher-level doxastic information . We elaborate further on the main results in Baltag and Smets (Proceedings of TARK, 2009a , Proceedings of WOLLIC’09 LNAI 5514, 2009b ), applying them to the issue of convergence to truth . We study the conditions under which the belief revision induced by a series of truthful iterated upgrades eventually stabilizes on true beliefs. We give two different conditions ensuring that beliefs converge to “full” (...) (complete) truth , as well as a condition ensuring only that they converge to true (but not necessarily complete) beliefs. (shrink)

In this paper, we study indiscernibility relations and complementarity relations in hyper arrow structures. A first-order characterization of indiscernibility and complementarity is obtained through a duality result between hyper arrow structures and certain structures of relational type characterized by first-order conditions. A modal analysis of indiscernibility and complementarity is performed through a modal logic which modalities correspond to indiscernibility relations and complementarity relations in hyper arrow structures.

The aim of this paper is to give new kinds of modal logics suitable for reasoning about regions in discrete spaces. We call them dynamic logics of the region-based theory of discrete spaces. These modal logics are linguistic restrictions of propositional dynamic logic with the global diamond E. Their formulas are equivalent to Boolean combinations of modal formulas like E(A ∧ ⟨α⟩ B) where A and B are Boolean terms and α is a relational term. Examining what we can say (...) about dynamic models when we use formulas to describe them, we successively address the axiomatization/completeness issue and the decidability/complexity issue of our dynamic logics of the region-based theory of discrete spaces. (shrink)

This paper presents a simple decidable logic of functional dependence LFD, based on an extension of classical propositional logic with dependence atoms plus dependence quantifiers treated as modalities, within the setting of generalized assignment semantics for first order logic. The expressive strength, complete proof calculus and meta-properties of LFD are explored. Various language extensions are presented as well, up to undecidable modal-style logics for independence and dynamic logics of changing dependence models. Finally, more concrete settings for dependence are discussed: continuous (...) dependence in topological models, linear dependence in vector spaces, and temporal dependence in dynamical systems and games. (shrink)

This paper sets out a new way of combining Kripke-complete modal logics: lexicographic product. It discusses some basic properties of the lexicographic product construction and proves axiomatization/completeness results.

In this work, we investigate the relationship between paraconsistent semantics and some well-known topological spaces such as connected and continuous spaces. We also discuss homotopies as truth preserving operations in paraconsistent topological models.

This paper defines a Sahlqvist fragment for relevant logic and establishes that each class of frames in the Routley-Meyer semantics which is definable by a Sahlqvist formula is also elementary, that is, it coincides with the class of structures satisfying a given first order property calculable by a Sahlqvist-van Benthem algorithm. Furthermore, we show that some classes of Routley-Meyer frames definable by a relevant formula are not elementary.