What is a Herbrand disjunction? I am supposed to find a Herbrand Disjunction for the following formula: 
$$(\exists x)(P(f(f(x)))\supset P(x))$$
I'm still confused; what exactly is a Herbrand disjunction? Is it the same as a Herbrandization? I Googled Herbrand disjunction, but I found not a single page which defines it. 
 A: A clause C is a Herbrand disjunction for a quantified formula P when there is some $n$-ary quantifier-free relation $R$ such that


*

*C is a disjunction of literals each made up from $R$ and $n$ terms

*P is the existential closure of $R$ (i.e., $\exists x_1,...x_n. R(x_1,...,x_n)$)

*P is satisfiable iff C is.


Finding Herbrand disjunctions is a vital step in Herbrandisation, which shows how from any formula of predicate logic we can construct a proposition in Herbrand-normal form that is satisfiable iff the original formula is.  The process of Herbrandisation introduces new constants and functions, so it does not conserve logical equivalence.
A: There are differences between satisfiable (true some interpretation) and valid (true under all interpretations). A Herbrand disjunction is valid, not invalid (not false under some interpretation). More accurately a Herbrand disjunction is a tautology. The important thing is that Herbrand's fundamental theorem is that every     first-order quantified valid formula can be reduced to a finite tautological propositional quantifier-free logic formula. The creation of these disjuncts is a Herbrand expansion. When it is a tautology it is a Herbrand disjunction.
