The question is roughly: How applicable are the methods of predicate logic for concrete applications?
The difficulty I herein see is that when using e.g. resolution, one manipulates symbols without using their meaning, i.e. whatever one proves, it's always a proof valid for all models.
As an example, take group theory. Here we have 4 "axioms" (which are the definition of a group):
1) It's closed under its operation
2) associativity
3) Existence of a left neutral element
4) Existence of a left inverse element
Now, to actually use resolution, one would introduce a relation P(x,y,z) with intended meaning $x○ y = z$, pour the above axioms into formulas and then use the negation of a valid statement (i.e. tautology) to prove the tautology.
E.g. we could now make a statement saying "There exists a right neutral element". If it's true, then the axioms implicate this statement, and we can use resolution to show that the negation is an unfulfillable.
However, now the question arises:
Just because a statement is true for our model, how do we know whether it's applicable for all models that are in the scope of the broadened formula we constructed to contain the model?
In other words: How do I know whether a property of my model is provable via predicate logic resolution? And how do I avoid predicate logic resolution showing me a false result because the formula I build over the model has a model I don't care about, but in which the statement I want to show is false?
If we translate 1) into a formula, it'd be: $\forall x \forall y \exists z: P(x,y,z)$
However, even though it depicts what one wants, i.e. that if we see $P(x,y,z)$ as $x○y=z$, this means that $x○y$ always is an element of the group, it can also be seen as something completely different. This formula e.g. does not exclude the model that P is simply always true for a special $z$, which hardly describes a model for any interesting operator ○. Let's call that model "static model".
So, every true statement for our formula is also true in the static model. But not all true statements in the static model are true for our formula, e.g. in the static model we can say "For all x and y, x○y = z" for our constant z. This doesn't hold for our formula. Yes, there's models where it's correct, but there are also models where it's wrong.
So, the same probably goes for the model upon which I built the formula. But which true statements aren't true for my formula anymore? How do I recognize them?