Por que esse procedimento de eliminação de corte termina (caso de contração)?

Na pesquisa de Melliès, Semântica categórica da lógica linear , é dado um procedimento de eliminação de corte para a lógica linear intuicionista, que inclui o seguinte caso:

3.9.3 Promoção x contração

A prova é transformado em prova pi $$\displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{\displaystyle\frac{\pi_2\\\vdots}{\Upsilon_1 , !A , !A , \Upsilon_2 \vdash B}}{\Upsilon_1 , !A , \Upsilon_2 \vdash B} \text{ Contraction} }{ \Upsilon_1 , !\Gamma , \Upsilon_2 \vdash B } \text{ Cut}$$ $$\displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{\pi_2\\\vdots}{\Upsilon_1 , !A , !A , \Upsilon_2 \vdash B} }{ \Upsilon_1 , !A , !\Gamma , \Upsilon_2 \vdash B } \text{ Cut} }{ \displaystyle\frac{\Upsilon_1 , !\Gamma , !\Gamma , \Upsilon_2 \vdash B}{\Upsilon_1 , !\Gamma , \Upsilon_2 \vdash B} \rlap{\;\text{ Series of Contractions and Exchanges}} } \text{ Cut}$$

Por que este é um passo indutivo válido? Nem o tamanho da fórmula de corte nem o tamanho das derivações estão diminuindo. (Na prova transformada, o ramo direito do corte inferior é potencialmente maior após a eliminação indutiva do corte superior.) Portanto, não está claro por que esse procedimento deve terminar.

Estendo o que escrevi como comentário. Como há um grande número de casos na prova, apenas dou uma idéia do motivo pelo qual essa transformação termina. A resposta curta é:

No caso de promoção versus contração, após a transformação, o número de contrações na parte da prova que contém cortes diminuiu em um.

Para detalhar um pouco mais, eu diria que você se enganou porque achou que o número de cortes ou o tamanho da prova deveriam diminuir para garantir a rescisão. No entanto, a rescisão pode ser comprovada observando outros parâmetros da prova.

Se você quiser provar a rescisão, precisará mostrar apenas que cada regra será aplicada por um número finito de tempo. Você pode provar que a promoção da regra de transformação versus contração será aplicada no máximo m vezes, em que m é o número de contrações na sua prova inicial. Para provar isso, basta observar que nenhuma regra introduz uma nova contração na árvore de provas. E este diminui o número de contração em um. Você pode fazer esse truque para qualquer outra regra "promotion vs sthg" para provar que essa será aplicada apenas um número finito de tempo.