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