Consider the set of formulae formulas of a logic. If there was only one sort of (binary) "unary" deduction $\phi \Rightarrow \psi$ - defined syntactically like $(\forall x)\phi(x) \Rightarrow \phi(a)$ - we would immediately have a category of formulaeformulas (with deductibility $\Rightarrow$ as morphism). But alas, there are also ternary other ("higher") deduction rules, e.g.
$p, \lbrace p, q \rbrace \Rightarrow p \wedge q$ (rule of conjunction)
$\lbrace p\rightarrow q, p \Rightarrow rbrace\Rightarrow q$ (modus ponens)
(How) can formulae formulas of "classical logics" (propositional and FO) be made into a category despite of those ternary other relations (= rules)?
