FIRST-ORDER POSSIBILITY MODELS AND FINITARY COMPLETENESS PROOFS

AbstractThis article builds on Humberstone’s idea of defining models of propositional modal logic where total possible worlds are replaced by partial possibilities. We follow a suggestion of Humberstone by introducing possibility models for quantified modal logic. We show that a simple quantified modal logic is sound and complete for our semantics. Although Holliday showed that for many propositional modal logics, it is possible to give a completeness proof using a canonical model construction where every possibility consists of finitely many formulas, we show that this is impossible to do in the first-order case. However, one can still construct a canonical model where every possibility consists of a computable set of formulas and thus still of finitely much information.

Download Full-text

QUANTIFIED MODAL LOGIC ON THE RATIONAL LINE

The Review of Symbolic Logic ◽

10.1017/s1755020314000021 ◽

2014 ◽

Vol 7 (3) ◽

pp. 439-454 ◽

Cited By ~ 4

Author(s):

PHILIP KREMER

Keyword(s):

Modal Logic ◽

Real Line ◽

Topological Spaces ◽

Topological Semantics ◽

Cantor Space ◽

Quantified Modal Logic ◽

Propositional Modal Logic ◽

The Family ◽

Modal Logic S4 ◽

Rational Line

AbstractIn the topological semantics for propositional modal logic, S4 is known to be complete for the class of all topological spaces, for the rational line, for Cantor space, and for the real line. In the topological semantics for quantified modal logic, QS4 is known to be complete for the class of all topological spaces, and for the family of subspaces of the irrational line. The main result of the current paper is that QS4 is complete, indeed strongly complete, for the rational line.

Download Full-text

Logical Tools

10.1093/oso/9780192846655.003.0002 ◽

2021 ◽

pp. 14-52

Author(s):

Cian Dorr ◽

John Hawthorne ◽

Juhani Yli-Vakkuri

Keyword(s):

Modal Logic ◽

Possible Worlds ◽

Higher Order ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

System P

This chapter presents the system of classical higher-order modal logic which will be employed throughout this book. Nothing more than a passing familiarity with classical first-order logic and standard systems of modal logic is presupposed. We offer some general remarks about the kind of commitment involved in endorsing this logic, and motivate some of its more non-standard features. We also discuss how talk about possible worlds can be represented within the system.

Download Full-text

EVERYONE KNOWS THAT SOMEONE KNOWS: QUANTIFIERS OVER EPISTEMIC AGENTS

The Review of Symbolic Logic ◽

10.1017/s1755020318000497 ◽

2019 ◽

Vol 12 (2) ◽

pp. 255-270 ◽

Cited By ~ 1

Author(s):

PAVEL NAUMOV ◽

JIA TAO

Keyword(s):

Modal Logic ◽

Epistemic Logic ◽

Possible Worlds ◽

Completeness Theorem ◽

Kripke Semantics ◽

Possible Worlds Semantics ◽

Distributed Knowledge ◽

First Order ◽

Soundness And Completeness ◽

First Order Modal Logic

AbstractModal logic S5 is commonly viewed as an epistemic logic that captures the most basic properties of knowledge. Kripke proved a completeness theorem for the first-order modal logic S5 with respect to a possible worlds semantics. A multiagent version of the propositional S5 as well as a version of the propositional S5 that describes properties of distributed knowledge in multiagent systems has also been previously studied. This article proposes a version of S5-like epistemic logic of distributed knowledge with quantifiers ranging over the set of agents, and proves its soundness and completeness with respect to a Kripke semantics.

Download Full-text

REALIZABILITY SEMANTICS FOR QUANTIFIED MODAL LOGIC: GENERALIZING FLAGG’S 1985 CONSTRUCTION

The Review of Symbolic Logic ◽

10.1017/s1755020316000095 ◽

2016 ◽

Vol 9 (4) ◽

pp. 752-809 ◽

Cited By ~ 2

Author(s):

BENJAMIN G. RIN ◽

SEAN WALSH

Keyword(s):

Modal Logic ◽

Graph Model ◽

Church’S Thesis ◽

Quantified Modal Logic ◽

First Order ◽

Continuity Principle ◽

Generalized Continuity ◽

Church's Thesis ◽

Order Arithmetic ◽

The Stability

AbstractA semantics for quantified modal logic is presented that is based on Kleene’s notion of realizability. This semantics generalizes Flagg’s 1985 construction of a model of a modal version of Church’s Thesis and first-order arithmetic. While the bulk of the paper is devoted to developing the details of the semantics, to illustrate the scope of this approach, we show that the construction produces (i) a model of a modal version of Church’s Thesis and a variant of a modal set theory due to Goodman and Scedrov, (ii) a model of a modal version of Troelstra’s generalized continuity principle together with a fragment of second-order arithmetic, and (iii) a model based on Scott’s graph model (for the untyped lambda calculus) which witnesses the failure of the stability of nonidentity.

Download Full-text

COMPLETENESS OF SECOND-ORDER PROPOSITIONAL S4 AND H IN TOPOLOGICAL SEMANTICS

The Review of Symbolic Logic ◽

10.1017/s1755020318000229 ◽

2018 ◽

Vol 11 (3) ◽

pp. 507-518

Author(s):

PHILIP KREMER

Keyword(s):

Modal Logic ◽

Intuitionistic Logic ◽

Second Order ◽

Topological Semantics ◽

First Order ◽

Propositional Modal Logic ◽

Propositional Quantifiers ◽

Modal Logic S4 ◽

Natural Way

AbstractWe add propositional quantifiers to the propositional modal logic S4 and to the propositional intuitionistic logic H, introducing axiom schemes that are the natural analogs to axiom schemes typically used for first-order quantifiers in classical and intuitionistic logic. We show that the resulting logics are sound and complete for a topological semantics extending, in a natural way, the topological semantics for S4 and for H.

Download Full-text

An incomplete decidable modal logic

Journal of Symbolic Logic ◽

10.2307/2274183 ◽

1984 ◽

Vol 49 (2) ◽

pp. 520-527 ◽

Cited By ~ 7

Author(s):

M. J. Cresswell

Keyword(s):

Modal Logic ◽

Possible Worlds ◽

Order Theory ◽

Finite Model ◽

Model Property ◽

Finite Model Property ◽

General Frame ◽

Propositional Modal Logic ◽

Modal Systems ◽

Modal Propositional Logic

The most common way of proving decidability in propositional modal logic is to shew that the system in question has the finite model property. This is not however the only way. Gabbay in [4] proves the decidability of many modal systems using Rabin's result in [8] on the decidability of the second-order theory of successor functions. In particular [4, pp. 258-265] he is able to prove the decidability of a system which lacks the finite model property. Gabbay's system is however complete, in the sense of being characterized by a class of frames, and the question arises whether there is a decidable modal logic which is not complete. Since no incomplete modal logic has the finite model property [9, p. 33], any proof of decidability must employ some such method as Gabbay's. In this paper I use the Gabbay/Rabin technique to prove the decidability of a finitely axiomatized normal modal propositional logic which is not characterized by any class of frames. I am grateful to the referee for suggesting improvements in substance and presentation.The terminology I am using is standard in modal logic. By a frame is understood a pair 〈W, R〉 in which W is a class (of “possible worlds”) and R ⊆ W2. To avoid confusion in what follows, a frame will henceforth be referred to as a Kripke frame. By contrast, a general frame is a pair 〈, Π〉 in which is a Kripke frame and Π is a collection of subsets of W closed under the Boolean operations and satisfying the condition that if A is in Π then so is R−1 “A. A model on a frame (of either kind) is obtained by adding a function V which assigns sets of worlds to propositional variables. In the case of a general frame we require that V(p) ∈ Π.

Download Full-text

Substance and first-order quantification over individual-concepts

Journal of Symbolic Logic ◽

10.2307/2273182 ◽

1980 ◽

Vol 45 (2) ◽

pp. 193-203 ◽

Cited By ~ 6

Author(s):

John Bacon

Keyword(s):

Modal Logic ◽

Possible Worlds ◽

Definite Descriptions ◽

Free Logic ◽

First Order ◽

Individual Concept ◽

The Past ◽

Individual Concepts ◽

The World ◽

Ordinary Usage

An individual-concept, hereinafter “individuation”, is a function from possible worlds to individuals. Constant individuations I will call “subsistents” (the notion will presently be generalized). A “substance”, after Thomason [35], is a subsistent whose value exists for the world at hand. In the systems of quantified modal logic developed over the past twenty years, the tendency has been to restrict the range of quantifiers to substances (often represented technically by the simple individuals that would be the values of the constant individuations), while allowing constant terms (particularly descriptions) to express arbitrary individuations. One result is to invalidate unrestricted universal instantiation (and existential generalization), rather as in free logic. Such systems approximate some features of ordinary usage rather nicely, e.g. the behavior of quantifiers and definite descriptions in tensed discourse. Stalnaker and Thomason's Q3r [34], based on the latter's Q3 [35], [36], is exemplary of this approach.The suggestion has repeatedly been considered to quantify over individuations in general (Kanger [14], Kaplan [17], Hughes and Cresswell [12, p. 196], Thomason [35, p. 136], Pollock [30]).

Download Full-text

Undecidability of First-Order Intuitionistic and Modal Logics with Two variables

Bulletin of Symbolic Logic ◽

10.2178/bsl/1122038996 ◽

2005 ◽

Vol 11 (3) ◽

pp. 428-438 ◽

Cited By ~ 7

Author(s):

Roman Kontchakov ◽

Agi Kurucz ◽

Michael Zakharyaschev

Keyword(s):

Modal Logic ◽

Intuitionistic Logic ◽

Modal Logics ◽

Kripke Frame ◽

Standard Nomenclature ◽

Quantified Modal Logic ◽

First Order

AbstractWe prove that the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also show that the two-variable fragment of a quantified modal logic L with expanding first-order domains is undecidable whenever there is a Kripke frame for L with a point having infinitely many successors (such are, in particular, the first-order extensions of practically all standard modal logics like K, K4, GL, S4, S5, K4.1, S4.2, GL.3, etc.). For many quantified modal logics, including those in the standard nomenclature above, even the monadic two-variable fragments turn out to be undecidable.

Download Full-text

Set-Theoretic Dependence

The Australasian Journal of Logic ◽

10.26686/ajl.v12i3.2131 ◽

2015 ◽

Vol 12 (3) ◽

Author(s):

John Wigglesworth

Keyword(s):

Modal Logic ◽

Possible Worlds ◽

Impossible Worlds ◽

Logical Framework ◽

Truth Conditions ◽

First Order ◽

Dependence Relations ◽

Asymmetric Dependence ◽

Satisfactory Account ◽

First Order Modal Logic

In this paper, we explore the idea that sets depend on, or are grounded in, their members. It is said that a set depends on each of its members, and not vice versa. Members do not depend on the sets that they belong to. We show that the intuitive modal truth conditions for dependence, given in terms of possible worlds, do not accurately capture asymmetric dependence relations between sets and their members. We extend the modal truth conditions to include impossible worlds and give a more satisfactory account of the dependence of a set on its members. Focusing on the case of singletons, we articulate a logical framework in which to evaluate set-theoretic dependence claims, using a normal first-order modal logic. We show that on this framework the dependence of a singleton on its single members follows from logic alone. However, the converse does not hold.

Download Full-text

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

10.29007/cpbz ◽

2018 ◽

Author(s):

Damien Doligez ◽

Jael Kriener ◽

Leslie Lamport ◽

Tomer Libal ◽

Stephan Merz

Keyword(s):

Modal Logic ◽

Modal Logics ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Propositional Modal Logic ◽

Theorem Provers ◽

Syntactic Abstraction

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.

Download Full-text