Bounds for cut elimination in intuitionistic propositional logic (Q1204120)

Gentzen's procedure eliminates cut, but at the sacrifice of lengthening the proof super-exponentially. (And for quantificational logic, this is inevitable.) The author gives much smaller bounds for classical and intuitionistic logics. The main tool he uses is the inversion principle: roughly, one can obtain from the given proof of a sequent a simpler proof of a subsequent. For the classical case, it works naturally, and produces an exponential bound. But, in the intuitionistic case, the lack of left-right symmetry of sequents makes the situation more complicated, and the author uses new kinds of inversion operations (e.g. if \(M,(u\to v)\to w\Rightarrow r\) is derivable, then so is \(M,u,(v\to w)\Rightarrow r)\), and a new definition of degrees of formulas in which different connectives receive different weights. The bound obtained is much higher than in the classical case, and too complicated to be reproduced here. By using these devices, the author sets up a new system, which is equivalent to Gentzen's \({\mathbf{LJ}}\), to give an efficient decision procedure for intuitionistic propositional logic.