 It is not clear yet whether Condition 1 gives a lower bound on the scope of provability logic. For example, it is still an open question whether GL is the provability logic of \(I \Delta_0+\Omega_1\), a theory which is somewhat weaker than \(I \Delta_0\)+EXP in that \(\Omega_1\) is the axiom asserting that for all \(x\), its power \(x^{\log(x)}\) exists. Provability logic GL is arithmetically sound with respect to \(I \Delta_0+\Omega_1\), but except for some partial results by Berarducci and Verbrugge (1993), providing arithmetic realizations consistent with \(I \Delta_0+\Omega_1\) for a restricted class of sentences consistent with GL, the question remains open. Its answer may hinge on open problems in computational complexity theory.