Исчисление Ламбека, обогащенное субэкспоненциалами

В варианте линейной логики Лафонта правило сокращения заменяется так называемым правилом мультиплексирования. В этой работе мы рассматриваем вариант правила мультиплексирования, в котором !A подразумевает любое положительное число копий A. Правило ослабления не допускается. Мы также заимствуем правило !-введения из так называемой легкой линейной логики Жирара. В данной работе мы изучаем исчисление Ламбека, обогащенное такими правилами.
Мы доказываем, что для обогащенного исчисления Ламбека имеет место теорема об устранении сечения и подстановке, а также соблюдается условие Ламбека о непустоте левых частей выводимых секвенций. Доказывается неразрешимость данного исчисления. Доказывается, что исчисление становится разрешимым, если количество копий A, порождаемое в правиле мультиплексирования, ограничено фиксированной константой.