How to check, whether the formula is a tautology

How do we decide whether the formula in predicate logic is a tautology? Is there some universal way to decide?

Let’s have an example:


My solution (not correct and not complete)

So the first thing I do is to rename some variables on the right side.


No, I can do this:


And this:


So my question is:

How can I decide and proove, whether it is a tautology?

Solutions Collecting From Web of "How to check, whether the formula is a tautology"

I quote from Wikipedia:

A tautology in first-order logic is a sentence that can be obtained by taking a tautology of propositional logic and uniformly replacing each propositional variable by a first-order formula (one formula per propositional variable).

In propositional logic a tautology is a formula which evaluates to be true for every possible substitution of truth values of its variables.

In the example

$$\forall \,x \,(P(x) \land Q(x))\iff \forall \,x \,P(x) \land \forall \,x\,Q(x)\tag 1$$

we have the following different first order formulas:

  • $\forall \,x \,(P(x) \land Q(x))$
  • $\forall \,x \,P(x)$
  • $\forall \,x\,Q(x)$

These will be replaced by $A,B$, and $C$, respectively. We get

$$A \iff B\land C$$

which is not a tautology; its truth value depends on the truth values of the variables.

$(1)$ would be a tautology of first order logic if we could create it by the reverse substitution from a tautology of propositional logic.

For another example take the propositional tautology

$$A\land B \Rightarrow A\lor B$$

and let’s do the following substitutions:

  • $A$ : $\forall \,x \,(\exists \,y \,Q(x,y))$
  • $B$ : $\exists \,y \,P(y)$.

Now, we have

$$\forall\, x \,(\exists \,y \,Q(x,y))\, \land \,\exists \,y \,P(y) \Rightarrow \,\forall \,x \,(\exists \,y \,Q(x,y)) \lor \exists \,y \,P(y)$$

which is a tautology of the first order logic because it could be obtained by a substitution of first order expressions into a propositional tautology.

To tell whether the formula is true in every interpretation, the first step is to think through what each side of the formula says about an interpretation. The left side
(\forall x)[P(x) \land Q(x)]
says that $P$ and $Q$ hold of every object $x$ in the interpretation. The right side
(\forall x)[P(x)] \land (\forall x)[Q(x)]
says that $P$ holds for every object $x$ in the interpretation, and so does $Q$. Since the right and left sides both say that $P$ and $Q$ hold of all objects, the right and left sides will be equivalent in every interpretation.

Here is an example that is not valid in every interpretation:
(\forall x)[P(x) \lor Q(x)] \Leftrightarrow (\forall x)[P(x)] \lor (\forall x)[Q(x)]
The left side says that, for each object $x$, at least one of $P$ or $Q$ holds. The right side says that either $P$ holds of every object, or else $Q$ does. That is clearly not the same thing! And it naturally suggests an interpretation: let the objects be natural numbers, let $P(x)$ say “$x$ is even”, and let $Q(x)$ say “$x$ is odd”. Then the left side of the compound formula above holds in this interpretation, but the right side does not. You should treat falling back on formal proofs to verify a formula as a kind of last resort when more intuitive methods fail.

This method (think through what the formula means) is much faster than blindly trying to use inference rules to deduce a formula.