 These are all theorems of quantificational logic with identity. Given Reflexivity (I1), the classical axiom of universal instantiation (\(\forall 1\)) is all that is required for the proof of these theorems. So, free logicians have another incentive for the retreat from (\(\forall 1\)) to (\(\forall 1^{-}\)). It is not uncommon to use an existence predicate in order to distinguish terms that denote members of the domain from those that do not. In general, \(E!t\) is read to be true if \(t\) denotes a member of the domain, and false if it does not. This existence predicate is sometimes taken as primitive and sometimes defined by the formula \(\exists x(x =t)\). That suggests a different weakening of (\(\forall 1\)):