(Rtl ... tn]cp) (Rtl'" tn --+ cp) --+ [Rtl . . tn]cp axiom (9) PL+ def [ 1r] 1, 2, MP. The effects of the oracle rule of [4], stating that all PL theorems are axioms, are taken care of in the present setup by the p ropositio nal and quant ificationa l axioms.

J. 6 It is van instructive to see how the Hoare style rules for DPL as derived rules of i n ference in the present calculus. The test axioms from [4] are the two sides of the of Van Eijck and De Vries bi- implication [4] given by the test axiom (9). Here is the derivation of the existential test axiom. l. 2. 3. Here 1. 2. 3. ( Rtl ... tn)cp ..... ( Rtl . tn /\ cp). (Rtl . , . tn)cp <-+ (Rtl ... tn /\ cp)) --+ ((Rtl . tn 1\ cp) --+ (Rtl ... tn)cp) (Rtl ... tn /\ cp) --+ (Rtl ... tn)cp. is the derivation of the axiom (9) PL 1,2,MP.

Lambek Calculus and Boolean Connectives: On the Road, Onderzoeksinstituut [16] voor Taal en Spraak, Rijksuniversiteit, Utrecht. [17] A. Simon, 1992. 'Arrow Logic Lacks the Deduction Theorem', Mathematical Institute of the Hun garian Academy of Sciences, Budapest. 'A Modal Theory of Arrows 1', Report ML-92-04, I n st i t ute for Logic , L an guage [18) D. Vakarelov, 1992. [19] Y. Venema, 1992. Many-Dimensional Modal Logic, Di ssertat ion , Institute for Logic , Language and and Com put at i on , University of Amsterdam.