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)?
Yes, (Assm) and ($\equiv$) are axioms -- formally an axiom is neither more or less than a rule of inference that requires no premises.
It's not a particular problem that a named rule of inference has instances that concludes different things from identical premises -- except notationally: of course it means that you cannot reconstruct a proof sequence from knowing which axioms are used where and which named rules used with which premises in each line. But that is not a peculiarity of this particular calculus; "structural rules" such as (Ant) are standard fare in many proof systems.
The (Ch) rule is morally equivalent to your formulation of (Cut). If you have $\Gamma\varphi$ and $\varphi\Lambda\psi$, then you can conclude $\Gamma\Lambda\varphi$ and $\Gamma\Lambda\varphi\psi$ from them by applying Ant to each of them. Then (Ch) concludes $\Gamma\Lambda\psi$.
It doesn't look like the quote from Peter Smith claims that Cut could replace the (PC) rule. Even in proper sequent calculus, Cut doesn't replace anything -- thanks to the cut elimination theorem it isn't even necessary there.
However, in Ebbinghaus' system, both of (PC) and (Ctr) are "cut-like" in that their premises contains a formula $\psi$ that disappears completely in the conclusion. Usually in sequent calculi, Cut is the only rule where a premise can contain a formula that has a more complex structure than any formula in the conclusion. And, as noted above, Cut isn't even necessary there.
Here, on the other hand, (PC) and (Ctr) are necessary -- if we remove them, we completely lose the ability to reason about negation, and with it the ability to reason about implication (which I suppose is to be treated as an abbreviation for $\neg p\lor q$).
And it is really most un-sequentlike to lack ($\neg$A) and ($\neg$S) rules. Instead, the (Ctr) rule is perverse enough to add more connectives to formula from the conclusion when building its premises.
Later edit: Here is a set of natural sequent-like ($\neg$A) and ($\neg$S) rules in the syntax of Ebbinghaus:
$$(\neg A) \frac{\Gamma\quad \varphi}{\Gamma\quad\neg\varphi\quad\psi} \qquad (\neg S) \frac{\Gamma\quad \varphi\quad \mathcal A}{\Gamma\quad\neg\varphi} \text{ where }\mathcal A\text{ is a propositional variable not free in }\Gamma, \varphi $$
However, these rules are not enough to make $\neg p\lor q$ work well as a representation of $p\to q$ -- the usual elimination rule for $\to$ goes through fine, but $\to$ cannot be introduced sensefully if it's built on a disjunction that works intuitionistically. Adding one of (PC) or (Ctr) back in would probably save that, however.