@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 Isn't this step redundant from viewpoint of formalist as we already assume to have our background theory to be already giva formal theory? So why do we need this "encoding in sets" construction? This part I not understand.

@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?