In Ebbinghaus et al., Mathematical Logic, a sequent calculus with the following rules is used:
(Ant) $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma' & \varphi\end{array}$, if $\Gamma \subseteq \Gamma'$ $\qquad$ (Assm) $\begin{array}{ll} \\ \hline \Gamma & \varphi\end{array}$, if $\varphi \in \Gamma$
(PC) $\begin{array}{lll} \Gamma & \psi & \varphi \\ \Gamma & \lnot \psi & \varphi \\ \hline \Gamma & & \varphi\end{array}$ $\qquad\qquad$ (Ctr) $\begin{array}{lll} \Gamma & \lnot\varphi & \psi \\ \Gamma & \lnot \varphi & \lnot \psi \\ \hline \Gamma & & \varphi\end{array}$
($\lor A$) $\begin{array}{lll} \Gamma & \varphi & \chi \\ \Gamma & \psi & \chi\\ \hline \Gamma & (\varphi\lor\psi) & \chi\end{array}$ $\qquad$ ($\lor S$) $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma & (\varphi\lor\psi)\end{array}$, $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma & (\psi\lor\varphi)\end{array}$
($\exists A$) $\begin{array}{lll} \Gamma & \varphi\frac{y}{x} & \psi \\ \hline \Gamma & \exists x\varphi & \psi\end{array}$, if $y$ is not free in $\Gamma \; \exists x\varphi \; \psi$
($\exists S$) $\begin{array}{ll} \Gamma & \varphi\frac{t}{x} \\ \hline \Gamma & \exists x\varphi\end{array}$
($\equiv$) $\begin{array}{l} \\ \hline t \equiv t\end{array}$ $\qquad\qquad$ (Sub) $\begin{array}{lll} \Gamma & & \varphi\frac{t}{x} \\ \hline \Gamma & t \equiv t' & \varphi\frac{t'}{x}\end{array}$
It looks like this calculus only consists of deduction rules, without any axiom schemes. Is this correct? Or should we interpret (Assm) and ($\equiv$) as axiom schemes, because they deduce something from nothing? What about (Ant) and (Sub), where the conclusion isn't uniquely determined by the premisses, because it can contain arbitrary formulas or terms?
[Bonus question: The Hilbert system only has two deduction rules, but many axioms and axiom schemes. With the Hilbert system, I often had to look up "formal proofs" somewhere, because I didn't manage to find them myself. With the sequent calculus, I seem to be able to find the formal proofs myself. Is there a mathematical explanation for this phenomenon?]
In his review of the cited book, Peter Smith sharply criticizes the chosen deduction system:
Ch. 4 is called ‘A Sequent Calculus’. The version chosen is really, really, not very nice. For a start (albeit a minor point that only affects readability), instead of writing a sequent as $\text{‘}\Gamma \vdash \varphi\text{’}$, or $\text{‘}\Gamma \Rightarrow \varphi\text{’}$, or even $\text{‘}\Gamma : \varphi\text{’}$, EFT just write an unpunctuated $\text{‘}\Gamma \; \varphi\text{’}$. Much more seriously, they adopt a system of rules which many would say mixes up structural rules and classical logical rules for the connectives in an unprincipled way (thereby losing just the insights that a sequent system can be used to highlight). [To be more specific, they introduce a classical ‘Proof by Cases’ rule that takes us from the sequents (in their notation) $\Gamma \; \psi \; \varphi$ and $\Gamma \; \lnot \psi \; \varphi$ to $\Gamma \; \varphi$, and then appeal to Proof by Cases to get Cut as a derived rule. This really muddies the waters in various ways!]
The closest thing to (Cut) that is derived as a consequence of the rules in the book the Chain Rule:
(Ch) $\begin{array}{lll} \Gamma & & \varphi \\ \Gamma & \varphi & \psi \\ \hline \Gamma & & \psi \end{array}$ $\quad$ while (Cut) would be $\begin{array}{lcr} \Gamma & \vdash & \Delta \; \varphi \\ \varphi \; \Lambda & \vdash & \psi \\ \hline \Gamma \; \Lambda & \vdash & \Delta \; \psi \end{array}$ or $\begin{array}{lll} \Gamma & & \varphi \\ \varphi & \Lambda & \psi \\ \hline \Gamma & \Lambda & \psi \end{array}$
I don't see how (Ch) or (Cut) could replace (PC). I'm not sure whether this is related to the fact that the above calculus interprets a sequent $\phi \; \varphi \; \psi \; \chi$ as $\phi \rightarrow (\varphi \rightarrow (\psi \rightarrow \chi))$, so that each sequent must have exactly one succedent, and the $\vdash$ sign can be omitted. Is it possible to add (Cut) as rule, remove one of the other rules and possibly adjust the remaining rules slightly, and get the same calculus (where the unmodified original rules can be obtained as derived rules)?