 There is another oddity about the \(\forall\)-I rule. We initially introduced the idea of a subproof as representing suppositional reasoning: a subproof is a deduction from a hypothesis. But in \(\forall\)-I we use a subproof that doesn’t have a hypothesis! If this seems objectionably odd, we could say that the subproof of an application of \(\forall\)-I, does have a hypothesis, but an unstated, metalinguistic, one: the supposition is that the (otherwise uninterpreted) term \(a\) stands for some element in the domain. This is not as arbitrary as it might seem: if we modify the rules to give universally free logic (see Nolt 2020)—that is, quantificational logic freed from the assumptions made in ordinary first order logic that the domain is non-empty and that all singular terms denote elements of it—this hypothesis comes into the object language and is explicitly stated. Free logic is most easily formulated with an existence predicate, \(E!\), and the rule becomes