Abstract

\ 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 and shown to be consistent within a system \ \ of contraction free logic with unrestricted abstraction. In Petersen :665–694, 2003) it was established that adding \ to \ \ 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 \ to gain a stronger notion, conveniently labeled \, which is sufficient to prove a form of nested double induction and thereby the totality of 2-recursive functions.