Generalized definitional reflection and the inversion principle (Q2470764)

In this paper, definitional reflection -- a principle proposed by Hallnäs and the author in a series of other papers -- is related to the inversion principle -- as introduced by Lorenzen, corrected by Hermes, and later adopted by Prawitz for his programme of general proof theory. It is shown that ``both, definitional reflection and the inversion principle are consequences of generalized definitional reflection'', a generalization of the definitional reflection in the presence of variables. However, ``both are strictly weaker than generalized definitional reflection, but neither of them entails the other one''. To obtain generalized definitional reflection from simple definitional reflection, an \(\omega\)-principle is considered. The question remains whether there is a similar principle for the inversion principle.