C'OSTISUISG V--lRIATIONS ON X SYSTEM OF GENTZEN hy ZVOSIMIR ha16 in Zagreb (Yugoslavia) GEXTZES has shown in [lJ that,, in his sequent version of predicate logic, the dist.inction between IPC and CPC is forinally represented as distinction betweeii singular and multiple version of his system. KLEENE has shown in [a] that singularity of the riiles (-1) and (+T) will suffice for IPC. L~PEZ-ESCOBAR has shown in [3.1 that thc, singularity of ( + i ) alone, or (+T) alone will not suffice for IPC, because putting any of them in multiple form yields CPC. He has also shown (in [3] again) that any combination of singular and mult'iple rules will yield IPC, CD or CPC.
The method of KLEENE and L~PEZ-ESCOBAR is to start from multiple version of Q 1 (that is from CPC) and t o find t,lie restricted versions (rest,ricted by t'he singularit'y conditions imposed on some of the rules) adequate for IPC (KLEENE) and CD ( L ~P E z -ESCOBAR). With such an attitude L6PEZ-ESCOBAR calls any singularity restriction an intuitionistic rest.riction (in [3]), and using this terminology we may suniinarize the above nientioned results : 1 ) intuitionistic re~trict~ions on (+T) and ( + i ) are adequate for IPC:
2 ) intuitionistic restrictions on (-1) and (+x) (but not on (+'I')) arc adrquatc, for C' D (hut not for IPC),
- intuitionistic. restrictions on (+T) alone or on ( + i )
alone are not adequate for IPC.
But with such a n attitude we can not answer the following question: \Yliich of thc. iwles of G 1. in ninltiple form, are intuitionistically permissible. and which of t1ic.m are strictly classical (that nieans, n-hich of t.heni will convwt an otherwiw intiiit.ionistic system into a classical one)?