Laboratory of Mathematical Logic at PDMI

Вторник, 22 февраля, комната 106. Начало в 17:00.

Докладчик: В. Жижкун.

ВОССТАНОВЛЕНИЕ ДОКАЗАТЕЛЬСТВ ПО СХЕМЕ В СЕКВЕНЦИАЛЬНЫХ ИСЧИСЛЕНИЯХ
Известно, что восстановление доказательства данной секвенции по схеме - алгоритмически неразрешимая задача для исчисления LK^{\Pi\Sigma} (стандартное секвенциальное исчисление в сечениями только по предваренным формулам с "однородным" кванторным префиксом: либо только кванторы всеобщности, либо только существования). Однако оказалось, что если в этом исчислении заменить правила введения квантора на правила введения произвольного числа кванторов, то такая задача становится разрешимой для древовидных доказательств. Результат тем более интересен, так как два упомянутых исчисления эквивалентны с точки зрения выводимости.