Models of linear logic

Предлагается исследование варианнта линейной логики без модальностей. В отличие от подхода с базовыми связями $\otimes$ и $()^\bot$ (линейное отрицание), сформулированного Жираром, в качестве базовых используются связки $\otimes$ и $\multimap$ (линейная импликация). Это различие позволяет нам получить широкую подсистему линейной логики (назвываемую позитивной линейной логикой) без инволютивного отрицания (если закон двойного отрицания удаляется из линейной логики в формулировке Жирара, то полученная система получается черезвычайно ограниченной). Такой подход позволяет получить несколько естественных моделей для различных подсистем линейной логики, включая генерические модели для так называемой минимальной линейной логики. В частности, показано, что эти модели возникают спонтанно в переходе от теории множеств к теории мультимножеств. В статье построена модель полной (немодальной) линейной логики, генеричная относительно любой модели позитивной линейной логики. Однако, проблема построения генеричной модели для позитивной линейной логики остается открытой. Библ. – 2 назв.