Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCompleteness of logics with the transitive closure modality and related logics
99
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
We give a sufficient condition for Kripke completeness of modal logics enriched with the transitive closure modality. More precisely, we show that if a logic admits what we call definable filtration (ADF), then such an expansion of the logic is complete; in addition, has the finite model property, and again ADF. This argument can be iterated, and as an application we obtain the finite model property for PDL-like expansions of logics that ADF.
rate research
Read More
The logics RL, RP, and RG have been obtained by expanding Lukasiewicz logic L, product logic P, and Godel--Dummett logic G with rational constants. We study the lattices of extensions and structural completeness of these three expansions, obtaining results that stand in contrast to the known situation in L, P, and G. Namely, RL is hereditarily structurally complete. RP is algebraized by the variety of rational product algebras that we show to be Q-universal. We provide a base of admissible rules in RP, show their decidability, and characterize passive structural completeness for extensions of RP. Furthermore, structural completeness, hereditary structural completeness, and active structural completeness coincide for extensions of RP, and this is also the case for extensions of RG, where in turn passive structural completeness is characterized by the equivalent algebraic semantics having the joint embedding property. For nontrivial axiomatic extensions of RG we provide a base of admissible rules. We leave the problem open whether the variety of rational Godel algebras is Q-universal.
Predicate logic is the premier choice for specifying classes of relational structures. Homomorphisms are key to describing correspondences between relational structures. Questions concerning the interdependencies between these two means of characterizing (classes of) structures are of fundamental interest and can be highly non-trivial to answer. We investigate several problems regarding the homomorphism closure (homclosure) of the class of all (finite or arbitrary) models of logical sentences: membership of structures in a sentences homclosure; sentence homclosedness; homclosure characterizability in a logic; normal forms for homclosed sentences in certain logics. For a wide variety of fragments of first- and second-order predicate logic, we clarify these problems computational properties.
This paper shows how to transform explosive many-valued systems into paraconsistent logics. We investigate especially the case of three-valued systems showing how paraconsistent three-valued logics can be obtained from them.
This paper examines the complexity of hybrid logics over transitive frames, transitive trees, and linear frames. We show that satisfiability over transitive frames for the hybrid language extended with the downarrow operator is NEXPTIME-complete. This is in contrast to undecidability of satisfiability over arbitrary frames for this language (Areces, Blackburn, Marx 1999). It is also shown that adding the @ operator or the past modality leads to undecidability over transitive frames. This is again in contrast to the case of transitive trees and linear frames, where we show these languages to be nonelementarily decidable. Moreover, we establish 2EXPTIME and EXPTIME upper bounds for satisfiability over transitive frames and transitive trees, respectively, for the hybrid Until/Since language. An EXPTIME lower bound is shown to hold for the modal Until language over both frame classes.
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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
