ABSTRACT
Here ( i l ) is just a reformulation of (iO) in view of the equivalence (A) for RPC-lattices. Replacing y in (iO) by i y , I obtain ( i2 ); hence the axioms (m4) and (iO) imply the axiom system (B) for cm from Lemma 4 . The axiom ( i 2 ) is a particular instance of ( i0); however, together with (m3) this instance is equivalent to (iO) over the axioms of eg since
x ,“ix I »“iy by (m3) ",_,y b “>y-*y by ( i 2 ) x ,-ix b ->y->y by (CR) x ,“ix I-ty by (m3) x ,“ix b y by (M P)
from where the deduction principle leads to (iO). - It follows from these proofs that also the pure modus ponens calculi defined by these new axiom system s will be separated for each subset of A , V , n . Again, it follows from T /V . = that, for any formula v, the deducibility of b v for ci is equivalent to Pj(v) = e in Fj. Thus each of the various axiom system s for ci gives, sim ultaneously, a system of defining equations for the class A r
Let T be a term algebra containing the positive connectives and -i . Let cc be the pure modus ponens calculus defined by a set of axioms for the intui tionistic calculus ci together with the axiom
Defining V c by the same conditions as V d, and replacing cd, A d, T d, V d, R ci, d -fram e, K P d in Theorem l d by cc, A c , T , V c , R c , c-fram e, L K , there holds w ithout changes to its proof
THEOREM l c [verbally as Theorem l d] .
