Нижние границы для Фреге и Расширенного Фреге

9

Википедия [1] утверждает, что наиболее известная нижняя оценка размера доказательств Фреге является квадратичной, и что нет известных суперлинейных нижних оценок для числа линий доказательств Фреге.

Вопросов:

1) Какова наиболее известная нижняя граница для числа строк расширенных доказательств Фреге?

2) Каков наиболее известный нижний предел для размера расширенных доказательств Фреге? Это все еще квадратично, как во Фреге?

3) Древовидный Extended Frege может имитировать DAG-подобный Extended Frege за полиномиальное количество шагов. Существуют ли суперлинейные нижние оценки для размера / числа линий на древовидном расширенном Фреге?

4) Какие тавтологии приводят к линейной нижней границе числа строк и к квадратичной нижней границе размера в доказательствах Фреге, как указано в википедии?

Obs: Мне известно о том факте, что для постоянной глубины Фреге у нас есть размер нижних границ порядка 2Ω(n6d), Но я действительно заинтересован в полной мощности Фреге и Расширенного Фреге.

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

проверка
источник

Ответы:

13

1, 2, 4) Наиболее известные нижние оценки для расширенного Фреге такие же, как для Фреге: линейное число линий и квадратичный размер. Это относится, например, к тавтологии¬2n(в основном, любая тавтология, которая не является экземпляром замещения более короткой тавтологии и чья сумма длин всех подформул является квадратичной). Это доказано в « Ограниченной арифметике» Крайчека , логике высказываний и теории сложности для систем Фреге, но аргумент работает и для расширенных систем Фреге.

3) Мне не совсем понятно, как именно вы определяете древовидный расширенный Фреге (должен быть механизм, позволяющий повторное использование аксиом расширения), но я не знаю каких-либо суперлинейных нижних границ для числа линий в древовидном Фреге или расширенные системы Фреге.

Эмиль Йержабек
источник
1
Разве вы не можете определить Extended Frege как Circuit Frege (в вашей статье APAL 2004)? И, следовательно, древовидная схема Фреге является непосредственной
Иддо Цамерет
1
@Iddo: Я могу, но я также могу определить это несколькими другими способами, и не совсем ясно, что их число будет одинаковым в этом строгом режиме (линейном).
Эмиль Йержабек
1
Кроме того, я думаю, что для расширенного Фреге нижняя граница размера является только линейной, а не квадратичной, верно?
Иддо Цамерет
2
Нет, это то, что я пытаюсь объяснить. Квадратичная нижняя граница верна для расширенного Фреге, даже если об этом обычно не говорится.
Эмиль Йержабек
1
Я думал, что это квадратично, только если вы определяете размер расширенного Фреге, считая количество (различных) подформул. Но фактический размер является линейным. Тогда мне придется вернуться к доказательству ...
Иддо Цамерет