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?

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?

REMARK: Arguably, the present question is a duplicate of Does PA prove (Artemov-style) the consistency of a stronger system? and the present question was indeed, at one point in time, closed as a duplicate. However, the community subsequently decided to reopen the present question, perhaps in part because Artemov himself has posted an answer that clarifies some things.

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 proof of the consistency of set theory be realized?

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?