On the syntactical construction of systems of modal logic

1945 ◽  
Vol 10 (3) ◽  
pp. 83-94 ◽  
Author(s):  
J. C. C. Mckinsey

When C. I. Lewis developed his theory of strict implication, he left open the question which of his various systems should be regarded as being closest to our intuitions—though he was inclined to favor the system S2. There are to be found in the literature numerous discussions of this question; most of these have condemned S2 as being too strong, and have proposed ways of weakening it.In the present paper I shall attempt to throw some light on this question by setting up a syntactical definition of “possibility.” I shall show that every system of modal logic constructed on the basis of this definition is at least as strong as the Lewis system S4.As the intuitive basis for the syntactical definition of possibility, I take the position that to say a sentence is possible means that there exists a true sentence of the same form. Thus, for example, it would be said that the sentence, “Lions are indigenous to Alaska,” is possible, because of the fact that the sentence, “Lions are indigenous to Africa,” has the same form and is true.

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.


1934 ◽  
Vol 43 (5) ◽  
pp. 518 ◽  
Author(s):  
J. C. Chenoweth McKinsey

1951 ◽  
Vol 16 (2) ◽  
pp. 112-120 ◽  
Author(s):  
Schiller Joe Scroggs

Dugundji has proved that none of the Lewis systems of modal logic, S1 through S5, has a finite characteristic matrix. The question arises whether there exist proper extensions of S5 which have no finite characteristic matrix. By an extension of a sentential calculus S, we usually refer to any system S′ such that every formula provable in S is provable in S′. An extension S′ of S is called proper if it is not identical with S. The answer to the question is trivially affirmative in case we make no additional restrictions on the class of extensions. Thus the extension of S5 obtained by adding to the provable formulas the additional formula p has no finite characteristic matrix (indeed, it has no characteristic matrix at all), but this extension is not closed under substitution—the formula q is not provable in it. McKinsey and Tarski have defined normal extensions of S4* by imposing three conditions. Normal extensions must be closed under substitution, must preserve the rule of detachment under material implication, and must also preserve the rule that if α is provable then ~◊~α is provable. McKinsey and Tarski also gave an example of an extension of S4 which satisfies the first two of these conditions but not the third. One of the results of this paper is that every extension of S5 which satisfies the first two of these conditions also satisfies the third, and hence the above definition of normal extension is redundant for S5. We shall therefore limit the extensions discussed in this paper to those which are closed under substitution and which preserve the rule of detachment under material implication. These extensions we shall call quasi-normal. The class of quasi-normal extensions of S5 is a very broad class and actually includes all extensions which are likely to prove interesting. It is easily shown that quasi-normal extensions of S5 preserve the rules of replacement, adjunction, and detachment under strict implication. It is the purpose of this paper to prove that every proper quasi-normal extension of S5 has a finite characteristic matrix and that every quasi-normal extension of S5 is a normal extension of S5 and to describe a simple class of characteristic matrices for S5.


1963 ◽  
Vol 28 (2) ◽  
pp. 135-142 ◽  
Author(s):  
Frederic B. Fitch

The purpose of this paper is to provide a partial logical analysis of a few concepts that may be classified as value concepts or as concepts that are closely related to value concepts. Among the concepts that will be considered are striving for, doing, believing, knowing, desiring, ability to do, obligation to do, and value for. Familiarity will be assumed with the concepts of logical necessity, logical possibility, and strict implication as formalized in standard systems of modal logic (such as S4), and with the concepts of obligation and permission as formalized in systems of deontic logic. It will also be assumed that quantifiers over propositions have been included in extensions of these systems.


Author(s):  
Jinsheng Chen ◽  
Hans Van Ditmarsch ◽  
Giuseppe Greco ◽  
Apostolos Tzimoulis

We introduce a class of neighbourhood frames for graded modal logic using an operation from Kripke frames to neighbourhood frames. This class of neighbourhood frames is shown to be first-order definable but not modally definable. We also obtain a new definition of graded bisimulation by modifying the definition of monotonic bisimulation.  


Author(s):  
Anil Gupta

Alfred Tarski’s definition of truth is unlike any that philosophers have given in their long struggle to understand the concept of truth. Tarski’s definition is more clear and precise than any previous definition, but it is also unusual in character and more restricted in scope. Tarski does not provide a general definition of truth. He provides instead a method of constructing, for a range of formalized languages L, definitions of the notions ‘true sentence of L’. A remarkable feature of Tarski’s work on truth is his ‘Criterion T’, which lays down a general condition that any definition of ‘true sentence of L’ must satisfy. Tarski’s ideas have exercised an enormous influence in philosophy. They have played an important role in the formulation and defence of a range of views in logic, semantics and metaphysics.


2008 ◽  
Vol 18 (1) ◽  
pp. 29-55 ◽  
Author(s):  
MARCO BERNARDO ◽  
STEFANIA BOTTA

Behavioural equivalences are a means of establishing whether computing systems possess the same properties. The specific set of properties that are preserved by a specific behavioural equivalence clearly depends on how the system behaviour is observed and can usually be characterised by means of a modal logic. In this paper we consider three different approaches to the definition of behavioural equivalences – bisimulation, testing and trace – applied to three different classes of systems – non-deterministic, probabilistic and Markovian – and we survey the nine resulting modal logic characterisations, each of which stems from the Hennessy–Milner logic. We then compare the nine characterisations with respect to the logical operators, in order to emphasise the differences between the three approaches in the definition of behavioural equivalences and the regularities within each of them. In the probabilistic and Markovian cases we also address the issue of whether the probabilistic and temporal aspects should be treated in a local or global way and consequently whether the modal logic interpretation should be qualitative or quantitative.


2008 ◽  
Vol 1 (3) ◽  
pp. 267-304 ◽  
Author(s):  
DOV GABBAY ◽  
ODINALDO RODRIGUES ◽  
ALESSANDRA RUSSO

In this article, we propose a belief revision approach for families of (non-classical) logics whose semantics are first-order axiomatisable. Given any such (non-classical) logic $L$, the approach enables the definition of belief revision operators for $L$, in terms of a belief revision operation satisfying the postulates for revision theory proposed by Alchourrón, Gärdenfors and Makinson (AGM revision, Alchourrón et al. (1985)). The approach is illustrated by considering the modal logic K, Belnap's four-valued logic, and Łukasiewicz's many-valued logic. In addition, we present a general methodology to translate algebraic logics into classical logic. For the examples provided, we analyse in what circumstances the properties of the AGM revision are preserved and discuss the advantages of the approach from both theoretical and practical viewpoints.


1953 ◽  
Vol 18 (3) ◽  
pp. 234-236 ◽  
Author(s):  
Ruth Barcan Marcus

Lewis and Langford state, “… it appears that the relation of strict implication expresses precisely that relation which holds when valid deduction is possible. It fails to hold when valid deduction is not possible. In that sense, the system of strict implication may be said to provide that canon and critique of deductive inference which is the desideratum of logical investigation.” Neglecting for the present other possible criticisms of this assertion, it is plausible to maintain that if strict implication is intended to systematize the familiar concept of deducibility or entailment, then some form of the deduction theorem should hold for it. The purpose of this paper is to analyze and extend some results previously established which bear on the problem.We will begin with a rough statement of some relevent considerations. Let the system S contain among its connectives an implication connective ‘I’ and a conjunction connective ‘&’. Let A1, A2, …, An ⊦ B abbreviate that B is provable on the hypotheses A1, A2, …, An for a suitable definition of “proof on hypotheses”, where A1, A2, …, An, B are well-formed expressions of S.


2018 ◽  
Vol 47 (3) ◽  
Author(s):  
María Manzano ◽  
Manuel Crescencio Moreno

This article is a continuation of our promenade along the winding roads of identity, equality, nameability and completeness. We continue looking for a place where all these concepts converge. We assume that identity is a binary relation between objects while equality is a symbolic relation between terms. Identity plays a central role in logic and we have looked at it from two different points of view. In one case, identity is a notion which has to be defined and, in the other case, identity is a notion used to define other logical concepts. In our previous paper, [16], we investigated whether identity can be introduced by definition arriving to the conclusion that only in full higher-order logic with standard semantics a reliable definition of identity is possible. In the present study we have moved to modal logic and realized that here we can distinguish in the formal language between two different equality symbols, the first one shall be interpreted as extensional genuine identity and only applies for objects, the second one applies for non rigid terms and has the characteristic of synonymy. We have also analyzed the hybrid modal logic where we can introduce rigid terms by definition and can express that two worlds are identical by using the nominals and the @ operator. We finish our paper in the kingdom of identity where the only primitives are lambda and equality. Here we show how other logical concepts can be defined in terms of the identity relation. We have found at the end of our walk a possible point of convergence in the logic Equational Hybrid Propositional Type Theory (EHPTT), [14] and [15].


Sign in / Sign up

Export Citation Format

Share Document