# Sequent calculi: Formalizing the term "derivation"

1. Context
Currently, I am writing a text that involves a certain sequent calculus, call it $$S$$. I want to define a function on the set $$P_S$$ of all derivations in $$S$$ by well-founded recursion on the partial order on $$P_S$$ given by the subproof-relation.

The meaning of the expression "derivation in a sequent calculus" probably is obvious to the working logician. That might be one reason why the introductory texts on proof theory that I have read (e.g. Troelstra, Ebbinghaus, Negri) do not formalize the terms "derivation in a sequent calculus“ or "proof in a sequent calculus“. However, without a formalization my attempts to define the subproof-relation etc. are unsatisfactory. Defining the set of derivations inductively seems like a good idea.

2.Questions
What are common ways to formalize the term "derivation in a sequent calculus“ in the literature? (Please give references.) As a finite list as suggested in the question posed here? As a graph (i.e. a proof tree)? Or simply without specifying "what" object a proof is: "(insert initial sequent here) is a proof. If $$\nu$$ is a proof, then (insert inference rule application in sequent calculus notation) is a proof“? What formalization do you prefer, and why?

EDIT: I believe that this question is not a duplicate of the one referenced above. The referenced question asks, whether a specific text (Ebbinghaus) gives a definition of the term derivation — to which the answer is apparently "not explicitly".

• Does this answer your question? What is the definition of "a derivation of a sequent "? If not, please edit your question to make it more precise. Commented Jul 15, 2022 at 10:40
• See Takeuti, page 11: a formal proof (or LK-proof) is a tree of sequents satisfying the following condition: (1) the topmost sequents are initial sequents; (2) every sequent except the lowest one is an upper sequent of an inference whose lower sequent is also in the tree. Commented Jul 15, 2022 at 10:51

1. An axiomatic sequent $$S$$ is a proof of a sequent $$S$$.
1. If $$\mathcal D$$ is a proof of a sequent $$S$$, then $$\dfrac {\mathcal D}{S'}$$ is a proof of a sequent $$S'$$, provided that $$S$$ is an instance of the premiss and $$S'$$ an instance of the conclusion of some one-premiss rule.