The consistency of syntactical treatments of knowledge1 (How to compile quantificational modal logics into classical FOL)
Jim des Rivières, Hector J. Levesque · Computational Intelligence · 1988
The relative expressive power of a sentential operator □α is compared to that of a syntactical predicateL(‘α’) in the setting of first‐order logics. Despite well‐known results by Montague and by Thomason that claim otherwise, any of the so‐called “modal” logics of knowledge and belief can be compiled into classical first‐order logics that have a corresponding predicate on sentences. Moreover, through the use of a partial truth predicate, the standard modal axiom schemata can be translated into single sentences, making it possible to use conventional first‐order logic theorem provers to directly derive results in a wide class of modal logics.