Замечания о релевантной коннексивной логике без сокращения

Аннотация

Настоящая статья посвящена метатеоретическому исследованию CRW — непротиворечивой коннексивной релевантной логики без закона сокращения. В CRW доказуемы тезисы Аристотеля и Боэция, а антецеденты и консеквенты всех ее импликативных законов имеют хотя бы одну общую пропозициональную переменную. Отличие CRW от других коннексивных релевантных логик со схожим классом законов заключается в сохранении непротиворечивости — в CRW не существует такой формулы, что она и ее отрицание являются теоремами. Кроме того, благодаря отсутствию сокращения, в CRW блокируется стандартный вывод парадокса Карри. В основе семантики CRW лежит понятие коммутативного моноида — алгебры с коммутативной ассоциативной операцией и нейтральным элементом. Данные свойства позволяют содержательно проинтерпретировать элементы носителя алгебры как конечные совокупности эмпирических досье — конкретных наблюдений, экспериментов и измерений. В статье доказывается корректность аксиоматизации CRW и семантическая полнота относительно исчисления. Показывается, что CRW является консервативным расширением импликативного фрагмента релевантной логики RW. Доказательство семантической полноты строится методом канонической модели, опирающимся на технику А. Уркварта в адаптации Й. Вайса. Совместно оба результата устанавливают адекватность аксиоматики и семантики, то есть совпадение классов доказуемых и общезначимых формул CRW.