In natural deduction, is it correct that an inference rule operates on sequents which have only one formula on their right hand sides?
Why does an inference rule seem to operate on formulas in Hurley's An Concise Introduction to Logic? For example:
modus ponens (MP)
$$\dfrac{\quad p ⊃ q \quad \\ \quad p \quad}{q} $$
Is it correct that an inference rule under natural deduction operates on sequents, but can be shortened by omitting the antecedents of the sequents and therefore seem to operate on formulas (succedent)? (note: a sequent consists of an antecedent of formulas and a succedent (only one formula for natural deduction).)
Thanks.
Natural deduction can be equivalently expressed in both formulations, either operating on formulas or operating on sequents.
If we restrict to the (intuitionistic) fragment with only implication, the rules for natural deduction operating on sequents are: $$ \dfrac{}{\Gamma, A \vdash A}\text{ax} \qquad \dfrac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}\to_\text{intro} \qquad \dfrac{\Gamma \vdash A \to B \qquad \Gamma \vdash A}{\Gamma \vdash B}\to_\text{elim} $$
Note that the inference rules of natural deduction for sequents change only the formula on the right part of a sequent, except for discharging some hypotheses on the left of a sequent (see $\to_\text{intro}$). For this reason, it is natural to formulate natural deduction as a deductive system operating only on formulas.
The rules for natural deduction operating on formulas are ($[A]$ means that the hypotheses $A$ is discharged):
$$ A \qquad \dfrac{[A]^* \\ \ \vdots \\ B}{A \to B}\to_\text{intro}^* \qquad \dfrac{A \to B \qquad A}{B}\to_\text{elim} $$
and we write $\Gamma \vdash_\text{ND} A$ if there is a derivation in natural deduction for formulas whose conclusion (the bottom of the derivation) is $A$ and whose hypotheses (the formulas on the top of the derivation that are not discharged) are among the formulas in $\Gamma$.
Now it is clear that $\Gamma \vdash_\text{ND} A$ in natural deduction for formulas (i.e. there is a derivation of $A$ where the hypotheses are among the formulas in $\Gamma$) if and only if the sequent $\Gamma \vdash A$ is derivable in natural deduction for sequents.
This approach extends easily to other connectives and quantifications.
As usual, each formulation has its pros and cons. For instance, natural deduction on formulas is handy to express the composition of derivations (the operation that replaces an hypothesis with a derivation of that hypothesis, if any). Natural deduction on sequents manages inference rules that discharge hypotheses (such as $\to_\text{intro}$) in a more natural way.
For the sake of completeness, the inference rules used by Hurley's book for its version of natural deduction for formulas are not exactly the same as the rules I wrote here. His modus ponens is $\to_\text{elim}$ here, but there is not analogue of $\to_\text{intro}$. This is not a problem, because his formulation of natural deduction for formulas is equivalent to the formulation of natural deduction for formulas presented here. Indeed, the rule $\to_\text{intro}$ can be simulated in his system (deduction theorem) and vice-versa, Hurley's inference rules can be simulated in the formulation of natural deduction for formulas presented here.