Por Raheleh Jalali (Institute of Computer Science - Czech Academy of Sciences).
We study the connection between the form of the primitive rules of a proof system and the rules the system admits. We introduce a general and syntactically defined family of sequent-style calculi over the modal language and its fragments as an approximate formalization for "constructively acceptable" systems. We call these calculi constructive and 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 several sequent calculi for intuitionistic modal logics, including CK, IK, and their extensions by the modal axioms T, B, 4, 5, and the axioms for bounded width and depth, and propositional lax logic. 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, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than IPC has a constructive sequent calculus.
Transmissão via Zoom (pw: 919 4789 5133).
