Generality and Existence I: 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 ‘tonk’, and I show that the rules for the quantifiers—and the existence predicate—satisfy that condition.

Do you like this, or have a comment? (I especially value feedback on work which is yet to be be published in final form.) If you do, please  share or reply on Twitter, or  email me.