Детали доказательства теоремы Гёделя (Мендельсон)

[Sonic86]

Читаю доказательство в книге Мендельсона Матлогика, не могу понять некоторые вещи технического характера в Предложении 3.25:

Цитата:

(4) $\operatorname{Gen}(x,y)$: "выражение с ГН $y$ получается из выражения с ГН $x$ по правилу обобщения", или формально:
$\exists v \limits_{v<y}(\operatorname{Evbl}(v)\& y=2^3*2^3*v*2^5*x*2^5)$

Кратко, $\operatorname{Evbl}(v)=1\Leftrightarrow v$ - переменная, операция $*$ - это "образ" конкатенации последовательностей во множестве арифметических операций (ГН - мое сокращение термина гёделев номер). Просто как раз $2^3*2^3*v*2^5*x*2^5$ и должно расшифровываться как формула. А у нас $3$ - ГН левой скобки, $5$ - ГН правой скобки и тогда формула расшифровывается как $((v)x)$, т.е. во-первых скобки не там стоят (раз уж автор взял такую технику написания формул, то и следовал бы ей), а во-вторых - квантор-то где? Он вообще не кодируется; верно ли, что такая "бескванторная" запись биективно соответствует кванторной записи?

Далее, в пункте 6 при определении $\operatorname{Trm}(x)$ автор зачем-то рассматривает последовательность $f;f(;f(t_1,;...;f(t_1,...,t_n;f(t_1,...,t_n)$ и на основании ее строит формулу. Но зачем - это же некорректные термины!

Потом еще вопросы будут.

[fortunat]

Все вопросы к автору.