1,721,077 research outputs found
A Note on the Use of Sum in the Logic of Proofs
No full textThe Logic of Proofs~LP, introduced by Artemov, encodes the same reasoning as the modal logic~S4 using proofs explicitly present in the language. In particular, Artemov showed that three operations on proofs (application~, positive introspection~!, and sum~+) are sufficient to mimic provability concealed in S4~modality. While the first two operations go back to G{\"o}del, the exact role of~+ remained somewhat unclear. In particular, it was not known whether the other two operations are sufficient by themselves. We provide a positive answer to this question under a very weak restriction on the axiomatization of LP
Modal interpolation via nested sequents
Full text linkThe main method of proving the Craig Interpolation Property (CIP) constructively uses cut-free sequent proof systems. Until now, however, no such method has been known for proving the CIP using more general sequent-like proof formalisms, such as hypersequents, nested sequents, and labelled sequents. In this paper, we start closing this gap by presenting an algorithm for proving the CIP for modal logics by induction on a nested-sequent derivation. This algorithm is applied to all the logics of the so-called modal cube
Realization for justification logics via nested sequents: Modularity through embedding
No full textAbstractJustification logics are refinements of modal logics, where justification terms replace modalities. Modal and justification logics are connected via the so-called realization theorems. We develop a general constructive method of proving the realization of a modal logic in an appropriate justification logic by means of cut-free modal nested sequent systems. We prove a constructive realization theorem that uniformly connects every normal modal logic formed from the axioms d, t, b, 4, and 5 with one of its justification counterparts. We then generalize the notion of embedding introduced by Fitting for justification logics, which enables us to extend our realization theorem to all natural justification counterparts. As a result, we obtain a modular realization theorem that provides several justification counterparts based on various axiomatizations of a modal logic. We also prove that these justification counterparts realize the same modal logic if and only if they belong to the same equivalence class induced by our embedding relation, thereby demonstrating that the embedding provides the right level of granularity among justification logics
Weak arithmetical interpretations for the Logic of Proofs
Full text linkArtemov established an arithmetical interpretation for the Logics of Proofs LPCS, which yields a classical provability semantics for the modal logic S4. The Logics of Proofs are parameterized by so-called constant specifications CS, stating which axioms can be used in the reasoning process, and the arithmetical interpretation relies on constant specifications being finite. In this article, we remove this restriction by introducing weak arithmetical interpretations that are sound and complete for a wide class of constant specifications, including infinite ones. In particular, they interpret the full Logic of Proofs LP
A syntactic realization theorem for justification logics
No full textJustification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms \$mathsfd\$, \$mathsft\$, \$mathsfb\$, \$mathsf4\$, and \$mathsf5\$ with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting's realization merging technique. We further strengthen the realization theorem for \$mathsfKB5\$ and \$mathsfS5\$ by showing that the positive introspection operator is superfluous
Two ways to common knowledge
No full textIt is not clear what a system for evidence-based common knowledge should look like if common knowledge is treated as a greatest fixed point. This paper is a preliminary step towards such a system. We argue that the standard induction rule is not well suited to axiomatize evidence-based common knowledge. As an alternative, we study two different deductive systems for the logic of common knowledge. The first system makes use of an induction axiom whereas the second one is based on co-inductive proof theory. We show the soundness and completeness for both systems
- …
