Modal logic is an extension of traditional propositional logic. It adds more operators, such as "it is possible that," "it is necessary that," "it will always be the case that," "an agent believes that," etc. 

Evolution

In the last fifty years, modal logic has become very useful in many areas of computer science, such as artificial intelligence, database theory, distributed systems, programme verification, and security theory.

The father of modal logic is German mathematician and philosopher Gottfried Leibniz, who created calculus and mechanics. There are two kinds of truth, in his opinion. If a statement is true in any state of affairs, it is said to be necessarily true. Take note that one may have factual assertions. That is, such claims could be incorrect, all else being equal. 

Hugh MacColl made new advances to modal logic in the 1800s but needed more attention. Modern modal logic was started by C. I. Lewis in a set of academic articles, starting with "Implication and the Algebra of Logic" in 1912. Lewis came up with modal logic and strict implication because classical logic allows paradoxes of material implication, like the idea that a falsehood implies any claim. This work ended with the publication of his book Symbolic Logic in 1932. This book presented the five systems S1 through S5.

Likewise 1959, Saul Kripke proposed the standard Kripke semantics for modal logic. It was the start of the modern era in modal semantics. This type of semantics is often called "possible worlds" semantics. Kripke and A. N. Prior had written to each other for a long time before. Kripke semantics is easy, but E. W. Beth says that semantic-tableaux or analytic tableaux make it easier to prove things.

Operators

Modal logic operators include conjunction and negation, which are propositional logic operators, as well as operators that can mean "it is necessary that," "after a programme has ended," "an agent knows or believes that," "it is always the case that," and so on. Problems in modal logic, like satisfiability, have been looked at by computer scientists. Satisfiability is a way to tell if a statement in a certain logic can be satisfied. In modal logic, there is a wide range of how hard it is to satisfy something. Depending on how limited modal logic is, its complexity can range from being NP-complete to being very hard to decide.

Epistemic logic

Epistemic logic is helpful when discussing the knowledge of individuals in a community since it provides justifications for knowledge and belief. Distributed systems and the notion of artificial intelligence both benefit from epistemic logic. Reasoning about zero-knowledge proofs, a branch of cryptography theory, uses specific types of epistemic logic.

Adaptability

The fact that modal operators can mean different things makes modal logic easy to use in many areas of computer science. The "necessary" operator, the basic modal operator, and its opposite, the "possibility" operator, can mean different things based on the context. For example, the "necessary" operator can mean "after all possible computations of a programme have ended," "agent I know that," "it is always true that," "it should be true that," and so on. 

Furthermore, the semantics of modal logic is based on the semantics of possible worlds. Possible-worlds semantics looks at the different worlds or states that could be true after something changes in one world. For example, there are many possible ways that tomorrow could turn out, but only one of those ways comes true. There are rules that modal operators must follow. Computer scientists have examined satisfiability and validity in different kinds of modal logic.

Image source: Unsplash