Interesting Identities in First-Order Logic

Question

Are there more identities of this sort (http://en.wikipedia.org/wiki/First-order_logic#Provable_identities) that are interesting/non-trivial? It seems that most further work in first-order logic is metalogical, but I wonder how much more there is to understand in the logic. Interesting boolean identities would also satisfy this question.

Answer 1

Of course there are.

Consider :

$\vdash (\alpha \rightarrow \forall x \beta) \leftrightarrow \forall x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$

$\vdash (\exists x \beta \rightarrow \alpha) \leftrightarrow \forall x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$

$\vdash (\forall x \beta \rightarrow \alpha) \leftrightarrow \exists x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$

$\vdash (\alpha \rightarrow \exists x \beta) \leftrightarrow \exists x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$

Basically, they are inter-derivable form the corresponding ones with $\land$ and $\lor$.

Are them interesting ?

In the foolowing book : George Tourlakis, Mathematical Logic (2008), the mathematical logic is treated as an equational calculus, i.e. with $\leftrightarrow$ (or $\equiv$) as "basic" connective.

There you can find a huge amount of "identities" with their proof.