PA theorem

[Giovanni Lagnese]

It is true that, for any formula with a free variable P(x) in the language
of first order arithmetic, it is a PA theorem that:
If:
i) an x exists such that P(x)
ii) for each x such that P(x) there exists a y>x such that P(y)
Then for every z there exists a k such that P(k) and k>z?
Is this, for any formula with a free variable P(x), a theorem of PA?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210718/9b0cf03a/attachment.html>