Algorithm for determining entailment in First Order Logic

Question

Consider the following algorithm for determining entailment in First-Order-Logic. 1. Convert the first order logic sentences to propositional logic. 2. Use the resolution algorithm to determine everything that is entailed by our converted sentences. In what situations does this algorithm won't work?

Answer 1

Some (arguably most) sentences of first-order logic cannot be expressed in propositional logic in any useful way. For example, "no pigs can fly" can be expressed in first-order logic as $\neg(\exists x)(P(x) \wedge F(x))$ (with the right choice of predicates). In propositional logic, the best possible translation of "no pigs can fly" is simply $Q$ - recall that propositional logic can't handle quantification or predicates. But $\neg(\exists x)(P(x) \wedge F(x))$ has all sorts of interesting consequences; for example, $(\forall x)(P(x) \implies \neg F(x))$. The best translation of this second sentence into propositional logic is just $R$. $R$ is not a consequence of $Q$ in propositional logic.

So, to answer your question about in which situations this algorithm won't work: any situation in which first-order logic is an important part of either the original sentences or of the consequences, which is almost always.

It's important to realize that first-order logic is not just propositional logic in disguise. First-order logic expresses ideas that propositional logic is literally unable to convey. So "converting" a sentence of first-order logic into propositional logic almost always loses most of the meaning.