How to find out if a set of formulas in first order language is inconsistent?

Question

What is the best and quickest way to find out if a set of formulas in first order logic is inconsistent? I really have no idea how to do that.

As an example the $\forall x \exists y \forall z$ $ \phi$ is inconsistent with $\exists x \neg \exists y \exists z$ $ \phi$ but it is consistent with the following formulas

1. $\exists x \forall y \exists z$ $ \phi$
2. $\forall x \exists y \forall z$ $ \neg \phi$
3. $\forall x \forall z \exists y$ $ \neg \phi$

Or $\{ \exists y \exists x \forall z (C(x,y,z)) \rightarrow \neg C(x,x,x) \}$ is an inconsistent formula but $\{ \forall x(A(x) \rightarrow B(x)),\forall x(A(x) \rightarrow \neg B(x))\}$ is a consistent set of formula.

I would like to know how to find out if a set of formulas in first order language is inconsistent?

Answer 1

A useful tool is the Tableaux Method.

See also :

• Raymond Smullyan, First-Order Logic (1968)

or :

• Peter Smith, An Introduction to Formal Logic (2003).

For example, "running" the method on the couple of formulae :

$∀x(A(x)→B(x)),∀x(A(x)→¬B(x))$

you will find an "open path" defining an interpretation that satisfy both. Thus the set with the two formulae is consistent.

Answer 2

There is no systematic way to determine whether a set of formulas is consistent which always works.

(If such a procedure existed it could be used to decide logical validity of first-order formulas, because $\varphi$ is logically valid exactly if $\{\neg\varphi\}$ is inconsistent, and logical validity is well known to be undecidable.)

Therefore, in general you need to be smart and find a trick that will work specifically for the particular set of formulas you're looking at.

If it is inconsistent, that can always be shown by producing a formal proof of a contradiction from starting from the formulas. (Finding such a formal proof can be difficult, though).

On the other hand, if it is consistent, it may or may not be possible to prove it is consistent. Often, and in particular in exercises, it will be possible to show a set of formulas is consistent by describing how to construct a model for them, but this approach doesn't work for all consistent sets of formulas.