I
I n [loll) MCKIYSEY and TAXSKI define a translation T from wffs of propositional calculus into wffs of modal logic, and prove (Thm. 5.1) that F I c n iff Fs4 T (a), where 1C is the intuitionist calculus. We wish to investigate the relation between any system PA of propositional calculus formed by adding some set A of classically valid wffs to the axioms of IC, and the corresponding system MA of modal logic which can be axiomatised by adding the set T"R t o the axioms of S 4.
First we note that by Thms. 5.2 and 3.4 of [lo], MA is normal, and hence.by Thm. 3.6 has a characteristic matrix %A = (M, { 0 } , LJ, n, -, C ) which is a closhre algebra.2) Clearly there also exists a characteristic matrix TIA = ( P , {0}, +, ., + , 1) for PA which is a Brouwerian algebra; for we can apply LINDENBAUM'S theorem as i n [73 Thms. 4 and 11, so as to obtain a matrix with just one designated element, and then use [lo] Thm. 4.1. Given any closure algebra '$It, in [9] McKIxsEY and TARSKI define (Def. 1.13) a Brouweriaii algebra m* whose elements are the closed elements of 91. It is evident that %* satisfies a wffnr iff Yl l satisfies T ( a ) . Proof. (i) Let 91 be a closure algebra which is characteristic for MA. Then SJX* satisfies every element of A , and hence is a matrix for PA. Hence if I-01, n* satisfies N , and therefore 1131 satisfies T ( a ) , whence F yA T (01) . (ii) Let h ' be a Brouwerian algebra which is characteribtic for PA. Then by [9]
Thrn. 1.15. there exists a closure algebra YI I such that 9ni * is isomorphic to n.
Yel l therefore satisfies every wff in T"A, and is thus a matrix (not necessarily characteristic) for M A . If t MAT ( ~1 ) . then T (a) is satisfied by 911, and so a is satisfied by ill?*, whence I-pAa. C o r o l l a r y
, where PC i s the classical propositional ca2culus.
T h e o r e m 1. t p , a i f f kMA T ( a ) .
Proof. PC = Plal where 01 is p v i p ; T ( a ) is then:
and it is known that S 5 = M{rca)l. 0 p v 0 1 0 1 , 1) Numerals in square brackets refer to items listed in the bibliography at the end of the article. ' *) 1.e. ( M , w, n, -, C) is a closure algebra. Tosave unnecessary verbiage, we do not here distinguish between a closure algebra ( M , w, A , -, C> and the corresponding matrix ( M , (0) , u, n, -, C>, where w represents &, A represents v ,represents i and c represents 0 . Similarly, we do not distinguish between aBrouwerian algebra ( P , + , * , 1) and the corresponding matrix ( P , { O } , +, *, +, i } , where a + b = b b -. a , i a = = l -a , 0 = i 1, and +represents & , represents V , -? represents -+ , and i represents 7.