A modal extension of intuitionist logic.
Robert A. Bull · Notre Dame Journal of Formal Logic · 1965
R. A. BULL 1.In [3] (pp. 38, 39) Prior gives a modal extension of IC by adding to it the rules R1.caβ==>CLaβ R2.Caβ =$>CaMβ R3.Caβ=$>CaLβ, if a is fully modalised, 1 R4.Ca β =$> CMa β, if β is fully modalised.This system, which he calls MIPQ, is analogous to S5, in the sense that adding ANpp to it yields S5, and is intuitionistically plausible, in the sense that collapsing the modal operators yields IC.The purpose of this paper is to give a characterization of the normal models for MIPQ (in section 2) and show that it has the finite model property (in section 3).From this last result it follows immediately that MIPQ is decidable, since its normal models are strong models for the rules.Before I proceed with this work I wish to refer briefly to a related system.The question as to whether MIPQ-or any other modal extension of IC-formalises concepts which an intuitionist philosopher would regard as modal is quite distinct from the formal ones answered in this paper.As Prior points out, one could regard the propositions of MIPQ as predicates in one individual variable, x say, and regard L and M as Tlx and Σx.Perhaps this would give a suitable intuitionist interpretation of modality, but I prefer a rather stronger system in which La and Ma can be interpreted as 'a is the case in all possible worlds' and 'a is the case in some possible world'.This system has for its models those obtained by taking any model for IC, 4H say, and any n ^ 1 and (1) Taking as truth-values sequences of n elements of ϋ.(2) Designating , where 1 is the designated element of ϋ.(3) Determining non-modal operators by applying the operators of H to corresponding terms of sequences.1. Ie if every occurrence of a variable in a is an occurrence in the argument of a modal operator.