 Theorem 6.  Let n be a natural number &gt; 0. If f is a computable function, then there are infinitely many formulas A, provable in Sn, such that if k is the length of the shortest proof of A in Sn and l is the length of the shortest proof of A in Sn+1, then k &gt; f(l).