Functoroids and ptykoids (Q1345902)

In a sense, this paper is a sequel to the author's ``A proof-theoretical analysis of ptykes'' [ibid. 33, No. 1, 57-79 (1994; Zbl 0813.03041)], but is self-contained and can be read independently. Ptykoids are first-order analogues of ptykes, and are defined roughly as follows. First, a 0- functoroid is defined to be a partial recursive function, and an \((n + 1)\)-functoroid maps \(n\)-functoroids to 0-functoroids. Ptykoids are obtained by starting from total functions. (The formal definitions are quite complicated.) What is crucial is that a \(\Pi^0_{n + 2}\)- formula of PA can be reduced to the statement saying that a particular \(n\)-functoroid is a ptykoid. Then, for \(i = 1,2\), the author characterizes those ptykoids that are provably so in PA + true \(\Pi^0_{i + 1}\)-sentences, and exhibits some \(i\)-ptykoids that cannot be proved so. Thus, they provide true but non-provable \(\Pi^0_{i + 2}\)- statements, for \(i = 1,2\). In these characterizations, different auxiliary proof systems are used for \(i = 1\) and \(i = 2\). (The one for \(i = 2\) is more elaborate, naturally.) This may explain why nothing is said about cases for \(i > 2\).