Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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)?
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$.
