As discussed in another MO question, Sergei Artemov has proposed that the standard formalization Con(PA) of "PA is consistent" is flawed, and has proposed a different way to formalize "proving that PA is consistent" (which he claims is closer to Hilbert's original intention).

Setting aside the debates over the "correctness" of Artemov's formalization, we can ask a technical question:

Can PA prove that ZF is consistent (in Artemov's sense)?

Artemov shows that, according to his definitions, PA proves that PA is consistent, and suggests that Hilbert's program is not yet dead. But what Hilbert wanted wasn't an arithmetic proof that arithmetic is consistent; he wanted a finitary proof that set theory is consistent. If we provisionally accept Artemov's definitions, can Hilbert's desire for a finitary proof of the consistency of set theory be realized?