F_d versus F_{d+1}

Importance: High ✭✭✭
Author(s): Krajicek, Jan
Subject: Logic
Recomm. for undergrads: no
Posted by: zitterbewegung
on: October 18th, 2007

\begin{problem} Find a constant $k$ such that for any $d$ there is a sequence of tautologies of depth $k$ that have polynomial (or quasi-polynomial) size proofs in depth $d+1$ Frege system $F_{d+1}$ but requires exponential size $F_d$ proofs. \end{problem}

Problem statement from \href{http://www.math.cas.cz/~krajicek/problemy.html#pl}.

Such tautologies are known if $k$ may depend on $d$ (for $k:= d$). This problem is also closely related to conservativity relations among bounded arithmetic theories.


*[K1] J.Krajicek: "Lower Bounds to the Size of Constant-Depth Propositional Proofs", J. of Symbolic Logic, 59(1), (1994), pp.73-86

[K2] J. Krajicek: "Bounded arithmetic, propositional logic, and complexity theory", Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, Cambridge - New York - Melbourne, (1995), 343 p. (on page 243)

* indicates original appearance(s) of problem.