# Predicate logic - model independent solving?

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?

• Not sure if I understand what you're asking. You don't use any specific model to prove your statement ("there is a right neutral element"), you just prove it using the axioms of your theory, there is no semantics involved. Then any model for your theory will automatically satisfy that property – la flaca Feb 2 '18 at 12:04
• Exactly that's the problem. We "want" our relation to be something special here, but actually, it isn't. So while it can be interpreted like we want it, this is by far not the only possible interpretation. As such, there are statements in group theory, that do not hold for our formula, simply because they are true for one of the possible models of the formula, but not for all of them – Sudix Feb 2 '18 at 12:11
• No, that will not happen because you don't pick a model for your formula, that is not the way it goes. You pick a model for your axiomatic theory and then that formula will hold for your model – la flaca Feb 2 '18 at 12:14
• If you limit yourself to interpret your formula in any way you want, then the model in which you are interpreting it doesn't need to be a model for your theory, you don't have that guarantee – la flaca Feb 2 '18 at 12:22
• If you apply resolution to the set of axioms plus the negation of the formula, the procedure test if the formula is a logical consequence of the axioms, i.e. true in every model of the axioms. – Mauro ALLEGRANZA Feb 2 '18 at 13:11