Dolne granice dla Frege i Extended Frege

Wikipedia [1] stwierdza, że ​​najlepiej znana dolna granica dla wielkości dowodów Frege jest kwadratowa i że nie ma znanych dolnych granic superliniowych dla liczby linii dowodów Frege.

Pytania:

1) Jaka jest najbardziej znana dolna granica dla liczby linii rozszerzonych proofów Frege?

2) Jaka jest najbardziej znana dolna granica wielkości rozszerzonych proofów Frege? Czy nadal jest kwadratowy jak we Frege?

3) Rozszerzona frege przypominająca drzewo może symulować rozszerzoną frege podobną do DAG w wielomianowej liczbie kroków. Czy są jakieś superliniowe dolne granice rozmiaru / liczby linii na podobnym do drzewa rozszerzonym Frege?

4) Jakie tautologie prowadzą do dolnej granicy liniowej dla liczby linii i do dolnej granicy kwadratowej dla wielkości w próbach Frege'a, jak podano na wikipedii?

Obs: Zdaję sobie sprawę z tego, że dla stałej głębokości Frege mamy mniejsze rozmiary rzędu rzędu $2^{\Omega(n^{6^{-d}})}$. Ale naprawdę interesuje mnie Frege z pełną mocą i Extended Frege.

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

1, 2, 4) Najbardziej znane dolne granice rozszerzonego Frege są takie same jak dla Frege: liczba liniowa linii i rozmiar kwadratowy. Dotyczy to np. Tautologii$\neg^{2n}\top$(w zasadzie każda tautologia, która nie jest instancją zastępującą krótszą tautologię i której suma długości wszystkich podformuł jest kwadratowa). Potwierdza to arytmetyka, logika zdań i teoria złożoności Krajíčka dla systemów Frege, ale argument ten działa również w przypadku rozszerzonych systemów Frege.

3) Nie jest dla mnie do końca jasne, jak dokładnie zdefiniujesz drzewiastą rozszerzoną Frege (musi istnieć mechanizm pozwalający na ponowne użycie aksjomatów rozszerzenia), ale nie znam żadnych superliniowych dolnych granic liczby linii w tregeike Frege lub rozszerzone systemy Frege.