what is regular proof

Question

What is a regular proof according to the proof theory ?I am reading Proof Theory by Gaisi Takeuti and he mentions eigenvariable which seems to be an very important concept to understand the definition fo "regular proof "

Answer 1

The concept of eigenvariable is defined at page 10 and it is use in the rules for quantifiers :

$\forall$-right and $\exists$-left.

It is the parameter or free variable occurring in the upper sequent that is used to introduce the quantifier in the lower sequent.

In both rules it is subject to a proviso : it does not occur in the lower sequent.

A regular proof is defined at page 15 :

Definition 2.9. A proof in LK is called regular if it satisfies the condition that firstly, all eigenvariables are distinct from one another, and secondly, if a free variable $a$ occurs as an eigenvariable in a sequent $S$ of the proof, then a occurs only in sequents above $S$.

---

The concept of regular proof is useful in order to prove some results regarding substitution :

Proposition 2.13. Let $t$ be an arbitrary term and $S(a)$ a provable (in LK) sequent in which $a$ is fully indicated. The $S(t)$ is also provable.