![](/files/happy5.png)
Frege system
F_d versus F_{d+1} โ โ โ
Author(s): Krajicek
Problem Find a constant
such that for any
there is a sequence of tautologies of depth
that have polynomial (or quasi-polynomial) size proofs in depth
Frege system
but requires exponential size
proofs.
![$ k $](/files/tex/c450c3185f7285cfa0b88d3a903c54f7df601201.png)
![$ d $](/files/tex/aeba4a4076fc495e8b5df04d874f2911a838883a.png)
![$ k $](/files/tex/c450c3185f7285cfa0b88d3a903c54f7df601201.png)
![$ d+1 $](/files/tex/d12876ec5aba6fc7725b6ad9bafff09031e119d8.png)
![$ F_{d+1} $](/files/tex/2129cdebf19ae664e724cfc3b91b1dd9c4c152f0.png)
![$ F_d $](/files/tex/04582527583369f7eddec662e831a2c8e3ebd722.png)
Keywords: Frege system; short proof
![Syndicate content Syndicate content](/misc/feed.png)