[Math] 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.