(Rtl ... tn]cp) (Rtl'" tn --+ cp) --+ [Rtl . . tn]cp axiom (9) PL+ def [ 1r] 1, 2, MP. The effects of the oracle rule of , 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  are the two sides of the of Van Eijck and De Vries bi- implication  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  voor Taal en Spraak, Rijksuniversiteit, Utrecht.  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.  Y. Venema, 1992. Many-Dimensional Modal Logic, Di ssertat ion , Institute for Logic , Language and and Com put at i on , University of Amsterdam.