I'm having some difficulty with understanding the following paragraphs taken from the Russell & Norvig’s Artificial Intelligence: A Modern Approach, regarding first-order logic inference:
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 Father symbol, then infinitely many nested terms such as Father(Father(Father(John))) can be constructed. Our propositional algorithms will have difficulty with an infinitely large set of sentences.
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 finite 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 (Richard and John), then all terms of depth 1 (Father(Richard) and Father(John)), then all terms of depth 2, and so on, until we are able to construct a propositional proof of the entailed sentence.
I understand that infinite nested terms are generated during substitution—but the next paragraph talking about the theorem totally goes over my head.