3
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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? $\endgroup$ – Tim Jul 24 '20 at 11:37
  • $\begingroup$ @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$. $\endgroup$ – Mauro ALLEGRANZA Jul 27 '20 at 7:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.