zbMATH — the first resource for mathematics

Intuitionistic Frege systems are polynomially equivalent. (English) Zbl 1095.03062
Zap. Nauchn. Semin. POMI 316, 129-146 (2004); translation in J. Math. Sci., New York 134, No. 5, 2392-2402 (2006).
It is known that any two classical Frege systems polynomially simulate each other [see S. A. Cook, and R. A. Reckhow, “The relative efficiency of propositional proof systems”, J. Symb. Log. 44, 36–50 (1979; Zbl 0408.03044)]. As the same proof does not work for the intuitionistic Frege systems, since they can have non-derivable admissible rules, the authors polynomially simulate a single admissible rule and show that any two intuitionistic Frege systems polynomially simulate each other. In fact, it is provided that adding an admissible rule to a standard formulation of intuitionistic propositional logic cannot lead to a dramatic reduction in the size of proofs.

03F20 Complexity of proofs
03D15 Complexity of computation (including implicit computational complexity)
Full Text: EuDML