Релевантные системы с глобальными правилами вывода.

Abstract

Современные исследования в области неклассической логики позволяют придти к выводу, что доказательства метатеорем о наиболее важных свойствах формальных систем с релевантной импликацией часто зависят от тех методов и средств, которые используются при их построении. Собственно говоря, релевантная логика не является в этом смысле исключением. Это подтверждается следующим простым примером. Теорема об устранении сечения недоказуема для некоторых расширений модальной системы $S4$, так называемой Брауэровой системы, и $S5$ в их стандартных, "традиционных” формулировках и доказуема для этих же систем, если они построены с учетом некоторых новых или дополнительных средств. Дело, по-видимому, заключается в том, что дедуктивные свойства логического исчисления с неклассическими логическими связками существенным образом зависят от принципов, лежащих в основе синтаксического построения этого исчисления.

Логическая система может быть задана различными способами: аксиоматически, в виде табличного исчисления и т.д. Не все из них одинаково удобны для анализа выводов. Самые широкие возможности в этом плане открывают секвенциальные исчисления и системы натурального вывода. Если же речь идет о стандартизации выводов, нормализации выводов и других подобных процедурах, первостепенное значение приобретает известная теорема Генцена об устранении сечения в различных ее вариантах. Существует конкретная проблема - представить логическую систему в секвенциальной форме таким образом, чтобы имела место теорема об устранимости сечения. В области неклассических логик эта проблема нетривиальна.

В данной работе предлагается один из возможных методов построения секвенциальных исчислений с релевантной импликацией, который, по моему мнению, открывает новые возможности в плане нормализации выводов в логических системах, получивших название релевантных. В основе метода лежат выдвинутые О.Ф.Серебрянниковым идеи о различении существенных и несущественных вхождений подформул в данную формулу и использовании понятия пути в дереве секвенций. Понятие пути в выводе, по-видимому, впервые было эффективно использовано Д.Правицем в доказательстве нормализационной теоремы для системы натурального вывода [5]. Введение такого понятия в формулировку секвенциальных исчислений по существу означает нетрадиционную трактовку правил вывода. В стандартных формулировках все правила вывода локальны в том смысле, что корректность их применения зависит только от вида секвенций, являющихся посылками данного правила. Однако можно применять правила иного типа, а именно правила, регламентирующие переход от одних секвенций к другим в зависимости от того, каковы выводы секвенций, являющихся их посылками. Другими слонами, корректность применения таких правил (назовем их глобатьными правилами) всегда зависит не только от вида их посылок, но и от состояния выводов этих посылок.