 The difficulty in formulating correct restrictions on these rules is connected to the absence of any obvious semantic interpretation of the instantial terms. Classically, the truth of \(\exists xF(x)\) in a model implies that (if every element of the domain has a name) then the quantification has a true instance, but not that we can identify which instance it is. Thus, when the rule of EI is used in a proof in an otherwise interpreted language, the person constructing the proof may not be in a position to define the instantial term: it remains uninterpreted. A moderately complicated model theoretic account has, however, been developed by Fine (1985a,b), which allows proof of the soundness of appropriately restricted EI and UG rules. (Those interested in using these rules for practical purposes in giving short proofs should consult Fine’s work: he gives streamlined statements of the rules and restrictions, and provides a simple algorithm, his dependency diagrams, for checking that the instantial terms in a proof comply with the restrictions.) For those familiar with Hilbert’s Epsilon Calculus (see Avigad &amp; Zach 2020), perhaps the easiest way of seeing the soundness of properly restricted EI and UG is to think of the instantial terms as abbreviating \(\epsilon\)-terms: the terms occurring in a proof that complies with the restrictions can be expanded to appropriate \(\epsilon\)-terms, whereas such expansion is blocked when the restrictions are violated (see Hazen 1987, for a more detailed account). Cellucci (1995) gives an interesting discussion on a variety of rules related to EI and UG. Pelletier (1999) recounts the many re-formulations of the UG and EI rules in the early 1950s–1960s.