What is the definition of "a derivation of a sequent "?

Question

In Chapter IV. A Sequent Calculus in Ebbinghaus' Mathematical Logic, a sequent is defined as:

If we call a nonempty list (sequence) of formulas a sequent, then we can use sequents to describe "stages in a proof". For instance, the "stage" with assumptions $\phi_1,\dots,\phi_n$ and claim $\phi$ is rendered by the sequent $\phi_1\dots \phi_n \phi$. The sequence $\phi_1 \dots\phi_n$ is called the antecedent and $\phi$ the succedent of the sequent $\phi_1\dots \phi_n \phi$.

and a sequent is defined to be derivable:

If, in the calculus $\mathfrak{S}$, there is a derivation of the sequent $\Gamma \phi$, then we write $\vdash \Gamma \phi$ and say that $\Gamma \phi$ is derivable.

1.1 Definition. A formula $\phi$ is formally provable or derivable from a set $\Phi$ of formulas (written: $\Phi \vdash \phi$) if and only if there are finitely many formulas $\phi_1,\dots,\phi_n$ in $\Phi$ such that $\vdash \phi_1 \dots\phi_n \phi$

Question: What is the definition of "a derivation of the sequent $\Gamma \phi$"? (Has it been defined in the book?)

Is "a derivation of the sequent $\Gamma \phi$" defined as a sequence of sequents, where

• the first sequent can be derived from an inference rule which has no sequent in their assumption parts, and
• each following sequent follows from some previous sequents by some inference rule?

Thanks.

---

The book gives rules of inference

We divide the rules of the sequent calculus $\mathfrak{S}$ into the following categories: structural rules (2.1, 2.2), connective rules (2.3, 2.4, 2.5, 2.6), quantifier rules (4.1,4.2) and equality rules (4.3,4.4).

All the inference rules have the form of

$$ \frac{sequent}{sequent} $$

except two inference rules which have no sequent in their assumption parts:

2.2 Assumption Rule (Assm).

$$ \frac{}{\Gamma \phi} $$

if $\phi$ is a member of $\Gamma$.

and

4.3 Reflexivity Rule for Equality (==).

$$ \frac{}{t==t} $$

Answer 1

It seems that an explicit definition of "derivation" is lacking.

The first occurrence of the term is at page 16, in the context of the calculus of terms.

The calculus is a set of rules to generate terms.

The process to produce terms is described:

We say that one can derive the string $s$ in the calculus of terms. The derivation just described can be given schematically as follows: [a sequence of terms with the corresponding rule].

The same for formulas [page 17].

Thus, a derivation in the calculus of sequents is a sequence of sequents ["we use sequents to describe "stages in a proof" ", page 60], where each sequent is produced from the previous ones according to the rules of the calculus.

This is the usual notion of derivation in a formal system: the only difference is that the "building block" is not a single formula but a sequent.