# Certain sequents as inference rules

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$.

• Not sure exactly what you mean $\varphi \vdash \psi$ is a(sequent)[en.wikipedia.org/wiki/Sequent_calculus] and sequents (like natural deduction) go all the wayback to Gerhard Gentzen[en.wikipedia.org/wiki/Gerhard_Gentzen] they are both together described in "Untersuchungen über das logische Schließen." (2 parts) Mathematische Zeitschrift. 39 . 1934 and 1935 you can use $\varphi_1 , \varphi_2 \vdash \psi$ as a rule. but $\forall x \varphi_1 , \varphi_2(x) \vdash \psi(x)$ is not wellformed while $\forall x ( \varphi_1 \to ( \varphi_2(x) \to \psi(x)))$ is wellformed. – Willemien Feb 13 '14 at 17:18