MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

2 added 81 characters in body

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)?

1

Categories of logical formulae

Consider the set of formulae of a logic. If there was only one sort of (binary) deduction - defined syntactically - we would immediately have a category of formulae (with deductibility $\Rightarrow$ as morphism). But alas, there are also ternary deduction rules, e.g.

$p, q \Rightarrow p \wedge q$ (rule of conjunction)

$p\rightarrow q, p \Rightarrow q$ (modus ponens)

(How) can formulae of "classical logics" (propositional and FO) be made into a category despite of those ternary relations (= rules)?