I have read the answer of Carl Mummert for the question on how to avoid circularity. I would like to ask further as I want to study models of set theory. As I understand, with say assuming the consistency of ZFC, we can construct different models to prove independence result. Hence, we need not only mathematical logic with formulas and proofs etc., but some "sets" and "structures" to define models.
I eagerly want to know whether my understanding is correct: We have our first layer of logic which is just finitary (as it has only one nonlogical symbol $\epsilon$) as explained by Carl so that we can talk about sets and place ourselves in a world with sets where we can have models. We also assume the consistency of ZF-Inf (or equivalently Peano Arithmetic), we can hence use sets in the usual sense, in particular, we also have finite strings with which we make the second layer of logic and there we carry out those independence results (for instance, CH is undecidable with respect to ZFC). The syntactic stuff is from the second layer and the semantic stuff (namely the models) is from the sets under the first layer.