FOM: Syntactic distiction between finitary and infinitary

[JOE SHIPMAN, BLOOMBERG/ SKILLMAN]

Shoenfield asks for a syntactic definition of "finite combinatorial statement"
that includes Harvey's principles but not Erdos's.  In my post on this subject
I said that Harvey's results were all of the form "For all k there exists n
{primitive recursive predicate of k,n}".  More precisely, Harvey's proposition
A3.4' is of the form "For all k,p>=1 there exists n such that ..." where the ...
is a statement about "insertion rules in the set of k,n-trees".  From the
definitions it is obvious that for a fixed k and n one can enumerate all such
insertion rules and check the desired property for any p in an amount of time
bounded by an elementary function in n and k.  There are various ways to
formalize the notion of primitive recursive predicate syntactically going back
to Hilbert.  In any event, Harvey's statement is easily formalizable in finite
set theory (ZF/Infinity) and hence equivalent to a statement of arithmetic by
Godel coding, thus absolute for any transitive model of ZF containing all
countable ordinals.  Can Erdosian large-cardinal combinatorial principles be
stated in arithmetic?  If not, what kind of absoluteness do they have?  -- JS