> The meaning of the "exists" quantifier is that it runs over the universe of entities; the formula it quantifies over must be true when instantiated on at least one such entity.
This much is true when we start assigning semantics to formulas - which is what leads to model theory, where you assume that a mathematical universe already exists and you're trying to figure out which sets of formulas describe which parts of it (to oversimplify).
If you look at the ZFC axioms purely syntactically, there aren't many presuppositions. Essentially we only posit that we should be able to coherently reason about finite sequences of strings - because a first-order proof is nothing more than that. That seems easy enough to believe. And it's what allows us to write proofs with computers.
This much is true when we start assigning semantics to formulas - which is what leads to model theory, where you assume that a mathematical universe already exists and you're trying to figure out which sets of formulas describe which parts of it (to oversimplify).
If you look at the ZFC axioms purely syntactically, there aren't many presuppositions. Essentially we only posit that we should be able to coherently reason about finite sequences of strings - because a first-order proof is nothing more than that. That seems easy enough to believe. And it's what allows us to write proofs with computers.