Abstract

$$\mathbf {Z}$$ is a new type of non-finitist inference, i.e., an inference that involves treating some infinite collection as completed, designed for contraction free logic with unrestricted abstraction. It has been introduced in Petersen (Studia Logica 64:365–403, 2000) and shown to be consistent within a system $$\mathbf {{}L^iD{}}{}$$ $$_{\uplambda }$$ of contraction free logic with unrestricted abstraction. In Petersen (Arch Math Log 42(7):665–694, 2003) it was established that adding $$ \mathbf {Z}$$ to $$\mathbf {{}L^iD{}}{}$$ $$_{\uplambda }$$ is sufficient to prove the totality of primitive recursive functions but it was also indicated that this would not extend to 2-recursive functions such as the Ackermann–Péter function, for instance. The purpose of the present paper is to expand the underlying idea in the construction of $$\mathbf {Z}$$ to gain a stronger notion, conveniently labeled $$\mathbf {Z}_2$$, which is sufficient to prove a form of nested double induction and thereby the totality of 2-recursive functions.