zbMATH — the first resource for mathematics

The functional interpretation of modal necessity. (English) Zbl 0911.03012
Rijke, Maarten de (ed.), Advances in intensional logic. Dordrecht: Kluwer Academic Publishers. Appl. Log. Ser. 7, 61-91 (1997).
Since the early days of Kripke-style possible-worlds semantics for modalities, there has been a significant amount of research into the development of mechanisms for handling and characterizing modal logics by means of ‘naming’ possible worlds, either directly by introducing identifiers, or indirectly by some other means (such as, e.g., using formulas to identify the possible world). In first-order predicate logics the individuals over which one quantifies are naturally assumed to have names. The main connectives of modal logics are such that they quantify over (higher-order) objects which are not usually given names, in some cases for methodological reasons.
The Curry-Howard functional interpretation of logics appears to be particularly suitable to deal with ‘arbitrary’ objects within a mathematical theory of deduction. Once names for arbitrary objects are introduced, the mechanism of abstraction, which goes back at least to Frege’s Grundgesetze mechanism of binding free-variables via so-called ‘value-range’ function-terms, serves to ‘discharge’ assumptions such as that the particular name denoted an arbitrary object.
The present paper reports on the conceptual apparatus as a preparation for the framework of labelled natural deduction for modal necessity. It is part of ongoing research, and the results about various metamathematical properties of the logical system will be left to a further publication.
For the entire collection see [Zbl 0885.00029].

03B45 Modal logic (including the logic of norms)