Multimodal logic

Last updated

A multimodal logic is a modal logic that has more than one primitive modal operator. They find substantial applications in theoretical computer science.

Contents

Overview

A modal logic with n primitive unary modal operators is called an n-modal logic. Given these operators and negation, one can always add modal operators defined as if and only if .

Perhaps the first substantive example of a two-modal logic is Arthur Prior's tense logic, with two modalities, F and P, corresponding to "sometime in the future" and "sometime in the past". A logic [1] with infinitely many modalities is dynamic logic, introduced by Vaughan Pratt in 1976 and having a separate modal operator for every regular expression. A version of temporal logic introduced in 1977 and intended for program verification has two modalities, corresponding to dynamic logic's [A] and [A*] modalities for a single program A, understood as the whole universe taking one step forwards in time. The term multimodal logic itself was not introduced until 1980. Another example of a multimodal logic is the Hennessy–Milner logic, itself a fragment of the more expressive modal μ-calculus, which is also a fixed-point logic.

Multimodal logic can be used also to formalize a kind of knowledge representation: the motivation of epistemic logic is allowing several agents (they are regarded as subjects capable of forming beliefs, knowledge); and managing the belief or knowledge of each agent, so that epistemic assertions can be formed about them. The modal operator must be capable of bookkeeping the cognition of each agent, thus must be indexed on the set of the agents. The motivation is that should assert "The subject i has knowledge about being true". But it can be used also for formalizing "the subject i believes ". For formalization of meaning based on the possible world semantics approach, a multimodal generalization of Kripke semantics can be used: instead of a single "common" accessibility relation, there is a series of them indexed on the set of agents. [2]

Notes

  1. Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 – September 4, 2009, Tutorial Lectures. Springer. p. 112. ISBN   978-3-642-03753-5.
  2. Ferenczi 2002, p. 257.

Related Research Articles

<span class="mw-page-title-main">Saul Kripke</span> American philosopher and logician (1940–2022)

Saul Aaron Kripke was an American analytic philosopher and logician. He was Distinguished Professor of Philosophy at the Graduate Center of the City University of New York and emeritus professor at Princeton University. Kripke is considered one of the most important philosophers of the latter half of the 20th century. Since the 1960s, he has been a central figure in a number of fields related to mathematical and modal logic, philosophy of language and mathematics, metaphysics, epistemology, and recursion theory.

Understood in a narrow sense, philosophical logic is the area of logic that studies the application of logical methods to philosophical problems, often in the form of extended logical systems like modal logic. Some theorists conceive philosophical logic in a wider sense as the study of the scope and nature of logic in general. In this sense, philosophical logic can be seen as identical to the philosophy of logic, which includes additional topics like how to define logic or a discussion of the fundamental concepts of logic. The current article treats philosophical logic in the narrow sense, in which it forms one field of inquiry within the philosophy of logic.

In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a modal logic-based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians.

Modal logic is a kind of logic used to represent statements about necessity and possibility. It plays a major role in philosophy and related fields as a tool for understanding concepts such as knowledge, obligation, and causation. For instance, in epistemic modal logic, the formula can be used to represent the statement that is known. In deontic modal logic, that same formula can represent that is a moral obligation.

In logic, a normal modal logic is a set L of modal formulas such that L contains:

Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Joyal. It was first conceived for modal logics, and later adapted to intuitionistic logic and other non-classical systems. The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the model theory of such logics was almost non-existent before Kripke.

<span class="mw-page-title-main">Method of analytic tableaux</span>

In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.

Deontic logic is the field of philosophical logic that is concerned with obligation, permission, and related concepts. Alternatively, a deontic logic is a formal system that attempts to capture the essential logical features of these concepts. It can be used to formalize imperative logic, or directive modality in natural languages. Typically, a deontic logic uses OA to mean it is obligatory that A, and PA to mean it is permitted that A, which is defined as .

Common knowledge is a special kind of knowledge for a group of agents. There is common knowledge of p in a group of agents G when all the agents in G know p, they all know that they know p, they all know that they all know that they know p, and so on ad infinitum. It can be denoted as .

Intensional logic is an approach to predicate logic that extends first-order logic, which has quantifiers that range over the individuals of a universe (extensions), by additional quantifiers that range over terms that may have such individuals as their value (intensions). The distinction between intensional and extensional entities is parallel to the distinction between sense and reference.

The autoepistemic logic is a formal logic for the representation and reasoning of knowledge about knowledge. While propositional logic can only express facts, autoepistemic logic can express knowledge and lack of knowledge about facts.

In philosophical logic, the concept of an impossible world is used to model certain phenomena that cannot be adequately handled using ordinary possible worlds. An impossible world, , is the same sort of thing as a possible world , except that it is in some sense "impossible." Depending on the context, this may mean that some contradictions, statements of the form are true at , or that the normal laws of logic, metaphysics, and mathematics, fail to hold at , or both. Impossible worlds are controversial objects in philosophy, logic, and semantics. They have been around since the advent of possible world semantics for modal logic, as well as world based semantics for non-classical logics, but have yet to find the ubiquitous acceptance, that their possible counterparts have found in all walks of philosophy.

Epistemic modal logic is a subfield of modal logic that is concerned with reasoning about knowledge. While epistemology has a long philosophical tradition dating back to Ancient Greece, epistemic logic is a much more recent development with applications in many fields, including philosophy, theoretical computer science, artificial intelligence, economics and linguistics. While philosophers since Aristotle have discussed modal logic, and Medieval philosophers such as Avicenna, Ockham, and Duns Scotus developed many of their observations, it was C. I. Lewis who created the first symbolic and systematic approach to the topic, in 1912. It continued to mature as a field, reaching its modern form in 1963 with the work of Kripke.

A modal connective is a logical connective for modal logic. It is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non-truth-functional in the following sense: The truth-value of composite formulae sometimes depend on factors other than the actual truth-value of their components. In the case of alethic modal logic, a modal operator can be said to be truth-functional in another sense, namely, that of being sensitive only to the distribution of truth-values across possible worlds, actual or not. Finally, a modal operator is "intuitively" characterized by expressing a modal attitude about the proposition to which the operator is applied.

In mathematics and philosophy, Łukasiewicz logic is a non-classical, many-valued logic. It was originally defined in the early 20th century by Jan Łukasiewicz as a three-valued modal logic; it was later generalized to n-valued as well as infinitely-many-valued (0-valued) variants, both propositional and first order. The ℵ0-valued version was published in 1930 by Łukasiewicz and Alfred Tarski; consequently it is sometimes called the Łukasiewicz–Tarski logic. It belongs to the classes of t-norm fuzzy logics and substructural logics.

In logic and philosophy, S5 is one of five systems of modal logic proposed by Clarence Irving Lewis and Cooper Harold Langford in their 1932 book Symbolic Logic. It is a normal modal logic, and one of the oldest systems of modal logic of any kind. It is formed with propositional calculus formulas and tautologies, and inference apparatus with substitution and modus ponens, but extending the syntax with the modal operator necessarily and its dual possibly.

In modal logic, a classical modal logicL is any modal logic containing the duality of the modal operators

In mathematical logic, predicate functor logic (PFL) is one of several ways to express first-order logic by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic devices called predicate functors that operate on terms to yield terms. PFL is mostly the invention of the logician and philosopher Willard Quine.

In modal logic, standard translation is a logic translation that transforms formulas of modal logic into formulas of first-order logic which capture the meaning of the modal formulas. Standard translation is defined inductively on the structure of the formula. In short, atomic formulas are mapped onto unary predicates and the objects in the first-order language are the accessible worlds. The logical connectives from propositional logic remain untouched and the modal operators are transformed into first-order formulas according to their semantics.

Dynamic epistemic logic (DEL) is a logical framework dealing with knowledge and information change. Typically, DEL focuses on situations involving multiple agents and studies how their knowledge changes when events occur. These events can change factual properties of the actual world : for example a red card is painted in blue. They can also bring about changes of knowledge without changing factual properties of the world : for example a card is revealed publicly to be red. Originally, DEL focused on epistemic events. We only present in this entry some of the basic ideas of the original DEL framework; more details about DEL in general can be found in the references.

References