FORMALIZATION OF INTENSIONAL LOGIC
by A. Prior In his paper on this topic in Logique et analyse No. 2, J. Myhill explains why the formulae
(x) (.....x - ) (x) (.....x - ) (25) are not among the axioms of a certain system which he favours. His reasons for rejecting the formulae (25) seem to me quite conclusive. Since, however, his system [is equivalent to]contains S5 plus the classical functional calculus, the formulae (25), even if they are not laid down as axioms, are provable as theorems. I need not give the proof here, as the first part of it is in my 'Modality and quantification in S5', Journal of symbolic logic, vol. 21 (1956), and the rest
in Ruth C. Barcan's 'A functional calculus of first order based on strict implication', ibid. vol. II
This text has been edited by Fabio Corpina, Adriane Rini and Peter Øhrstrøm. The original is kept in the Prior collection at Bodleian Library, Oxford, Box 5. The words in  have been crossed out in the original.