[FOM] Zero-one law for finite random graphs

[Timothy Y. Chow]

Some weeks ago I asked about the reverse-mathematical status of the ham
sandwich theorem and of the existence of Ramanujan graphs.  Here's a third
item I'd like to ask about: the zero-one law for finite random graphs.
Let G_{n,p} be the finite random graph with n vertices, whose edges each
exist independently with probability p.  Then for any sentence phi in the
first-order language of graphs, the limit as n goes to infinity of the
probability that G_{n,p} satisfies phi is either 0 or 1.

I *think* this theorem can be stated in the first-order language of
arithmetic, but the usual proof proceeds by first showing that there
is a unique (up to isomorphism) countable random graph---an infinitary
argument.  (Thanks to Peter Cameron for pointing out this example to me.)
Is this use of infinity eliminable?  I would think that the answer to
this must be known.

This might also be an example of a probabilistic argument (albeit not
really a probabilistic *existence* argument) that doesn't "come down
to counting" (whatever that means).

Tim