Počet záznamů: 1
Universal proof theory: Feasible admissibility in intuitionistic modal logics
- 1.
SYSNO ASEP 0600572 Druh ASEP J - Článek v odborném periodiku Zařazení RIV J - Článek v odborném periodiku Poddruh J Článek ve WOS Název Universal proof theory: Feasible admissibility in intuitionistic modal logics Tvůrce(i) Akbar Tabatabai, Seyed Amirhossein (MU-W) SAI, ORCID
Jalali Keshavarz, Raheleh (UIVT-O)Číslo článku 103526 Zdroj.dok. Annals of Pure and Applied Logic. - : Elsevier - ISSN 0168-0072
Roč. 176, č. 2 (2025)Poč.str. 40 s. Forma vydání Tištěná - P Jazyk dok. eng - angličtina Země vyd. NL - Nizozemsko Klíč. slova admissible rules ; feasible disjunction property ; intuitionistic modal logics Vědní obor RIV BA - Obecná matematika Obor OECD Pure mathematics Vědní obor RIV – spolupráce Ústav informatiky - Obecná matematika CEP GA23-04825S GA ČR - Grantová agentura ČR GA22-01137S GA ČR - Grantová agentura ČR Způsob publikování Omezený přístup Institucionální podpora MU-W - RVO:67985840 UT WOS 001349603400001 EID SCOPUS 85207773176 DOI https://doi.org/10.1016/j.apal.2024.103526 Anotace We introduce a general and syntactically defined family of sequent-style calculi over the propositional language with the modalities {□,◇} and its fragments as a formalization for constructively acceptable systems. Calling these calculi constructive, we show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser's rules. This means that there exists a polynomial-time algorithm that, given a proof of the premise of a Visser's rule, provides a proof for its conclusion. As a positive application, we establish the feasible admissibility of Visser's rules in sequent calculi for several intuitionistic modal logics, including CK, IK, their extensions by the modal axioms T, B, 4, 5, and the axioms for bounded width and depth and their fragments CK□, propositional lax logic and IPC. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser's rules, it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than IPC has a constructive sequent calculus. Pracoviště Matematický ústav Kontakt Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757 Rok sběru 2026 Elektronická adresa https://doi.org/10.1016/j.apal.2024.103526
Počet záznamů: 1