This paper is a follow-up to our recent work, where we apply and extend the theory and methods of algorithmic correspondence theory previously developed for modal logics to the language \(\mathcal {L}_{R}\) of relevance logics with respect to their standard Routley-Meyer relational semantics. In the above mentioned precursor of the present work we develop a non-deterministic algorithmic procedure \(\mathsf {PEARL}\) for computing first-order equivalents in terms of that semantics and proving canonicity of formulae of a language \(\mathcal {L}^{+}_{R}\) extending \(\mathcal {L}_{R}\) with all residuals and adjoints of the connectives in \(\mathcal {L}_{R}\) . We identified a large syntactically defined class of inductive formulae in \(\mathcal {L}_{R}\) , and showed that \(\mathsf {PEARL}\) succeeds for every so defined inductive formula. In this work we present an alternative approach to defining inductive formulae for relevance logics, originally developed for polyadic modal logics in earlier works by Goranko and Vakarelov, based on a rewriting of the language \(\mathcal {L}_{R}\) that allows composing logical connectives into composite ‘box’ and ‘diamond’ terms that enable a ‘flat’ representation of formulae of \(\mathcal {L}_{R}\) , thus providing a technically simplified definition of the class of inductive formulae. We show that, modulo translation, the two approaches define the same class of inductive formulae, and explain how \(\mathsf {PEARL}\) can be modified to work on ‘flat’ inductive formulae.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Algorithmic Correspondence for Relevance Logics. II. Inductive Formulae in Flat Languages for Relevance Logics

  • Willem Conradie,
  • Valentin Goranko

摘要

This paper is a follow-up to our recent work, where we apply and extend the theory and methods of algorithmic correspondence theory previously developed for modal logics to the language \(\mathcal {L}_{R}\) of relevance logics with respect to their standard Routley-Meyer relational semantics. In the above mentioned precursor of the present work we develop a non-deterministic algorithmic procedure \(\mathsf {PEARL}\) for computing first-order equivalents in terms of that semantics and proving canonicity of formulae of a language \(\mathcal {L}^{+}_{R}\) extending \(\mathcal {L}_{R}\) with all residuals and adjoints of the connectives in \(\mathcal {L}_{R}\) . We identified a large syntactically defined class of inductive formulae in \(\mathcal {L}_{R}\) , and showed that \(\mathsf {PEARL}\) succeeds for every so defined inductive formula. In this work we present an alternative approach to defining inductive formulae for relevance logics, originally developed for polyadic modal logics in earlier works by Goranko and Vakarelov, based on a rewriting of the language \(\mathcal {L}_{R}\) that allows composing logical connectives into composite ‘box’ and ‘diamond’ terms that enable a ‘flat’ representation of formulae of \(\mathcal {L}_{R}\) , thus providing a technically simplified definition of the class of inductive formulae. We show that, modulo translation, the two approaches define the same class of inductive formulae, and explain how \(\mathsf {PEARL}\) can be modified to work on ‘flat’ inductive formulae.