Complejidad de prueba y límites inferiores

Una forma de probar NP coNP es mostrar que para cada sistema de prueba proposicional f computable en tiempo polinómico, existe una familia de tautologías para las cuales f requiere longitudes de prueba súper polinomiales (wrt la longitud de la tautología que se está probando). Resultados como el de Haken y Ajtai arreglan un sistema de prueba proposicional y prueban que cierta familia (PHP en este caso) requiere pruebas de longitud súper polinomiales.$\neq$$f$$f$

Mi pregunta: ¿Hay resultados que no arreglan un sistema de prueba y muestran, posiblemente, límites inferiores muy débiles, pero no triviales en la longitud de la prueba? Por ejemplo: ¿Hay resultados que muestren que para cada sistema de prueba proposicional, existe una familia de tautologías que requiere longitudes de prueba superlineales?

La declaración es falsa para cualquier familia de tautologías polinomiales reconocibles en el tiempo: el sistema de prueba simplemente verificará si la fórmula es una de ellas y aceptará si lo es. La longitud de prueba de ellos será O (1). Así que no creo que se conozca ningún ejemplo explícito.

$\notin$$\notin$$\notin$

Por otro lado, si NP no es igual a coNP, entonces la familia que consiste en todas las tautologías tiene una longitud súper polinómica en cualquier sistema de prueba eficiente.

Parte de lo que la gente intenta hacer en la complejidad profesional es descartar clases interesantes de algoritmos. Un límite inferior en un sistema de prueba implica un límite inferior para todos los algoritmos (no co-deterministas) cuya corrección puede demostrarse eficientemente en el sistema de prueba (si podemos formalizar y probar la corrección de un algoritmo para SAT en un sistema de prueba podemos considerar su ejecución fallida para encontrar una tarea satisfactoria como prueba de la tautología).