ABSTRACT

Then (AI) is adm issible for arbitrary sequents. Because let D be a deriva­ tion of M = > ▲ from which I wish to obtain a derivation of M = > N ; con­ sider the parameter tree P of ▲ , i.e . the subtree ascending from the root w ith sequents M h = > ▲ at its nodes h . Maximal nodes of P cannot be axiom s and so must be conclusions "w,M h = $ a of prem isses M h = > v . These sequents are sharp whence the restricted form (AI) w ill give a deri­ vation of M h = > v ,N from where (E n ) gives ~>v,Mh = > N . W riting P as the succedent in all sequents of P , I so obtain a derivation of M = 4 N .