Сети доказательства для исчисления Ламбека с одним делением и модальностью для ослабления, используемой только при отрицательной полярности

В статье вводится вариант исчисления Ламбека, допускающего пустые антецеденты секвенций. В этом варианте используются две связки: левое деление и одноместная модальность, которая встречается только с отрицательной полярностью и разрешает ослабление в антецеденте секвенции. Определяется понятие сети доказательства для этого исчисления, подобное аналогичным сетям для обычного исчисления Ламбека и линейной логики. Доказывается, что произвольная заданная секвенция выводится в рассматриваемом исчислении тогда и только тогда, когда для неё существует сеть доказательства. Тем самым устанавливается критерий для проверки выводимости в этом исчислении в терминах существования графа с определёнными свойствами (при этом размер графа ограничен длиной секвенции).