A general method of axiomatizing fragments (Q1176090)

The author presents a general method for axiomatizing fragments of first- order theories. The paper is obviously the contribution [U2 ] announced by the author in Lect. Notes Math. 1104, 453-475 (1984; Zbl 0574.03049). The method is so to speak the proof-theoretic counterpart of the model- theoretic procedure of \textit{C. Smorynski} in J. Symb. Logic 42, 530-544 (1977; Zbl 0381.03046). The fragment to be axiomatized is characterized by some property which is expressed by a sequence of so-called approximations of a certain type. \textit{N. Motohashi} introduced this procedure in Fundam. Math. 120, 127-142 (1984; Zbl 0582.03004) to express uniqueness by existence. An approximation is a function which associates a formula to any sequent of a certain type. The central concept of the paper under review is that of inference forms. These are figures for inference rules such that the axioms of a theory can be gained from them. A cut-elimination theorem for theories formalized by such inference forms is given. First, the new concept is applied to get and partly regain some concrete axiomatization results, and finally two general axiomatization theorems are proven for intuitionistic and classical theories with equality.