Bounds for cut elimination in intuitionistic propositional logic
type: Item
instance of: scholarly article
title: Bounds for cut elimination in intuitionistic propositional logic
zbMATH Open document ID: 0765.03028
DOI: 10.1007/BF01627506
author: Jörg Hudelmaier
published in: Archive for Mathematical Logic
publication date: 1993-03-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 126099
zbMATH Keywords: length of proof
zbMATH Keywords: cut elimination
zbMATH Keywords: inversion principle
zbMATH Keywords: degrees of formulas
zbMATH Keywords: efficient decision procedure for intuitionistic propositional logic
MaRDI profile type: Publication
cites work: Q5547552
cites work: A Note on Gentzen's Decision Procedure for Intuitionistic Propositional Logic
cites work: Untersuchungen über das logische Schliessen. I
cites work: On cut elimination in the presence of perice rule
cites work: On the scheme of induction for bounded arithmetic formulas
description: scientific article; zbMATH DE number 126099