An ontology-based first-order intensional logic

There exist many difficulties in the current semantics for first-order modal logic. For instance, the problem of rigid semantics. In order to solve the problem of rigid semantics, Melvin Fitting presented a semantics of first-order intensional logic (FOIL), in which both objects and intensions are explicitly present and can be quantified over. Intensions designate different objects under different circumstances - they are non-rigid designators. But in first-order intensional logic, there lacks a formal mechanism to determine the set of intensions. In this paper, we proposed an ontology-based first-order intensional logic, in which ontologies are introduced to restrain the modal logic frames and models. An ontology-based counterpart relation S is introduced into each model. By requiring that the designations of each intension in different possible worlds must accord with the relation S, we can correctly determine the set of intensions. In addition, our semantics can also solve the problem of rigid semantics.