Berry's paradox with Godel encoding

Question

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?

Answer 1

The problem comes when you write

. . . that evaluate to true at . . .

To express this in first-order logic, what you would need is a formula $\varphi$ of two variables such that for all natural numbers $m, n$, $\varphi(m, n)$ holds iff the formula with Godel number $m$ holds of $n$ in the standard model. This is impossible, by Tarski's theorem on the undefinability of truth.

Put another way, expressions of the relevant form ("The least natural number not first-order definable by a sentence with [property]") are not in fact definitions in first-order arithmetic. We can think of them as meaningful expressions in the context of arithmetic using a logic stronger than first-order logic (the general study of which is called "abstract model theory"), or as a first-order definition within some larger structure (say, in set theory), but we have to "go outside first-order arithmetic" somehow. And this prevents the paradox from working.

It's worth noting that we can get restricted truth predicates: for example, for each $k$, there is a formula $\psi_k$ of two variables such that for all natural numbers $m, n$, $\psi_k(m, n)$ holds iff $m$ is the Godel-number of a $\Sigma^0_k$-formula which holds of $n$. This lets us rigorously talk, in $\mathsf{PA}$ or similar, about the least number which is not definable by a $\Sigma^0_k$ formula of length $<$ [something really big]. But $\psi_k$, and consequently this "$\Sigma_k$-Berry definition," will be a $\Sigma^0_{k+1}$ formula. So this process never "catches its tail" and a genuine Berry paradox never arises.

Note that we can perform the same sort of "stratification" on the Liar paradox: while self-reference is achievable, the best approximation to the Liar we can get with a first-order sentence is something like "I am not a true $\Sigma_k$ sentence" - which is in fact true since it's not a $\Sigma_k$ sentence in the first place!

(Incidentally, these restricted truth predicates are quite useful in proof theory and computability theory, as are their higher analogues in set theory, so this isn't just an exercise in de-paradoxification.)