Frege systems for extensible modal logics (Q2503409): Difference between revisions

The author shows that all Frege systems for a wide class of modal logics are polynomially equivalent. Both the result and the method are extensions of the proof by \textit{G. Mints} and \textit{A. Kojevnikov} [Zap. Nauchn. Semin. POMI 316, 129--146 (2004); translation in J. Math. Sci., New York 134, No. 5, 2392--2402 (2006; Zbl 1095.03062)] of a similar result for intuitionistic logic, with an important difference. The previous proofs of similar results for non-classical systems [\textit{S. Buss} and \textit{G. Mints}, Ann. Pure Appl. Logic 99, No.1--3, 93--104 (1999; Zbl 0939.03064); \textit{M. Ferrari}, \textit{C. Fiorentini}, and \textit{G. Fiorino}, ``On the complexity of the disjunction property in intuitionistic and modal logics'', ACM Trans. Comput. Log. 6, No. 3, 519--538 (2005)] seemed to depend at least implicitly on cut elimination: admissibility of the basic rules was originally established by cut elimination, then a shortcut has been used to make the transformation polynomial. For the results in the reviewed paper a straightforward adaptation of cut elimination is not obvious, and probably non-elegant even if possible. The extension to the modal case is obtained by a drastic simplification of a ``realizability'' introduced by Ferrari et al. [loc. cit.]. The schema of the proof is the same as in Mints and Kojevnikov's paper [loc. cit.]: it is essentially a polynomial modeling of the basic admissible rules (found in a previous paper by the author [J. Log. Comput. 15, No. 4, 411--431 (2005; Zbl 1077.03011)]) by the standard Hilbert-type system. For the case of S4 the basis consists of the standard axioms, necessitation and the rules: From \(\square [\&_{i<n}(A_i \text{ iff } \square A_i) \to \bigvee_{j<m}\square C_j] \vee \square D]\) derive \(\bigvee_{j<m}[\square \&_{i<n}A_i \to \square C_j]\vee D\). Given the derivation \(d\) of the premise (with \(n=1\) for simplicity), let \(P(A)\) mean that \(A\) is derivable using subformulas of \(d\) and their implications. The derivability of the conclusion is proved by induction on \(d\) using a relation \(|F\) of formulas determined by \(|\square F := P(\square A_0 \to F) \& |F\), respecting Boolean connectives (and defined in an arbitrary way when \(F\) is a variable). For other systems (extensions of K4 and GL) covered by the general result in the paper the \(|\)-relation is defined in a similar but different way. The domain covered by this method is clearly delineated: it consists of what is called extensible modal systems in the previous paper by the author [loc. cit.]. One obvious exception is constituted by systems without the disjunction property, such as S5 or \(\text{S4.2}=\text{S4}+(\square\neg\square p \vee\square\neg\square\neg p)\), important in view of a recent result by J. Hamkins. It is natural to expect polynomial equivalence in these cases, too. The paper is well written and relatively short. If the simplification of the kind introduced here is possible for the realizabilities used by Ferrari et al. [loc. cit.] and Mints and Kojevnikov [loc. cit.], it would be nice to state them.