اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدCompleteness for Flat Modal Fixpoint Logics
140
0
0.0
(
0
)
تأليف
Luigi Santocanale
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
This paper exhibits a general and uniform method to prove completeness for certain modal fixpoint logics. Given a set Gamma of modal formulas of the form gamma(x, p1, . . ., pn), where x occurs only positively in gamma, the language Lsharp (Gamma) is obtained by adding to the language of polymodal logic a connective sharp_gamma for each gamma epsilon. The term sharp_gamma (varphi1, . . ., varphin) is meant to be interpreted as the least fixed point of the functional interpretation of the term gamma(x, varphi 1, . . ., varphi n). We consider the following problem: given Gamma, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language Lsharp (Gamma) on Kripke frames. We prove two results that solve this problem. First, let Ksharp (Gamma) be the logic obtained from the basic polymodal K by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective sharp_gamma. Provided that each indexing formula gamma satisfies the syntactic criterion of being untied in x, we prove this axiom system to be complete. Second, addressing the general case, we prove the soundness and completeness of an extension K+ (Gamma) of K_sharp (Gamma). This extension is obtained via an effective procedure that, given an indexing formula gamma as input, returns a finite set of axioms and derivation rules for sharp_gamma, of size bounded by the length of gamma. Thus the axiom system K+ (Gamma) is finite whenever Gamma is finite.
قيم البحث
اقرأ أيضاً
204 -
Eric Alsmann (School of Electrical Engineering
, Computer Science
, n University of Kassel
2021
We investigate the expressive power of the two main kinds of program logics for complex, non-regular program properties found in the literature: those extending propositional dynamic logic (PDL), and those extending the modal mu-calculus. This is ins
pired by the recent discovery of a decidable program logic called Visibly Pushdown Fixpoint Logic with Chop which extends both the modal mu-calculus and PDL over visibly pushdown languages, which, so far, constituted the ends of two pillars of decidable program logics. Here we show that this logic is not only more expressive than either of its two fragments, but in fact even more expressive than their union. Hence, the decidability border amongst program logics has been properly pushed up. We complete the picture by providing results separating all the PDL-based and modal fixpoint logics with regular, visibly pushdown and arbitrary context-free constructions.
We define a family of intuitionistic non-normal modal logics; they can bee seen as intuitionistic counterparts of classical ones. We first consider monomodal logics, which contain only one between Necessity and Possibility. We then consider the more
important case of bimodal logics, which contain both modal operators. In this case we define several interactions between Necessity and Possibility of increasing strength, although weaker than duality. For all logics we provide both a Hilbert axiomatisation and a cut-free sequent calculus, on its basis we also prove their decidability. We then give a semantic characterisation of our logics in terms of neighbourhood models. Our semantic framework captures modularly not only our systems but also already known intuitionistic non-normal modal logics such as Constructive K (CK) and the propositional fragment of Wijesekeras Constructive Concurrent Dynamic Logic.
Finiteness spaces constitute a categorical model of Linear Logic (LL) whose objects can be seen as linearly topologised spaces, (a class of topological vector spaces introduced by Lefschetz in 1942) and morphisms as continuous linear maps. First, we
recall definitions of finiteness spaces and describe their basic properties deduced from the general theory of linearly topologised spaces. Then we give an interpretation of LL based on linear algebra. Second, thanks to separation properties, we can introduce an algebraic notion of totality candidate in the framework of linearly topologised spaces: a totality candidate is a closed affine subspace which does not contain 0. We show that finiteness spaces with totality candidates constitute a model of classical LL. Finally, we give a barycentric simply typed lambda-calculus, with booleans ${mathcal{B}}$ and a conditional operator, which can be interpreted in this model. We prove completeness at type ${mathcal{B}}^nto{mathcal{B}}$ for every n by an algebraic method.
A recent strand of research in structural proof theory aims at exploring the notion of analytic calculi (i.e. those calculi that support general and modular proof-strategies for cut elimination), and at identifying classes of logics that can be captu
red in terms of these calculi. In this context, Wansing introduced the notion of proper display calculi as one possible design framework for proof calculi in which the analiticity desiderata are realized in a particularly transparent way. Recently, the theory of properly displayable logics (i.e. those logics that can be equivalently presented with some proper display calculus) has been developed in connection with generalized Sahlqvist theory (aka unified correspondence). Specifically, properly displayable logics have been syntactically characterized as those axiomatized by analytic inductive axioms, which can be equivalently and algorithmically transformed into analytic structural rules so that the resulting proper display calculi enjoy a set of basic properties: soundness, completeness, conservativity, cut elimination and subformula property. In this context, the proof that the given calculus is complete w.r.t. the original logic is usually carried out syntactically, i.e. by showing that a (cut free) derivation exists of each given axiom of the logic in the basic system to which the analytic structural rules algorithmically generated from the given axiom have been added. However, so far this proof strategy for syntactic completeness has been implemented on a case-by-case base, and not in general. In this paper, we address this gap by proving syntactic completeness for properly displayable logics in any normal (distributive) lattice expansion signature. Specifically, we show that for every analytic inductive axiom a cut free derivation can be effectively generated which has a specific shape, referred to as pre-normal form.
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a
linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Stra{ss}burger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
