Generality and Existence 1: Quantification and free logic

In this paper, I motivate a cut free sequent calculus for classical logic with first order quantification, allowing for singular terms free of existential import. Along the way, I motivate a criterion for rules designed to answer Prior's question about what distinguishes rules for logical concepts, like conjunction from apparently similar rules for putative concepts like Prior's Tonk, and I show that the rules for the quantifiers-and the existence predicate-satisfy that condition.