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?

  • $\begingroup$ Inconsistency is easy to establish, just prove the false theorem. Consistency is much harder. You have to establish that it is impossible to prove false. $\endgroup$ – DanielV Feb 24 '15 at 20:12
  • $\begingroup$ @DanielV what is false theorem and how do I can prove it? $\endgroup$ – No one Feb 24 '15 at 20:13
  • $\begingroup$ The false theorem is false. You prove it the way you prove everything else in math. Assumptions and inferences. $\endgroup$ – DanielV Feb 24 '15 at 20:14
  • $\begingroup$ so using false theorem how do you prove the inconsistency of examples I gave? $\endgroup$ – No one Feb 24 '15 at 20:15

A useful tool is the Tableaux Method.

See also :

or :

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


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

  • $\begingroup$ When building the tree, both formulas must be in the same tree yes? If yes, then which logic operator do I have to use to connect these two formulas? I should use $AND$ , $OR$ or ... ? $\endgroup$ – No one Feb 26 '15 at 6:36
  • 1
    $\begingroup$ @Drupalist - the procedure start with the conjunction of all the formulae in the set. But the first rule to apply is the "unpacking" of the conjunction; thus, in practice, you have only to list them and go on ... $\endgroup$ – Mauro ALLEGRANZA Feb 26 '15 at 8:19
  • 1
    $\begingroup$ @Drupalist - if a quantified formula has no variables "inside", the leading quantifiers are "void" (i.e. useless) and thus you can remove them. I.e. : $\forall n (0=0)$ is simply : $0=0$. $\endgroup$ – Mauro ALLEGRANZA Feb 26 '15 at 8:35
  • 1
    $\begingroup$ @Drupalist - Assume for simplicity that the "matrix" $\phi$ has no quantifiers. Then : 1) is $x$ in $\phi$ ? If no, then $\forall x \exists y \forall z \phi$ has the "same meaning" of $\exists y \forall z \phi$, and the same for $y$. Thus, in the end, we are left with $\forall z \phi$. Now again: is $z$ in $\phi$ ? if not then it is the same as $\phi$, whose negation is obviously $\lnot \phi$. If instead $z$ is in $\phi$, we cannot omit the quantifier and we are left with $\forall z \phi$; but its negation is $\lnot \forall z \phi,$ which is not the same as $\forall z \lnot \phi$. $\endgroup$ – Mauro ALLEGRANZA Feb 26 '15 at 13:27
  • 1
    $\begingroup$ Regarding your question about "if I should remove the quantifiers then what happens to negation sign that comes before the quantifiers?" the answer is : it stay in front of the "matrix". The "formal proof" is again: start with $\lnot \forall z \phi$ and move inside the negation to get : $\exists z \lnot \phi$. But if $z$ is not contained into $\phi$ we can delete the quantifier (and the fact that it has been changed from universal to existential does not affect the meaning, because it is a "void" quantifier) and we are left with $\lnot \phi$. $\endgroup$ – Mauro ALLEGRANZA Feb 26 '15 at 13:28

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.

  • $\begingroup$ What is the appropriate method to doing this? $\endgroup$ – No one Feb 24 '15 at 20:38
  • $\begingroup$ @Drupalist: If you were to read my answer, you would find that its very first sentence answers exactly that question. The third paragraph expands further. In fact, the entire answer is aimed at answering that question. Why do you keep asking it without reading the answers you get? $\endgroup$ – Henning Makholm Feb 24 '15 at 20:39
  • $\begingroup$ So you mean there is no general solution right? then as an example ow would solve the inconsistency of the examples I gave them in the question. I only need to know a procedure to do this $\endgroup$ – No one Feb 24 '15 at 20:43
  • $\begingroup$ @Drupalist: No matter how hard you "need to know a procedure", that won't help you when there is no such procedure. The world is not going to bend to your wants and needs in that way. $\endgroup$ – Henning Makholm Feb 24 '15 at 20:45
  • 1
    $\begingroup$ Well, that's not quite accurate - the set of inconsistent families of sentences (okay, fine - inconsistent finite families of sentences) is not computable, but it is computably enumerable - there is an algorithm $P$ which, when given input a family of sentences $F$, will eventually halt if $F$ is inconsistent. This $P$ need not be particularly mysterious - just search through all possible proofs in your favorite formal proof system (natural deduction, semantic tableaux, . . .). @HenningMakholm's point is that, if $F$ happens to be consistent, then this process will never tell you that. $\endgroup$ – Noah Schweber Feb 24 '15 at 21:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.