Limites inferiores para Frege e Frege estendido

A Wikipedia [1] afirma que o limite inferior mais conhecido para o tamanho das provas de Frege é quadrático e que não há limites inferiores superlineares conhecidos para o número de linhas de provas de Frege.

Questões:

1) Qual é o limite inferior mais conhecido para o número de linhas de provas de Frege estendidas?

2) Qual é o limite inferior mais conhecido para o tamanho das provas de Frege estendidas? Ainda é quadrático como em Frege?

3) O Frege estendido do tipo árvore pode simular o Frege estendido do tipo DAG em um número polinomial de etapas. Existem limites inferiores superlineares para tamanho / número de linhas no Frege estendido semelhante a uma árvore?

4) Quais são as tautologias que levam ao limite inferior linear para o número de linhas e ao limite inferior quadrático para o tamanho das provas de Frege, conforme declarado na wikipedia?

Obs: Estou ciente do fato de que, para profundidade constante Frege, temos limites inferiores de tamanho da ordem de . Mas estou realmente interessado em poder total Frege e Extended Frege.$2^{\Omega(n^{6^{-d}})}$

[1] https://en.wikipedia.org/wiki/Frege_system

$\neg^{2n}\top$

3) Não está totalmente claro para mim como exatamente você define Frege estendido em forma de árvore (deve haver um mecanismo que permita a reutilização de axiomas de extensão), mas não estou ciente de quaisquer limites inferiores superlineares no número de linhas em Frege semelhante a árvore ou sistemas Frege estendidos.