[FOM] ZFC-proofs of arithmetical statements

[joeshipman@aol.com]

Consider the following classes of ZFC-theorems about the integers (in a 
version of ZFC with both Separation and Replacement):

A) Arithmetical Theorems which have a proof not involving the Axiom of 
Infinity [equivalent to PA-theorems]
B) Arithmetical Theorems which have a proof not involving the Power Set 
Axiom
C) Arithmetical Theorems which have a proof not involving the 
Replacement Axiom-Scheme
D) All Arithmetical Theorems

Is it correct to say that each class strictly contains the previous 
one? Or do I need to replace B), for example, with

B') Arithmetical Theorems which have a proof not involving both the 
Power Set Axiom and the Axiom of Infinity?

What other interesting classes of arithmetical theorems can be defined 
in terms of which Axiom(-Schemes) of ZFC are needed? (Choice and 
Regularity and Extensionality ought not to matter in the presence of 
all the others, but perhaps one of them might be necessary if others 
are absent.)

-- JS