In Gentzen’s system \({\mathbf {LK}}\), the Cut Rule is redundant and other rules come in “dual” forms corresponding to connectives and quantifiers. Using these properties, H. Maehara gave a proof of the Craig Interpolation Theorem [Sūgaku 12, 235-237 (1960; Zbl 0123.24601)]. When going over this proof, one gets the feeling: one case is enough, all others go through just in a like manner. Extracting the cause of this feeling, the author formulates the notion of schematic regular (proof) systems, and proves that the interpolation theorem holds in them. Many definitions and apparatus are necessary to formulate the notion, but none of them is unexpected. The author indicates that various subsystems of \({\mathbf {LK}}\) and of (Girard’s) linear logic are regular systems. No richer language, like infinitary or higher-order, is considered. The reviewer should like to know if E. G. K. López-Escobar’s result on \(L_{\omega_1, \omega}\) [Fundam. Math. 57, 235-272 (1965; Zbl 0137.00701)] can be regarded as a corollary to the main theorem of this paper.
For the entire collection see [Zbl 0842.00009].