Possibility in Intuitionistic Higher-Order Logic

In classical modal logic possibility is definable in terms of necessity: to be possible is to be not necessarily false. However, this identification is intuitionistically dubious. This paper uses an intensionalist higher-order logic to analyse necessity and possibility from an intuitionistic point of view. Surprisingly, this higher-order point of view indicates that the orthodox principles of intuitionistic possibility, influentially articulated by Fischer Servi, are unjustified. In addition to forcing a reevaluation of the intuitionistic principles of modal logic, the results reveal an interesting landscape for intuitionistic modal metaphysics that can only be seen from a higher-order perspective.