2

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.

Chris Brooks
  • 7,424
Jakube
  • 1,847
  • An Herbrand disjunction for a logically valid first-order formula $\phi$ is a tautology that is a disjunction of closed instances of the Herbrand form (which is presumably what you called the herbrandization) of $\phi$. (I once wrote up a description of Herbrand forms and Herbrand's theorem, which might be useful for you. See Section 3 of "Resource Consciousness in Classical Logic" available at http://www.math.lsa.umich.edu/~ablass/llc9.pdf . – Andreas Blass Jun 08 '13 at 21:08
  • 1
    The first Google result for "Hebrand disjunction" (notice the quotes) is the Wikipedia article on Herbrand's theorem, which includes the text “If it is valid, $F(t_{11},\dots,t_{1n})\lor \dots \lor F(t_{k1}, \dots, t_{kn})$ is called a Herbrand disjunction for $(\exists y_1,\dots,y_n)F(y_1,\dots,y_n)$.” – Joshua Taylor Jun 08 '13 at 21:39
  • @Joshua Taylor How is k determined? And what is the Herbrand disjunction of the following?(∃x)(P(f(f(x)))⊃P(x)) – JOHN CORCORAN Aug 03 '16 at 20:14
  • @JOHNCORCORAN $k$ is just the number of disjuncts that you end up needing. The point is that if you know something about the domain so that you can infer, for instance, $(\exists x . P(x)) \leftrightarrow P(a) \lor P(b) \lor P(c)$, then the disjunction $P(a) \lor P(b) \lor P(c)$ is a Herbrand disjunction for $\exists x . P(x)$. Since there are three disjuncts there, the corresponding $k$ would be $3$. – Joshua Taylor Aug 03 '16 at 20:37
  • @Joshua Taylor (1) Wikipedia says nothing about a “domain”. Is that their mistake? (2)Wikipedia says the disjunction is called HERBRAND if it is valid. Is that correct? – JOHN CORCORAN Aug 03 '16 at 21:40
  • @JOHNCORCORAN Talking about the domain there may have been misleading. I think it's relevant, but not necessarily the point. As in the Wikipedia article, Herbrand's theorem says (I'll just use one variable here) that $\exists x . P(x)$ is valid if and only if there exists some valid disjunction $P(t_1) \lor \cdots \lor P(t_k)$. It doesn't say what $k$ might be. But I think the idea there is that, in the right to left direction, if $P(t_1) \lor \cdots \lor P(t_k)$ is valid, then you you can prove $\exists x . P(x)$ (just do a proof by cases). Then, in the left to right direction... – Joshua Taylor Aug 03 '16 at 22:04
  • @JOHNCORCORAN ...if $\exists x . P(x)$ is provable, then there's some finite disjunction (of $k$ disjuncts) $P(t_1) \lor \cdots \lor P(t_k)$ that is also provable. I think that direction is probably the harder one to prove. (For what it's worth, I think the reason that I mentioned domains in the earlier comment is that I was thinking about Herbrand interpretations, which construct a domain based on syntax.) – Joshua Taylor Aug 03 '16 at 22:06

2 Answers2

1

A clause C is a Herbrand disjunction for a quantified formula P when there is some $n$-ary quantifier-free relation $R$ such that

  1. C is a disjunction of literals each made up from $R$ and $n$ terms
  2. P is the existential closure of $R$ (i.e., $\exists x_1,...x_n. R(x_1,...,x_n)$)
  3. 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.

Charles Stewart
  • 4,597
  • Where does this definition come from? And how does it relate to the one at Wikipedia? @Charles Stewart – JOHN CORCORAN Aug 03 '16 at 20:25
  • 1
    @JOHNCORCORAN This definition is almost the same as the one Wikipedia, but phrased a little differently. C is the Herbrand disjunction (a disjunction of ($k$) literals, each made up from $R$ and $n$ terms: $R(t_{11},\dots,t_{1n}) \lor \dots \lor R(t_{k1},\dots,t_{kn})$), $P$ is the existential formula $\exists x_1,\dots,x_n . R(x_1, \dots, x_n)$. The only difference (which may or may not be important) is that this answer says that $P$ is satisfiable iff $C$ is, whereas Wikipedia says valid. – Joshua Taylor Aug 03 '16 at 22:14
0

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.

Michael McGrady
  • 1