We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \(\Box\) and \(\Diamond\). Starting points for this research are 2-sequents and indexed-based calculi (...) (sequents and tableaux). By extending and modifying existing proposals, we show how to achieve a syntactical proof of the cut-elimination theorem that is as close as possible to the one for first-order classical logic. In doing this, we implicitly show how small is the proof-theoretical distance between classical logic and the systems under consideration. (shrink)

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class (...) is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

The paper settles an open question concerning Negri-style labeled sequent calculi for modal logics and also, indirectly, other proof systems which make (more or less) explicit use of semantic parameters in the syntax and are thus subsumed by labeled calculi, like Brünnler’s deep sequent calculi, Poggiolesi’s tree-hypersequent calculi and Fitting’s prefixed tableau systems. Specifically, the main result we prove (through a semantic argument) is that labeled calculi for the modal logics K and D remain complete w.r.t. valid sequents whose relational (...) part encodes a tree-like structure, when the unique rule which contains an harmful implicit contraction—by which the condition that the premises be less complex than the conclusion is violated—is modified into a contraction-free one respecting the latter condition, thus making the proof-search space finite. (shrink)

We develop multi-conclusion nested sequent calculi for the fifteen logics of the intuitionistic modal cube between IK and IS5. The proof of cut-free completeness for all logics is provided both syntactically via a Maehara-style translation and semantically by constructing an infinite birelational countermodel from a failed proof search. Interestingly, the Maehara-style translation for proving soundness syntactically fails due to the hierarchical structure of nested sequents. Consequently, we only provide the semantic proof of soundness. The countermodel construction used to prove completeness (...) required a completely novel approach to deal with two independent sources of non-termination in the proof search present in the case of transitive and Euclidean logics. (shrink)

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the (...) cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for S4LPN based on Artemov–Fitting models. (shrink)

In many social contexts, social influence seems to be inescapable: the behavior of others influences us to modify ours, and vice-versa. However, social psychology is full of examples of phenomena where individuals experience a discrepancy between their public behavior and their private opinion. This raises two central questions. First, how does an individual reason about the behavior of others and their private opinions in situations of social influence? And second, what are the laws of the resulting information dynamics? In this (...) paper, we address these questions by introducing a formal framework for representing reasoning about an individual’s private opinions and public behavior under the dynamics of social influence in social networks. Moreover, we dig deeper into the involved information dynamics by modeling how individuals can learn about each other based on this reasoning. This compels us to introduce a new formal notion of reflective social influence. Finally, we initialize the work on proof theory and automated reasoning for our framework by introducing a sound and complete tableaux system for a fragment of our logic. Furthermore, this constitutes the first tableau system for the “Facebook logic” of J. Seligman, F. Liu, and P. Girard. (shrink)

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to (...) a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. (shrink)

This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated (...) labelled calculus. (shrink)