Home » Subject » Logic

F_d versus F_{d+1}

Importance: High ✭✭✭
Author(s): Krajicek, Jan
Subject: Logic
Keywords: Frege system
short proof
Recomm. for undergrads: no
Posted by: zitterbewegung
on: October 18th, 2007
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.

Problem statement from link.

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.

Bibliography

*[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.
add new comment