I understand that Turing reduced the halting problem to the satisfiability problem of first-order logic thus proving first-order logic undecidable. However, when thinking about the sequent calculus for first-order logic (a la Gentzen), the only problematic rules appear to be the forall-left and exists-right rules when trying to prove decidability via proof-search. When these rules are applied bottom-up with a formula of the form QxA(x) (with Q a universal or existential quantifier), they force one to instantiate the x in A(x) with some term t. Nevertheless, it seems to me that the only terms one needs to consider when performing such an instantiation are those which occur in the end sequent, or the eigenvariables that arise from forall-right or exists-left rules. All other terms appear to me to be irrelevant. Notice that if we restrict the terms t that we instantiate A(x) with to those that are eigenvariables or those that are in the end sequent, then the forall-left and exists-right rules need only be applied a finite number of times in proof-search. Thus, my question is about why this proof-search strategy does not work, and where the "non-termination" of performing proof-search enters?
I assume that my misconception has something to do with my assumption that "All other terms appear to me to be irrelevant." If this is indeed the case, then why is this assumption wrong?