Počet záznamů: 1  

Universal proof theory: Feasible admissibility in intuitionistic modal logics

  1. 1.
    SYSNO ASEP0600572
    Druh ASEPJ - Článek v odborném periodiku
    Zařazení RIVJ - Článek v odborném periodiku
    Poddruh JČlánek ve WOS
    NázevUniversal 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ánku103526
    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íč. slovaadmissible rules ; feasible disjunction property ; intuitionistic modal logics
    Vědní obor RIVBA - Obecná matematika
    Obor OECDPure mathematics
    Vědní obor RIV – spolupráceÚstav informatiky - Obecná matematika
    CEPGA23-04825S GA ČR - Grantová agentura ČR
    GA22-01137S GA ČR - Grantová agentura ČR
    Způsob publikováníOmezený přístup
    Institucionální podporaMU-W - RVO:67985840
    UT WOS001349603400001
    EID SCOPUS85207773176
    DOI https://doi.org/10.1016/j.apal.2024.103526
    AnotaceWe 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
    KontaktJarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757
    Rok sběru2026
    Elektronická adresahttps://doi.org/10.1016/j.apal.2024.103526
Počet záznamů: 1  

  Tyto stránky využívají soubory cookies, které usnadňují jejich prohlížení. Další informace o tom jak používáme cookies.