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

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

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

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

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.

• When viewing a derivation as a sequence of sequents, must the first sequent in the sequence be derived from an inference rule which has no sequent in its assumption part?
– Tim
Jul 24, 2020 at 11:37
• @Tim - Yes; see 2.2 Assumption rule: a sequent $\Gamma \varphi$ where $\varphi$ is a member of $\Gamma$ is the "starting" axiom. In standard Sequent calculus, axioms are $A \vdash A$. Jul 27, 2020 at 7:19