Individual concepts as propositional variables in \(ML^{\nu +1}\) (Q760420)

The author studies the many-sorted quantified modal systems defined previously by \textit{A. Bressan} [A general interpreted modal calculus (1972; Zbl 0255.02015); Aspects of philosophical logic, Synth. Libr. 147, 21-66 (1981; Zbl 0476.03028)]. \(ML^{\nu}\) (\(\nu\) : a positive integer) is a typed language, \(MC^{\nu}\) is a calculus (an extension of S5) based on that language. \(ML_*^{\nu}\) and \(MC_*^{\nu}\) differ from them by the addition of propositional constants and variables and of relations and functions having propositional arguments (they were designed to deal with probability theories along the lines of Reichenbach's work). \(MC^{\nu}\) had previously been proved complete for a semantics which is a natural extension of Kripke semantics, with a convention for transworld identification of individuals in each ''type'' \(\nu\). Here \(MC_*^{\nu}\) is proved complete by means of an embedding of \(ML_*^{\nu}\) into \(ML^{\nu +1}\) with type \(\nu +1\) containing only two individuals.