4
$\begingroup$

Herbrand's theorem shows that any formula of first-order logic can be expressed as a disjunction of quantifier-free formulas of first-order logic.

Is this equivalent to saying that Herbrand's theorem shows that any first-order logic formula can be expressed in Conjunctive Normal Form (CNF)?

$\endgroup$
4
$\begingroup$

Well, that's not really what Herbrand's theorem says. That's not a good way to think about Herbrand's theorem. To understand the answer to your question, you first need to understand a little better what Herbrand's theorem does and doesn't imply.

I suspect I know what you are thinking. You are thinking, given a statement $\varphi$ of first-order logic, you can find a disjunction $\psi_1 \lor \dots \lor \psi_k$ of quantifier-free formulas that is equivalent to $\varphi$. However, that's not really what Herbrand's theorem says. Herbrand's theorem doesn't necessarily give an effective or easy way to find the disjunction. Herbrand's theorem says that if $\varphi$ is true, then there exists such a disjunction, but to actually find the disjunction, you have to know that $\varphi$ is true, and you have to know a proof that it is true (roughly speaking).

Let me give you an example and an analogy that may clear things up. Here is D.W.'s theorem:

D.W.'s Theorem. Any formula of first-order logic can be expressed as either True or False. In other words, for every sentence $\varphi$ of first-order logic, there is a formula $\psi \in \{\text{True}, \text{False}\}$ such that $\varphi$ is valid if and only if $\psi$ is valid.

D.W.'s theorem is trivially true; I can prove it in a single line. Pretty cool, huh?

However, D.W.'s theorem is actually not very useful. Given a formula $\varphi$ of first-order logic, D.W.'s theorem doesn't help you figure out whether $\varphi$ is valid or not. Similarly, Herbrand's theorem doesn't really help you figure out whether $\varphi$ is valid or not.

Now, the formula $\text{True}$ is in Conjunctive Normal Form. Also, the formula $\text{False}$ is in Conjunctive Normal Form. Therefore, by D.W.'s theorem, every sentence $\varphi$ of first-order logic is equivalent to some quantifier-free formula $\psi$ in CNF form. However, this probably not the kind of equivalence you were hoping for, because given $\varphi$, it's not necessarily easy to compute the $\psi$ that is equivalent to $\varphi$.

$\endgroup$

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.