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 MT in which we shall implicitly interpret T.
Instead of using Godel's hard work of developing 1T from Z1 (arithmetic), we only need the easier fact that Z1 can be developed from 1T and thus from T as follows:
First developing from 1T a description of Z1, let N0 be defined in this description as the set of "closed terms of Z1" (using no other symbols than 0,1,+,⋅). Then a suitably defined binary relation ≈ on N0 intuitively meant as "these terms designate the same number" lets such terms play the role of the numbers they designate. So N0 plays the role of a model N of Z1 once ≈ is used in guise of equality symbol in the axioms of Z1 extended by the axioms of equality.
Let N0 be the set of closed terms of the so developed Z1. So ∀tN0, "t"∈N0 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∈ℕ, {FH | 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 CS1 with the following quality requirement (otherwise more complicated tricks could still make things work...):
For any two "statements" A, A'S obtained from an aH by respectively replacing its free variable by t, t'N0 (i.e. they are a(t), a(t') whose use of parenthesis is interpreted), we have
tt' ⇒ (C(A)⇔C(A'))
Thus we can use C as a binary relation C(a,n)⇔C(A) with arguments aH and nN where t represents n.
Let G be the formula of T with free variables n, m of type N defined as

FH, 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,

tN0, 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"))
kn, B("k") ⇎ C("B","k") ⇔ C("B("k")")
AS, M⊨(AC("A")).∎