## The Berry paradox

This famous paradox is the idea of "defining" a natural number *n* as, for example
"the smallest number not definable in less than twenty words". This would define in 10
words a number... not definable in less than 20 words.

By lack of mathematical precision, this reasoning does not bring a contradiction in mathematics. Let us formalize
this paradox into the form of a proof of the weak
Truth Undefinability theorem (using definitions from there).
For convenience we shall modify the reasoning to use not the concept of number *n*
defined by a formula, but that of number *n* defined as the smallest *k* such that *F*(*k*).

Let *M*⊨*T* in which we shall implicitly interpret *T*.

Instead of using Godel's hard work of developing **1T** from *Z*_{1} (arithmetic),
we only need the easier fact that *Z*_{1} can be developed from **1T** and thus from *T*
as follows:
First developing from **1T** a description of *Z*_{1}, let *N*_{0}
be defined in this description as the set of "closed terms of *Z*_{1}" (using no
other symbols than 0,1,+,⋅).
Then a suitably defined binary relation ≈ on *N*_{0} intuitively meant as "these terms designate the same number"
lets such terms play the role of the numbers they designate. So *N*_{0} plays the role of a model *N* of
*Z*_{1} once ≈ is used in guise of equality symbol in the axioms of *Z*_{1} extended
by the axioms of equality.

Let **N**_{0} be the set of closed terms of the so developed *Z*_{1}.
So ∀*t*∈**N**_{0}, "*t*"∈*N*_{0}
and the image of "*t*" in *N* is the value of *t*.

Let *H* be the notion in *T* playing the role of range (thus contain the values of quotes) of
"formulas of *T* with only one free variable with type *N*".

Let *h* denote some "size measure" functor from *H* to *N*, so that ∀**m**∈ℕ, {*F*∈*H* | *h*(*F*) ≤ "**m**"}
is finite (it has a number of elements in ℕ).

(If the language of *T* was finite, some other definition of *h* than "size" can be used to make things work.)

Let *C*∈**S**_{1} with the following quality requirement (otherwise more complicated tricks could still make things work...):
For any two "statements" *A*, *A'*∈*S* obtained from an *a*∈*H* by respectively
replacing its free variable by *t*, *t'*∈*N*_{0} (i.e. they are *a*(*t*), *a*(*t'*)
whose use of parenthesis is interpreted), we have

*t* ≈ *t'* ⇒ (*C*(*A*)⇔*C*(*A'*))

Thus we can use *C* as a binary relation *C*(*a*,*n*)⇔*C*(*A*) with arguments
*a*∈*H* and *n*∈*N* where *t* represents *n*.

Let *G* be the formula of *T* with free variables *n*, *m* of type *N* defined as
∀*F*∈*H*, *h*(*F*) ≤ *m* ⇒ (*C*(*F*,*n*) ⇒
∃*k*<*n*, *C*(*F*,*k*))

As any big number can be expressed by some arithmetical term whose size is significantly smaller,
∃*t*∈**N**_{0}, *h*("*G*(*n*,*t*)") ≤ (value of *t*).

Fixing such a *t* interpreted in ℕ as **m** and in *N* as *m*, let *B* the formula
*G*(*n*,*t*) with free variable *n*.

As (*C*(*F*,*n*) ⇒ ∃*k*<*n*, *C*(*F*,*k*)) means that *n* is not the
smallest *k* such that *C*(*F*,*k*), by the above finiteness property of *h* we have ∃**n**∈ℕ, *B*("**n**") .

Let **n** be the smallest of them: *B*("**n**")∧∀**k**<**n**, ¬*B*("**k**").

As moreover "*B*"∈*H* and *h*("*B*") ≤ *m* we have *C*("*B*","**n**")) ⇒
∃**k**<**n**, *C*("*B*","**k**")

(*B*("**n**")∧¬*C*("*B*","**n**"))∨(∃**k**<**n**, *C*("*B*","**k**")∧ ¬*B*("**k**"))

∃**k**≤*n*, *B*("**k**") ⇎ *C*("*B*","**k**") ⇔ *C*("*B*("**k**")")

∃*A*∈**S**,
*M*⊨(*A* ⇎ *C*("*A*")).∎