"Measure" of induction for cut-elimination in sequent calculus

347 Views Asked by At

I'm not very familiar with proof thoery, so I'm in trouble understanding different versions of the proof of the Cut-elimination Theorem for sequent calculus.

In Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 35 :

the proof of admissibility of cut is by induction on the weight [amounting to the length of a formula] of the cut formula and a subinduction on the sum of heights of derivations [where the height of a derivation is the greatest number of successive applications of rules in it] of the two premisses.

In Gaisi Takeuti, Proof Theory (2nd ed - 1987), page 23, a preliminary Lemma is proved with Proof of Lemma 5.4. We prove the Lemma

by double induction on the grade $g$ [where the grade of a formula $A$ is the number of logical symbols contained in it] and rank $r$ [where the rank of a thread $\mathcal F$ containing a sequent $J$ is the number of consecutive sequents, counting upward from the upper sequent of $J$] of the proof $P$ (i.e., transfinite induction on $\omega.g + r$).

How to "unwind" Takeuti formula with Negri & von Plato "induction" ?

1

There are 1 best solutions below

3
On BEST ANSWER

The proofs are the same and only the terminology changes.

The length of a formula (weight in [NvP2001]) corresponds to the number of connectives that it has (grade in [T1987]). This is because all connectives are binary (negation can be translated into implication to falsehood, $\neg A\equiv A\to\bot$).

So the outer induction is the same in both proofs. Then, for each $n$ of the outer induction, both proofs use an inner induction on the hight / rank of the derivation of the formula with length or weight $n$.

Hight of a derivation is the maximum number of successive rules, meaning the maximum path of the proof tree of the derivation. So, having a formula of length $n$ fixed from the outer induction, say $Q$ is the sequent that concludes that formula. Then, [NvP2001] does the inner induction on the greatest path of the derivations of the premises of $Q$, meaning the greatest path of the subtree that $Q$ defines.

Rank of a derivation is the maximum number of consecutive sequents starting to count from a sequent $J$. But if you put $J=Q$, then you see that the hight of the derivations of the premises of $Q$ is exactly the same as the rank of whole proof $P$ with respect to $Q$. I mean, in the proof of [T1987], after having fixed a formula of grade $n$, he does the inner induction on the rank of whole proof $P$, where $J$ is the sequent that concludes the formula that is fixed from the outer induction (which is $Q$). Then, the rank of $P$ with respect to $J$ is the maximum path of the subtree that $J$ defines. This is exactly the same as the hight of the derivations of the two premises of $J$, where $J=Q$.

When doing two inductions, you can define a double induction, meaning one induction on one variable that has parity two and on which you do the total induction. So, Takeuti says that the variable, $v$, of the total (inner and outer together) induction is $v(g,r)=\omega\cdot g+r$. Attention that $\omega\cdot g+r$ is a new variable defined on the previous two. What you stated to be $\omega\times\omega$ is the space from which $v$ takes values. Actually, the expression $\omega\cdot g+r$ defines a hierarchy on the two inductions. In this case, it means that induction on $r$ is a subinduction of the induction on $g$. This is because $v(g,r)=\omega g +r=g+r=\max\{g,r\}$ ($\omega g$ is the intersection of $\omega$ and $g$, which is of course $g$ and $g+r$ is the union of $g$ and $r$, which is their maximum). So, you have variable $v$ defined as: $$v(g,r)= \begin{cases} g,~\text{ if } g\geq r\\ r,~\text{ if } g< r \end{cases}$$

But this is the same as doing an outer induction on $g$ and then doing an inner induction on $r$, for $r\leq g$. Because if the outer induction is on $g$, then this means that $v(g,r)=g\Rightarrow r\leq g$. So, then you do your inner induction on $r$.