Formula equivalence (first-order logic)

First-order formulas are equivalent if they evaluate to the same truth value in every structure under every variable assignment.

Equivalence of objects is always defined in the same way and to the same effect: objects are considered equivalent when they behave the same in all possible contexts (or contexts considered interesting); equivalent objects can be replaced for one another in all possible contexts (or contexts considered interesting).

For first-order formulas, this is spelled out in what follows.

Formal Definition

Definition First-order formulas $\varphi$ and $\psi$ over a signature $\mathcal S$ are equivalent, $\varphi \SemEquiv \psi$ in symbols, if $$[\![\varphi]\!]_\beta^\mathcal A = [\![\psi]\!]_\beta^\mathcal A$$ holds for every $\mathcal S$-structure $\mathcal A$ and $A$-variable assignment $\beta$.

Example We have $\forall x_2 R(x_2) \wedge R(x_0) \SemEquiv R(x_0) \wedge \forall x_0 R(x_0)$, but $\forall x_0 R(x_0) \not \SemEquiv \exists x_0 R(x_0)$.

 

Basic properties

The relation $\SemEquiv$, defined between first-order formulas, satisfies all properties known from equivalence relations.

Lemma The relation $\SemEquiv$, defined on first-order formulas, is an equivalence relation. More precisely:

reflexivity

$\varphi \SemEquiv \varphi$ for every first-order formula $\varphi$.

symmetry

If $\varphi \SemEquiv \psi$, then $\psi \SemEquiv \varphi$, for all first-order formulas $\varphi$ and $\psi$ over the same signature.

transitivity

If $\varphi \SemEquiv \psi$ and $\psi \SemEquiv \chi$, then $\varphi \SemEquiv \chi$, for all first-order formulas $\varphi$, $\psi$, and $\chi$ over the same signature.

The proof is straightforward.

Congruence property and further properties of the equivalence relation

An important property is that the equivalence relation is compatible with every connective and with both quantifiers.

Congruence lemma The relation $\SemEquiv$, defined on the first-order formulas over a given signature $\mathcal S$, is a congruence relation in the following sense.

1. Given an $n$-ary connective $C$ and first-order formulas $\varphi_0, \dots, \varphi_{n-1}, \psi_0, \dots, \psi_{n-1}$ over $\mathcal S$ such that $\varphi_i \SemEquiv \psi_i$ for all $i < n$, then $C(\varphi_0, \dots, \varphi_{n-1}) \SemEquiv C(\psi_0, \dots, \psi_{n-1})$.
2. Given first-order formulas $\varphi$ and $\psi$ over $\mathcal S$ such that $\varphi \SemEquiv \psi$ and $i \in \mathbf N$, then $\exists x_i \varphi \SemEquiv \exists x_i \psi$ and $\forall x_i \varphi \SemEquiv \forall x_i \psi$.

A more general variant of this lemma states that if in a given first-order formula a subformula is replaced by an equivalent formula, then the resulting formula is equivalent to the given one.

The list of basic equivalences between propositional formulas hold for first-order logic.

There are additional laws for quantifiers.