How to check, whether the formula is a tautology

Question

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:

Vx(P(x)&Q(x))<->VxP(x)&VxQ(x)

My solution (not correct and not complete)

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

Vx(P(x)&Q(x))<->VxP(x)&VyQ(y)

No, I can do this:

Vx(P(x)&Q(x))<->Vx(P(x)&VyQ(y))

And this:

Vx(P(x)&Q(x))<->VyVx(P(x)&Q(y))

So my question is:

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

Answer 1

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.

Answer 2

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.