下のほうから
f_1(n):nで表される記号列のながさ
n*m;ｎで表される記号列の後ろにmで表される記号列を続けた記号列のGoedel数

P_1(n):nはある論理記号/変数記号のGoedel数である
P_2(n):nはある記号列のGoedel数である
P_3(n):nはある論理式のGoedel数である
P_4(l,n,m):ｎはGoedel数lの論理式とGoedel数ｎの論理式から推論規則1によって導かれる論理式のゲーデル数である
…
P_5(n):nはある証明（図）のGoedel数である
P_6(n,m):nはGoedel数nの論理式P、mはPの証明（図）のGoedel数である
∃m P_6(n,m):Goedel数nの論理式に対してある証明が存在する
つまりProv(n)

見たいな感じで気合で作ります
虱潰しよりはましだけど、これが面倒なことこの上ない