Modal Logic - Development of Modal Logic

Development of Modal Logic

Although Aristotle's logic is in large parts concerned with the theory of non-modalized categorical syllogisms, he also developed a modal syllogistic. Moreover, there are passages in his work, such as the famous sea-battle argument in De Interpretatione § 9, that are now seen as anticipations of modal logic and its connection with potentiality and time. So are the modal systems developed by Diodorus Cronus, Philo of Megara and the Stoic Chrysippus, which each contained precursors of modal axioms T and D as well as inter-defined notions of necessity and possibility. Modal logic as a self-aware subject owes much to the writings of the Scholastics, in particular William of Ockham and John Duns Scotus, who reasoned informally in a modal manner, mainly to analyze statements about essence and accident.

C. I. Lewis founded modern modal logic in his 1910 Harvard thesis and in a series of scholarly articles beginning in 1912. This work culminated in his 1932 book Symbolic Logic (with C. H. Langford), which introduced the five systems S1 through S5.

Ruth C. Barcan (later Ruth Barcan Marcus) developed the first axiomatic systems of quantified modal logic — first and second order extensions of Lewis's "S2", "S4", and "S5".

The contemporary era in modal semantics began in 1959, when Saul Kripke (then only a 19-year-old Harvard University undergraduate) introduced the now-standard Kripke semantics for modal logics. These are commonly referred to as "possible worlds" semantics. Kripke and A. N. Prior had previously corresponded at some length. Kripke semantics is basically simple, but proofs are eased using semantic-tableaux or analytic tableaux, as explained by E. W. Beth.

A. N. Prior created modern temporal logic, closely related to modal logic, in 1957 by adding modal operators and meaning "eventually" and "previously". Vaughan Pratt introduced dynamic logic in 1976. In 1977, Amir Pnueli proposed using temporal logic to formalise the behaviour of continually operating concurrent programs. Flavors of temporal logic include propositional dynamic logic (PDL), propositional linear temporal logic (PLTL), linear temporal logic (LTL), computational tree logic (CTL), Hennessy–Milner logic, and T.

The mathematical structure of modal logic, namely Boolean algebras augmented with unary operations (often called modal algebras), began to emerge with J. C. C. McKinsey's 1941 proof that S2 and S4 are decidable, and reached full flower in the work of Alfred Tarski and his student Bjarni Jonsson (Jonsson and Tarski 1951–52). This work revealed that S4 and S5 are models of interior algebra, a proper extension of Boolean algebra originally designed to capture the properties of the interior and closure operators of topology. Texts on modal logic typically do little more than mention its connections with the study of Boolean algebras and topology. For a thorough survey of the history of formal modal logic and of the associated mathematics, see Robert Goldblatt (2006).