An internal semantics for modal logic

ABSTRACT

In Kripke semantics for modal logic, “possible worlds” and the possibility relation are both primitive notions. This has both technical and conceptual shortcomings. From a technical point of view, the mathematics associated with Kripke semantics is often quite complicated. From a conceptual point of view, it is not clear how to use Kripke structures to model knowledge and belief, where one wants a clearer understanding of the notions that are primitive in Kripke semantics. We introduce modal structures as models for modal logic. We use the idea of possible worlds, but by directly describing the “internal semantics” of each possible world. It is much easier to study the standard logical questions, such as completeness, decidability, and compactness, using modal structures. Furthermore, modal structures offer a much more intuitive approach to modelling knowledge and belief.

REFERENCES

• Bat: Bates, B.: Leibniz on possible worlds. Logic, Methodology, and Philosophy of Science III (B. van Rootselaar and J.F. Staal, eds.), North-Holland, 1968, pp. 507-530.
• Bay: Bayart, A.: La correction de la logique module du premier et second ordre S5. Logique et Analyse 1(1958), pp. 2R-4t.
• Bi: Birkhoff, G.: Rings of sets. Duke Math. J. 3(1937), pp. 443-454.
• Bo: Bochmann, G.V.: Hardware specification with lemporal logic' an example. IEEE Trans. on Comput.~rs C-31(1982), pp. 223-231.
• Bu: Burgess, J.P.: Decidability for branching time. Studia Logica 39(1980), pp. 203-218.
• Ca1: Carnap, R.: Modalities and quantification. J. Symbolic Logic 11 (1946), pp. 33-64.
• Ca2: Carnap, R.: Meaning and necessity. The University of Chicago Press, 1947.
• CCF: José Mauro V. de Castilho , Marco A. Casanova , Antonio L. Furtado, A Temporal Framework for Database Specifications, Proceedings of the 8th International Conference on Very Large Data Bases, p.280-291, September 08-10, 1982
• CES: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• Ch: Chellas, B.F.: Modal logic. Cambridge Univ. Press, 1980.
• ES: E. Allen Emerson , A. Prasad Sistla, Deciding branching time logic, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.14-24, December 1984 [doi>10.1145/800057.808661]
• FHV: Fagin, R., Halpern, J.Y., Vardi, M.Y.: A model-theoretic analysis of knowledge - preliminary report. Prec. 25th IEEE Syrup on Foundations of Computer Science, 1984, pp. 268-278.
• Fi: Fine, K.: Normal forms in modal logic. Notre Dame J. Formal Lqgic 16(1975), pp. 229-237.
• FL: Fischer, M., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Computer and System Sciences 18(1979), pp. 194-211.
• Fr: van Fraa.~sen, B.: Compactness and Lowenheim-Skolem proofs in modal logic. Logique et Analyse 12(1969), pp. 167-178.
• Go: Goldblatt, R.I.: First-order definability in modal logic. J. Symbolic Logic 40(1975), pp. 35-40.
• Gu: Guillaume, M.: Rapports entre calculs propositionnels modaux el topologie impliques par certaine extensions de la methode des tableaux semantiques: Systeme de Feys-von Wright, Systeme S4 de Lewis, Systeme S5 de Lewis. Comptes Rendues des Seartces de I~tcademie de Sciences (Paris) 246(1958), pp. 1140-1142, 246(1958), pp. 2207-2210, and 247(195S), pp. 1282-1283.
• HM1: Joseph Y. Halpern , Yoram Moses, Knowledge and common knowledge in a distributed environment, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.50-61, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806735]
• HM2: Halpern, J.Y., Moses, Y.: ,4 guide to the modal logic of knowledge. To appear.
• Ha: Harsany, J.: Games of incomplete information played by Bayesian players, parts I-III. Management Science 14(1967-8), pp. 159-182, 320-334, 486-502.
• Hi1: Hintikka, J.: Quantifiers in deontic logic. S oc ie tas $ c ient ia rum i Fenn ica, Commentationes Humanarum Literarurn 23,4(1957), 1-23.
• Hi2: Hintikka, j.: Modalities and quantification. Theoria, 27(1961), 119-128.
• JT: Jonsson, B., 'rarski, A.: Boolean algebras with operators I. Arr~rican J. of Math, 23(1951), pp. 891-939.
• Ka: Kanger, S.: Provability in Logic. Stockholm Studies in Philosophy I, 1957.
• KP: Kozen, D., Parikh, R.: An elementary proof of the completeness of PDL. Theoretical Computer Science, 14(1981), pp. 113-118.
• Kr1: Kripke, S.A.: A completeness theorem in modal logic. J. $.mtbolic Logic 24(1959), pp. 1-14.
• Kr2: Kripke, S.A.: Semantical analysis of modal logic I- normal modal propositional calculi, Zeit. ~. math. Logik und Grundlagen d. Math. 9(1963), pp. 67-96. (Announced in J. Sy?nbolic Logic 24(1959), p. 323.)
• La: Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6(1977), pp. 467-480.
• Leh: Daniel Lehmann, Knowledge, common knowledge and related puzzles (Extended Summary), Proceedings of the third annual ACM symposium on Principles of distributed computing, p.62-67, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806736]
• Lem1: Lemmon, E.J.: Algebraic semantics for modal logics, parts I-II. J. Symbolic Logic 31(1966), pp. 45-65 and pp. 191-218.
• Lem2: Lemmon, E.J.: An introduction to modal logic (the "Lemmon Notes"), in collaboration with D. Scott and edited by K. Segerberg. American Phil Quarterly Mono. graph ,Series #1 l, 1977.
• Len: Lenzen, W.: Recent work in epistemic logic. Acta. Phil Fennica 30(1978), pp. 1-218.
• Lev: Levesque, Hector J,: A formal treatment of incomplete knowledge bases, Fairchild Technical Report No. 614, FLAIR Technical Report No. 3, Feb. 1982.
• Li: Witold Lipski, Jr., On Databases with Incomplete Information, Journal of the ACM (JACM), v.28 n.1, p.41-70, Jan. 1981 [doi>10.1145/322234.322239]
• Ma: Makinson, D.: On some completeness theorems in modal logic. Zeit. f. math. Logik und Grundlagen d. Math. 12(1966), pp. 379-384.
• MW: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• MH: McCarthy, J., Hayes, P.: Some philo-. sophical problems from the standpoint of artificial intelligence. In Machine intelligence 4 (D. Michie, ed.}, American Elsevier, 1969, pp. 463-502.
• MSHI: John McCarthy , Masahiko Sato , Takeshi Hayashi , Shigeru Igarashi, On the model theory of knowledge, Stanford University, Stanford, CA, 1978
• Mc: McKinsey, J, C. C.: A solution of the decision problem for the Lewis Systems S2 and $4, with an application to topology. J. S),nbolic Logic 6(1941), pp. 117-134.
• McT: McKinsey, J. C. C., Tarski, A.: Some theorems about the sentential calculi of Lewis and Heyting. J. S.m,bolic Logic 13(1948), pp. 83-96.
• Me: Meredith, C.A.: interpretations of different modal logics in the "Property Calculus". Mimeographed manuscript, Philosophy Department, Canterbury University College (recorded and expanded by A.N, Prior), 1956.
• Mo1: Montague, R.: Logical necessity, physical necessity, ethics, and quantifiers. Inquiry 4(1960), pp. 259-269. (Originally delivered before the Ann. Spring Conf. in Phil. at the Univ. of California, Los Angeles, 1955).
• Mo2: Montague, R.: Pragmatics. In Contemporary Philosophy (R. Kalibansky, ed.), La Nuova Italia Editrice, Florence, 1968, pp. 102-121.
• Pn: Pnueli, A.: The temporal logic of programs. Prec. 18th IEEE S. wnp. on Foundation of Computer Science, 1977, pp. 46-57.
• Pra1: Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. Prec. 17th IEEE Syrnp. on Foundations of Computer Science, Houston, 1976, pp. 109-121.
• Pra2: Pratt, V.R.: A near optimal method for reasoning about action. J. Computer and System Sciences 20(1980), pp. 231-254.
• Pri: Prior, A.N.: Possible worlds (idea attributeri to P.T. Geach). Phil Quarterly 12(1962), pp. 36-43.
• Rab: Rabin, M.O.: Decidability of secondorder theories and automata on infinite trees. Tram. AMS 141(1969), pp. 1-35.
• Rad: Radner, R.: Competitive equilibrium under uncerlainly. Econometrica 361,1958), pp. 21-58.
• Re: Rescher, N.: On alternatives in epistemic logic. In Studies in Modality, American Phil. Quarterly Monograph Series #8(1974), pp. 99-114.
• RS: John H. Reif , A. Prasad Sistla, A Multiprocess Network Logic with Temporal and Spatial Modalities, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.629-639, July 18-22, 1983
• Sc: Scott, D.: Advice on modal logic. In Philosophical problems in logic (K. Lambert, ed.), Reidel, 1970, pp. 143-173.
• SM: Schwartz, R.L., Melliar-Smith, P.M.' Temporal specification 'of distributed systems. Prec. 2nd Int. Conf. on Distributed Systems, Paris, 1981, pp. 1-9.
• Sta: Stalnaker, R.: A note on non-monotonic logic. Dept. of Philosophy, Cornell University, unpublished manuscript, 1980.
• Str: Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control 54(1982), pp. 121-141.
• Ts: Tsao-Chen, T.: Algebraic postulates and a geometric interpretation for the Lewis calculus of strict implication. Bulletin American Math. Soc. (Series 2) 44(1938), pp. 737-744.
• TW: Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of secondorder logic. Math. System Theory 2(1968), pp. 57-81.
• VW: Moshe Y. Vardi , Pierre Wolper, Automata theoretic techniques for modal logics of programs: (Extended abstract), Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.446-456, December 1984 [doi>10.1145/800057.808711]

INDEX TERMS

Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Languages, Theory, Verification