Нижние оценки длин доказательств с помощью коммуникационных аргументов

Рассмотрим такую игру: у каждого из двух участников есть подмножество одного и того же $n$-элементного множества, им требуется узнать, пересекаются ли их множества, передав как можно меньшее количество битов информации. Результат Калянасундарама и Шнитгера 1992 года гласит, что даже, если у участников будет доступ к общему источнику случайности и им требуется узнать верный ответ с вероятностью хотя бы $0.9$, то для этого в худшем случае им придется передать как минимум $Cn$ битов, где $C$ — константа.
В докладе мы увидим, как этот результат может быть использован для доказательства нижних оценок длин вывода в пропозициональных системах доказательств. Сначала мы продемонстрируем этот метод на элементарном примере для одной конкретной системы доказательств (в этой системе невыполнимость пропозициональной формулы показывается рассмотрением случаев значения четности суммы переменных). Затем мы поговорим о том, как этот метод обобщается для многих других систем доказательств.
Для понимания доклада не требуется никаких специальных знаний.