Abstract

We investigate introduction and elimination rules for truth-functional connectives, focusing on the general questions of the existence, for a given connective, of at least one such rule that it satisfies, and the uniqueness of a connective with respect to the set of all of them. The answers are straightforward in the context of rules using general set/set sequents of formulae, but rather complex and asymmetric in the restricted (but more often used) context of set/formula sequents, as also in the intermediate set/formula-or-empty context.