 For languages that do not allow vacuous quantification, clause (ii) can in each case be omitted. Non-inclusive free logic needs an additional rule that introduces \(\rE!t\) for some new individual constant \(t\) if a path does not already contain a formula of this form.