Turning cycles into spirals (Q1295442)

``Cycles'' in the title refers to those in logical flow graphs, a device \textit{S. R. Buss} introduced to analyze the LK proofs [Ann. Pure Appl. Log. 53, 75-102 (1991; Zbl 0749.03039)]. Such cycles make understanding the structure of a proof difficult. To avoid them, the author introduces a new calculus ALK [= Acyclic LK], which is obtained from LK by modifying rules, \(\exists\to\), \(\to\forall\), and Cut. In particular, Cut is allowed only when its Cut formula has a decent history in that Contractions in its logical paths must have the disjunction property. The author shows that ALK, indeed, avoids cycles, and those in LK become spirals in ALK. And, an LK proof of \(n\) lines can be turned into an ALK proof of \(\exp(\exp({\mathcal O}(n)))\) lines. [Here, \(\exp(x)\) means \(2^x\).] An ALK proof becomes an LK proof when necessary Contractions are added.