In this paper ontological implications of the Barcan formula and its converse will be discussed at the conceptual and technical level. The thesis that will be defended is that sentential moods are not ontologically neutral since the rejection of ontological implications of Barcan formula and its converse is a condition of a possibility of the imperative mood. The paper is divided into four sections. In the first section a systematization of semantical systems of quantified modal logic is introduced for the (...) purpose of making explicit their ontological presuppositions. In this context Jadacki's ontological difference between being and existence is discussed and analyzed within the framework of hereby proposed system of quantified modal logic. The second section discusses ontological implications of the Barcan formula and its converse within the system accommodating the difference between being and existence. The third section presents a proof of incompatibility of the Barcan formula and its converse with the use of imperatives. In the concluding section, a thesis on logical pragmatics foreclosing the dilemma between necessitism and contingentism is put forward and defended against some objections. (shrink)

This is a companion paper to Braüner where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic.

Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an ω–type schema of inference that naturally interpret the propositional and the predicate until–free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set of (...) extralogical axioms). For each system we provide a syntactic proof of cut elimination and a proof of completeness. (shrink)