I have some really big doubts about what is the real starting point of all (formal) mathematics.
For example: when I search on internet or study texts about the foundations of mathematics such as model theory, they always name "formulas" and "sets of formulas" quite easily. Model theory is done in set theory, such as ZFC of ZF (right?). But if it is really done in set theory (where everything is a set), shouldn't this formulas be sets? From what I know there should be some way to define or code formulas, but I haven't understood it yet so I'm not sure.
This is only one of my doubts, but now I'm going to explain my point of view of mathematics step by step so that it is possible to see if I'm missing something!
First order logic (FOD) can be defined and introduced without using the notion of set. Formal definitions are given in formal languages but since we haven't one yet, we eventually have to define the notions of first order logic in our natural language. This is not a tragedy, because in a certain sense we perfectly know our natural language and if we "assume" it, we can define the notions of FOD such as terms and well formed formulas. This definitions are not 100% formal, because we stated them in our language, but again, if we "assume" our natural language, then it's fine.
Now we have first order logic and well formed formulas. We can take as a primitive notions the membership predicate $\in$ and the equality predicate $=$. At this point we can state the axioms of set theory (ZFC for example), choose our inference rules and prove theorems about them. We can develop our usual mathematics with this axioms and objects, like analysis or analytic geometry. At this level, we say things like $$\exists x \forall y (y \not \in x) \hspace{20pt} \forall x \in \mathbb{N} \ \exists y \in \mathbb{N}(x+y=0) \hspace{20pt} \lim_{x \to 0} \frac{1}{x} = \infty \hspace{20pt} \zeta(s) = \sum_{n=1}^{\infty} \frac{1}{n^s}.$$
So far, inside ZFC the notions of "proof", "theory", "inference rule", "axiom", "language" are informal and their definition could be stated only in our informal natural language outside ZFC.
But now if we struggle a bit, we can use sets and what we know about them to formalize into ZFC our intuitive notions of formal languages, predicates, formal systems and formal theories, rules of inference, proofs and theorems (even if I don't know very well how all this complicated definitions are given). So we have defined our FOD idea into ZFC (that makes use of our intuitive FOD!). Now in ZFC we are able to formally define what a formal theory is and study it, defining the relations of "provable" $\vdash$ for set of predicates and "satisfiable" $\vDash$ between algebraic structures ("models") and set of predicates. At this level we can now say things like $$\lbrace p,q\rbrace \vdash p \wedge q \hspace{20pt} \mathcal{M} \vDash \sf PA \hspace{20pt} \textrm{Con}(T) \Leftrightarrow \nexists \varphi ( T \vdash \varphi \wedge T \vdash \neg \varphi)$$ and all of this objects are sets of our intuitive ZFC domain of discourse, so we can treat them as usual sets. In short, we are doing metamathematics in ZFC, studying theories (such as PA) written in some formal languages and asking if they are consistent, complete or sound, and all this objects are just sets. We could also study ZFC itself and define it as the set of axioms that we initially stated before. Note that now we have a formal definition of what a proof is for the formal languages that we have defined, but this is a definition for our object theories and not for our first ZFC, which has been defined just with our natural language (unless we are studying ZFC itself).
Is this view of mathematics correct or is there something that I'm missing?
I see that often it is used a completely different approach, and sometimes I even find that some metamathematical argouments or definitions are circular. I feel there's something that I'm not getting... but I don't know what it is.
Thank you for the possible help :P