What question did this study set out to answer?

To create a framework for sequent calculi that captures metainferences in S5 and Carnap's C.

April 3, 2026Journal of Philosophical Logic0 citationsOpen Access

Metainferences, Invalidities and Contraction-Free Sequent Calculi for S5 and Carnap’s C

Key Points

To create a framework for sequent calculi that captures metainferences in S5 and Carnap's C.
Developed a sequent calculus framework for modal logics
Represented locally and globally valid metainferences
Established contraction-free properties for the calculi
Ensured strongly terminating and backtracking-free proof search
Demonstrated that decision problems for S5 are reducible to classical logic
Showed that decision problems for Carnap's C are also reducible to classical logic
Provided a structured approach for proof search in modal logics

Abstract

Abstract This paper develops a sequent calculus framework for representing locally and globally valid metainferences through which contraction-free sequent calculi for the modal logics S5 and the propositional fragment of Carnap’s C are obtained. The sequent calculi allow for strongly terminating and backtracking-free proof search, features which in turn arguably explain why the decision problems for S5 and the propositional fragment of Carnap’s C are reducible to that of propositional classical logic.

KI fragen

Bookmark

View Full Paper