 The axiomatization of classical quantification logic with identity that emerges is discussed by Lambert (1963) with a different motivation in mind. While classical quantificational logic assumes singular terms denote members of the domain of quantification, Lambert wanted to allow for systems that remain “free” from such assumptions. Free quantificational logic makes room for empty singular terms, which fail to denote any member of the domain. That means that free logic need not prove every formula of the form: