What is really a "complete" deductive system for first-order theories. Given some first-order language and a set of axioms therefrom one still needs to specify a deductive system to turn it into a full-fledged first-order theory.
Currently I'm under the following impression. There are weaker and stronger deductive systems but there is actually a formalization of what it means for a system to be "good", i.e. "of the same strength as unformalized deductive reasoning". The definition calls for the system to be "sound" and "complete". Naturally, for any system with this quality the set of derivable formulas is the same. Furthermore, the most widely considered formal deductive systems are indeed such.
Now, a couple of citations from Wikipedia.
"A deductive system is sound if any formula that can be derived in the system is logically valid. Conversely, a deductive system is complete if every logically valid formula is derivable."
"A formula is logically valid (or simply valid) if it is true in every interpretation."
Are those really the correct definitions? I just can't wrap my head around the resulting definition of completeness. I mean: "every interpretation"?! That's one inconceivable proper class! How on earth could one then prove the completeness of some system?
 A: Happily, we don't have to worry about this, at least in the first-order case.
Given a standard deductive system $S$ for classical logic, we know from the appropriate version of the so-called completeness theorem (not worrying about the label just for the moment) that if $\Gamma$ is a set of first-order sentences, and $\varphi$ is a first order sentence, then

If $\Gamma \nvdash_S \varphi$ then there is a countable model -- an interpretation in the natural numbers -- which makes $\Gamma$ all true and $\varphi$ false.

Which is certainly enough to show that

If $\Gamma \nvdash_S \varphi$ then there is a model in your favourite inclusive sense which makes $\Gamma$ all true and $\varphi$ false.

so long as the set or class of models in your favourite inclusive sense include those tiddly little countable models!
Contraposing,

If every model in your favourite inclusive sense which makes $\Gamma$ all true makes $\varphi$ true, then $\Gamma \vdash_S \varphi$.

So $S$ is complete with respect to semantic consequence defined in terms of models in your favourite inclusive sense, however you define them, so long as you include the tiddly little countable ones. Even if you go for a whopping bigger-than-set-sized class of models. So you don't need to worry, even if you allow a proper-class seized collection of models, everything stays under control!
