Инфинитарные исчисления для первопорядковой логики вероятности с распределением на носителе и её фрагментов — 1

Первопорядковая логика вероятности с распределением на носителе — весьма известный формальный язык для рассуждения о вероятностях в теоретической информатике. В односортной версии этой логики имеются кванторы по элементам носителя, а в двухсортной добавляются кванторы по вещественным числам. Как было показано М. Абади и Дж. Хальперном, при почти всех сигнатурах двухсортная версия имеет как минимум ту же сложность, что и полная арифметика второго порядка, а потому для неё невозможно построить адекватное инфинитарное исчисление; см. также доклад С.О. Сперанского (04.03.2025).

Нас будет интересовать аксиоматизируемость односортной версии вышеупомянутой логики. Первый доклад будет посвящён построению сильно полного инфинитарного исчисления для неё. Здесь «инфинитарность» означает, что наше исчисление будет содержать омега-правила, т.е. правила со счётным числом посылок; однако сами формулы будут конечными. На втором докладе мы рассмотрим различные естественные фрагменты данной логики.