A note on finiteness in the predicative foundations of arithmetic (Q1288136)

\textit{S. Feferman} and \textit{G. Hellman} showed in ``Predicative foundations of arithmetic'' [J. Philos. Log. 24, 1-17 (1995; Zbl 0816.03030)] how to establish the existence and categoricity of a natural number system by predicative means given the primitive notion of a finite set of individuals and given also a suitable pairing function operating on individuals. In the paper under review it is shown that this existence and categoricity result does not rely (even indirectly) on finite-set induction.