@spaceisdarkgreen Think previous issues have been more or less been resolved. But what I still not understand is the reason to encode as intermediate step the formulae as sets. Lets stick on formalist's picture only. So we have 3 levels: 1) metatheory 2) background theory T' 3) object theory T. The formula $\varphi(x)$ is a priori written in language of object theory T, and by assumption $\exists^! x\, \varphi(x)$ is provable in T.

@spaceisdarkgreen ...So far we are in object theory. Now, background theory is formalized theory - as we are formalists -about object theory. So in backgrd theory we are dealing with formulae like eg $T \vdash \exists ! x\varphi(x)$ and $M\models \exists ! x\varphi(x)$ (M model of T), right? (as about(!) T). Now my question is why is it neccessary as you suggested to encode the formulae from this background theory in sets as you claimed above?

@spaceisdarkgreen Presumably I not understand what is going on in that part, but it appears strange to me how we proceed there: We take a formula in already formal background theory and encode it as a set. What is the meaning behind this procedure?

@spaceisdarkgreen As, if we as formalists assume that the background theory 2) is already a formal theory, what is the sense to "formalize" the formulae contained there?