Frege systems for extensible modal logics.

*(English)*Zbl 1101.03038The 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 G. Mints and 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 [S. Buss and G. Mints, Ann. Pure Appl. Logic 99, No.1–3, 93–104 (1999; Zbl 0939.03064); M. Ferrari, C. Fiorentini, and 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.

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.

Reviewer: G. E. Mints (Stanford)

PDF
BibTeX
XML
Cite

\textit{E. Jeřábek}, Ann. Pure Appl. Logic 142, No. 1--3, 366--379 (2006; Zbl 1101.03038)

Full Text:
DOI

##### References:

[1] | Buss, S.R.; Mints, G., The complexity of the disjunction and existential properties in intuitionistic logic, Annals of pure and applied logic, 99, 93-104, (1999) · Zbl 0939.03064 |

[2] | Buss, S.R.; Pudlák, P., On the computational content of intuitionistic propositional proofs, Annals of pure and applied logic, 109, 1-2, 49-64, (2001) · Zbl 1009.03027 |

[3] | Chagrov, A.V.; Zakharyaschev, M., Modal logic, Oxford logic guides, vol. 35, (1997), Oxford University Press · Zbl 0871.03007 |

[4] | Cook, S.A.; Reckhow, R.A., The relative efficiency of propositional proof systems, Journal of symbolic logic, 44, 1, 36-50, (1979) · Zbl 0408.03044 |

[5] | Ferrari, M.; Fiorentini, C.; Fiorino, G., On the complexity of the disjunction property in intuitionistic and modal logics, ACM transactions on computational logic, 6, 3, 519-538, (2005) · Zbl 1367.03019 |

[6] | Ghilardi, S., Unification in intuitionistic logic, Journal of symbolic logic, 64, 2, 859-880, (1999) · Zbl 0930.03009 |

[7] | Ghilardi, S., Best solving modal equations, Annals of pure and applied logic, 102, 3, 183-198, (2000) · Zbl 0949.03010 |

[8] | Iemhoff, R., On the admissible rules of intuitionistic propositional logic, Journal of symbolic logic, 66, 1, 281-294, (2001) · Zbl 0986.03013 |

[9] | Jeřábek, E., Admissible rules of modal logics, Journal of logic and computation, 15, 4, 411-431, (2005) · Zbl 1077.03011 |

[10] | Kleene, S.C., Disjunction and existence under implication in elementary intuitionistic formalisms, Journal of symbolic logic, 27, 1, 11-18, (1962) · Zbl 0112.24502 |

[11] | Mints, G.; Kojevnikov, A., Intuitionistic frege systems are polynomially equivalent, Zapiski nauchnyh seminarov POMI, 316, 129-146, (2004) · Zbl 1095.03062 |

[12] | R.A. Reckhow, On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976 · Zbl 0375.02004 |

[13] | Rybakov, V.V., () |

[14] | Zakharyaschev, M., Canonical formulas for \(K 4\). part I: basic results, Journal of symbolic logic, 57, 4, 1377-1402, (1992) · Zbl 0774.03005 |

[15] | Zeman, J.J., Modal logic: the Lewis-modal systems, (1973), Oxford University Press · Zbl 0255.02014 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.