Wikipedia [1] gibt an, dass die bekannteste Untergrenze für die Größe von Frege-Beweisen quadratisch ist und dass keine superlinearen Untergrenzen für die Anzahl der Zeilen von Frege-Beweisen bekannt sind.
Fragen:
1) Was ist die bekannteste Untergrenze für die Anzahl der Zeilen erweiterter Frege-Beweise?
2) Was ist die bekannteste Untergrenze für die Größe erweiterter Frege-Proofs? Ist es noch quadratisch wie in Frege?
3) Tree-like Extended Frege kann DAG-like Extended Frege in einer polynomiellen Anzahl von Schritten simulieren. Gibt es superlineare Untergrenzen für Größe / Anzahl der Linien auf baumartigen erweiterten Frege?
4) Welche Tautologien führen zur linearen Untergrenze für die Anzahl der Linien und zur quadratischen Untergrenze für die Größe in Frege-Proofs, wie in Wikipedia angegeben?
Obs: Mir ist bewusst, dass wir für Frege mit konstanter Tiefe Größenuntergrenzen in der Größenordnung von . Aber ich interessiere mich wirklich für Frege mit voller Leistung und Extended Frege.
quelle