Fix a signature $\sigma.$ Then a coherent formula is a first-order formula built using only $\{\wedge,\vee,\top,\bot,\exists\}.$ See the link for more information.
Furthermore, by a "special" sequent, let us mean a term of the form
$$\varphi \vdash \psi,$$
where $\varphi$ is a coherent formula and $\psi$ is an atomic formula.
Question. Have any authors explored the possibility that special sequents can be interpreted as inference rules? If so, where can I learn more?
Discussion. Here's a fluffy, example-driven discussion of what I had in mind.
We imagine our predicates are pieces of paper. A sequent of the form $\vdash P(0)$ (more properly, $\top \vdash P(0)$) just means that we may write $0$ on the piece of paper $P$ at any time. We can replace $\top$ with more interesting conditions to obtain more sophisticated inference rules. For example:
$$P(x) \wedge Q(x,y) \vdash P(y)$$
expresses that given strings $x$ and $y$, if $x$ is currently written down on $P$ and $(x,y)$ is written down on $Q$, then we're permitted to write down $y$ on $P$. Similarly with $\vee$ in place of $\wedge$.
Furthermore, existential quantification means what you'd expect: for example $$\exists x P(x) \vdash Q(0,0)$$
expresses that if we have anything whatsoever written on $P$, then we may write $(0,0)$ on $Q$.