To Formalize theory means You have certain and countable number of **axioms and rules of inference** which can be recognized. When You formalize theory Set2 You have to chose only finite part of such possible and used rules. So It is possible that Your Set1 theory prove that certain subset of possible rules is correct and consistent. But is has hidden cost. Suppose You have such proof based on Set1 informal theory. Suppose it is finite and has length N signs. Then only finite number of rules of inference and axioms was used! So we may formalize it by adding it into Set2 and then we obtain formal theory which may prove its own consistency. This is in contradiction with Gödel Theorems. 

Then You may construct such proof, but it have to have infinite amount rules of inference and axioms which are different each other, and this has to be uncountable infinity ( because Gödel theorems are valid for countable ones)

So You probably cannot prove that this informal proof, based on open system Set1 is correct, because it has to use certain rules of inference which are not clear, maybe not consistent in every situation and probably not applicable in certain situation, and which is the most important, impossible to count, so it cannot be grouped into countable amount of axiom schemas.