Буду благодарен за ответ на вопрос: правильно ли я понимаю, что в статье по первой ссылке утверждается, что в некотором смысле PA эквивалентна "ZF+аксиома отрицания бесконечности"?
"В некотором смысле эквивалентна" в данном случае означает, что в каждой из двух теорий можно построить интерпретацию другой. И нужна не просто ZF с отрицанием аксиомы бесконечности (она оказывается слишком слабой). Требуется ещё добавить аксиому, что каждое множество является подмножеством транзитивного множества (множество называется транзитивным, если каждый его элемент является его подмножеством). Видимо, эта добавка нужна, чтобы можно было доказать аксиомы индукции в модели арифметики.
Я понимаю, что "ZF+аксиома отрицания бесконечности" это намного проще, чем просто ZF без аксиомы бесконечности, о которой спрашивается в теме
Да, конечно.