Modal Logic Should Say More Than It Does.
Melvin Fitting · 1991
First-order modal logics, as traditionally formulated, are not expressive enough. It is this that is behind the di#culties in formulating a good analog of Herbrand's Theorem, as well as the well-known problems with equality, non-rigid designators, definite descriptions, and nondesignating terms. We show how all these problems disappear when modal language is made more expressive in a simple, natural way. We present a semantic tableaux system for the enhanced logic, and (very) briefly discuss implementation issues. 1 Introduction Necessity is the mother of modality, but she has a large family. It includes knows, believes, legally requires and morally requires, among others. Clearly a proper understanding of the behavior of modal operators is essential to any formal treatment of natural language, as well as to any formalization of everyday reasoning. Unfortunately, once the elementary level has been passed, virtually every feature that has made classical logic a powerful tool has ...