Non-binary inference rules

Solution 1:

Inference rules of arity $\geq 3$ are sometimes necessary. I'll give the example closest to my mind:

In my paper Exploring the Landscape of Relational Syllogistic Logics (arXiv link) with Larry Moss, we prove completeness theorems for a number of simple logics, often using systems with inference rules of arity $\geq 3$. See e.g. the rule $(\mathsf{CASES}^*)$ in Section 2.3, the schema $(\mathsf{CHAINS})$ in Section 2.4, and the rules $(\mathsf{DD})$ and $(\mathsf{DD}')$ in Section 2.5. We also show in Section 2.2 that there is no (finite) "syllogistic proof system" for the logic we call $\mathcal{L}_2$, because any complete set of "syllogistic rules" for this logic must have rules of unbounded arity!