I thought this is so obvious that people would have asked this question before, but for some reasons I can't find it. So here go:
We are working in PA. With Godel encoding, we can encode a FOL formula as a number. Further more, given a number, there exist FOL formula that allow us to: check whether that number is the encoding of a valid FOL formula; if it is a valid encoding, evaluate the encoded formula with a number; find the length of the formula and compare it with other numbers.
Hence we should be able to produce the FOL formula:
"x is the smallest number such that for all encoding of FOL formula that have length less than N that evaluate to true at an unique number, then x is not that number"
Here N stand for whatever an upper bound on the total length of the formula is going to be. In fact, N can be expressed by something that look like "(1+1)x(1+1)x...". Since this expression increase in length linearly while the number it expressed increase exponentially, eventually we can ensure that the number N actually is an upper bound on the length of the formula.
Hence it looks like Berry's paradox can apply. What is going on?