title: Confusion in first-order logic inference
body: <p>I'm having some difficulty with understanding the following paragraphs taken from the book Artificial Intelligence A modern approach, regarding first-order logic inference:</p>
  
  <p>The technique of propositionalization can be made completely general; that is, every first-order knowledge base and query can be propositionalized in such a way that entailment is preserved. Thus, we have a complete decision procedure for entailment....or perhaps not. There is a problem: When the knowledge base includes a function symbol, the set of possible ground term substitutions is infinite! For eg, if the knowledge base mentions the <em>Father</em> symbol, then infinitely many nested terms such as <em>Father(Father(Father(John)))</em> can be constructed. Our propositional algorithms will have difficulty with an infinitely large set of sentences.</p>
  
  <p>Fortunately, there is a famous theorem due to Jacques Herbrand(1930) to the effect that if a sentence is entailed by the original, first-order knowledge base, then there is a proof involving just a <em>finite</em> subset of the propositionalized knowledge base.Since any such subset has a maximum depth of nesting among it's ground terms, we can find the subset y first generating all the instantiations with constant symbols (<em>Richard</em> and <em>John</em>), then all terms of depth 1 (<em>Father(Richard)</em> and <em>Father(John)</em>), then all terms of depth 2, and so on, until we are able to construct a propositional proof of the entailed sentence.</p>
  
  <hr>
  
  <p>I understand that infinite nested terms are generated during substitution- but the next paragraph talking about the theorem totally goes over my head.</p>