I'm currently learning about the epsilon calculus and have read some paper (namely 'The Epsilon Calculus and Herbrand Complexity') where it is claimed that encoding of quantifiers on the term level using the epsilon-operator may allow for a more condensed representation. The sketch of reasoning there is the following: Since modus ponens is the only inference rule in $EC_{\epsilon}$, a formula $A^{\epsilon}$ is provable in $EC_{\epsilon}$ iff there is a tautology of the form $\bigwedge_{i,j}(B_i(t_j)) \rightarrow B_i(\epsilon_xB_i(x)) \rightarrow A^{\epsilon} (*)$. Thus it suffices to find the critical formulas $B_i(t_j) \rightarrow B_i(\epsilon_xB_i(x))$, i.e., the substitutions involved in the proof of A, such that $(*)$ is a tautology.
In totally don't understand what is meant by this. I mean, isn't $\bigwedge_{i,j}(B_i(t_j) \rightarrow B_i(\epsilon_xB_i(x)))$ always a tautology? So what shall be substituted now in order to be able to derive $A^{\epsilon}$? And what is the advantage here, in what sense what this be more complicated without the use of the epsilon-operator?
