Search

The variety of weak Heyting algebras was introduced in 2005 by Celani and Jansana. This corresponds to the strict implication fragment of the normal modal logic K$K$ which is also known as the subintuitionistic local consequence of the class of all Kripke models. Subresiduated lattices are a generalization of Heyting algebras and particular cases of weak Heyting algebras. They were introduced during the 1970s by Epstein and Horn as an algebraic counterpart of some logics with strong implication previously studied by Lewy and Hacking. In this paper we study the class of implicative‐infimum subreducts of weak Heyting algebras. In particular, we prove that this class is a variety by giving an equational base for it. We also present a topological duality for the algebraic category whose objects are the implicative‐infimum subreducts of subresiduated lattices. [ABSTRACT FROM AUTHOR]

Interpretability logic is a modal formalization of relative interpretability between first‐order arithmetical theories. Verbrugge semantics is a generalization of Veltman semantics, the basic semantics for interpretability logic. Bisimulation is the basic equivalence between models for modal logic. We study various notions of bisimulation between Verbrugge models and develop a new one, which we call w‐bisimulation. We show that the new notion, while keeping the basic property that bisimilarity implies modal equivalence, is weak enough to allow the converse to hold in the finitary case. To do this, we develop and use an appropriate notion of bisimulation games between Verbrugge models. [ABSTRACT FROM AUTHOR]

The notion of a critical successor [5] in relational semantics has been central to most classic modal completeness proofs in interpretability logics. In this paper we shall work with a more general notion, that of an assuring successor. This will enable more concisely formulated completeness proofs, both with respect to ordinary and generalised Veltman semantics. Due to their interesting theoretical properties, we will devote some space to the study of a particular kind of assuring labels, the so‐called full labels and maximal labels. After a general treatment of assuringness, we shall apply it to obtain a completeness result for the modal logic ILP$\mathsf {ILP}$ w.r.t. generalised semantics for a restricted class of frames. [ABSTRACT FROM AUTHOR]

We give an extension of the Jónsson‐Tarski representation theorem for both normal and non‐normal modal algebras so that it preserves countably many infinite meets and joins. In order to extend the Jónsson‐Tarski representation to non‐normal modal algebras we consider neighborhood frames instead of Kripke frames just as Došen's duality theorem for modal algebras, and to deal with infinite meets and joins, we make use of Q‐filters, which were introduced by Rasiowa and Sikorski, instead of prime filters. By means of the extended representation theorem, we show that every predicate modal logic, whether it is normal or non‐normal, has a model defined on a neighborhood frame with constant domains, and we give a completeness theorem for some predicate modal logics with respect to classes of neighborhood frames with constant domains. Similarly, we show a model existence theorem and a completeness theorem for infinitary modal logics which allow conjunctions of countably many formulas. [ABSTRACT FROM AUTHOR]

For (finitary) deductive systems, we formulate a signature‐independent abstraction of the weak excluded middle law (WEML), which strengthens the existing general notion of an inconsistency lemma (IL). Of special interest is the case where a quasivariety K$\mathsf {K}$ algebraizes a deductive system ⊢. We prove that, in this case, if ⊢ has a WEML (in the general sense) then every relatively subdirectly irreducible member of K$\mathsf {K}$ has a greatest proper K$\mathsf {K}$‐congruence; the converse holds if ⊢ has an inconsistency lemma. The result extends, in a suitable form, to all protoalgebraic logics. A super‐intuitionistic logic possesses a WEML iff it extends KC$\mathsf {KC}$. We characterize the IL and the WEML for normal modal logics and for relevance logics. A normal extension of S4$\mathsf {S4}$ has a global consequence relation with a WEML iff it extends S4.2$\mathsf {S4.2}$, while every axiomatic extension of Rt$\mathsf {R^t}$ with an IL has a WEML. [ABSTRACT FROM AUTHOR]

Let α be an arbitrary infinite ordinal, and 2

We prove an existential analogue of the Goldblatt‐Thomason Theorem which characterizes modal definability of elementary classes of Kripke frames using closure under model theoretic constructions. The less known version of the Goldblatt‐Thomason Theorem gives general conditions, without the assumption of first‐order definability, but uses non‐standard constructions and algebraic semantics. We present a non‐algebraic proof of this result and we prove an analogous characterization for an alternative notion of modal definability, in which a class is defined by formulas which are satisfiable under any valuation (the so‐called existential validity). Continuing previous work in which model theoretic characterization for this type of definability of elementary classes was proved, we give an analogous general result without the assumption of the first‐order definability. Furthermore, we outline relationships between sets of existentially valid formulas corresponding to several well‐known modal logics. [ABSTRACT FROM AUTHOR]

The boxdot conjecture asserts that every normal modal logic that faithfully interprets [ABSTRACT FROM AUTHOR]

The filtration method is often used to prove the finite model property of modal logics. We adapt this technique to the generalized Veltman semantics for interpretability logics. In order to preserve the defining properties of generalized Veltman models, we use bisimulations to define adequate filtrations. We give an alternative proof of the finite model property of interpretability logic [ABSTRACT FROM AUTHOR]

In previous works, we presented a modification of the usual possible world semantics by introducing an independent temporal structure in each world and using accessibility functions to represent the relation among them. Different properties ofthe accessibility functions (being injective, surjective, increasing, etc.) have been considered and axiomatic systems (called functional) which define these properties have been given. Only a few ofthese systems have been proved tobe complete. The aim ofthis paper is to make a progress in the study ofcompleteness for functional systems. For this end, we use indexes as names for temporal flows and give new proofs of completeness. Specifically, we focus our attention on the system which defines injectivity, because the system which defines this property without using indexes was proved to be incomplete in previous works. The only system considered which remains incomplete is the one which defines surjectivity, even ifwe consider a sequence ofnatural extensions ofthe previous one (© 2010 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Interpretability logic is an extension of provability logic. Veltman models and generalized Veltman models are two semantics for interpretability logic. We consider a connection between Veltman semantics and generalized Veltman semantics. We prove that for a complete image-finite generalized Veltman modelW there is a Veltman model W ′ that is bisimular to W. (© 2008 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

The main purpose of this work is to introduce the class of the monadic dynamic algebras (dynamic algebras with one quantifier). Similarly to a theorem of Kozen we establish that every separable monadic dynamic algebra is isomorphic to a monadic (possibly non-standard) Kripke structure. We also classify the simple (monadic) dynamic algebras. Moreover, in the dynamic duality theory, we analyze the conditions under which a hemimorphism of a dynamic algebra into itself defines a quantifier. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

We consider first order modal logic C firstly defined by Carnap in “Meaning and Necessity” [1]. We prove elimination of nested modalities for this logic, which gives additionally the Skolem-Löwenheim theorem for C. We also evaluate the degree of unsolvability for C, by showing that it is exactly 0′. We compare this logic with the logics of Henkin quantifiers, Σ11 logic, and SO. We also shortly discuss properties of the logic C in finite models. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

The standard rule of necessitation in systems of natural deduction for the modal logic S4 concludes □A from A whenever all assumptions A depends on are modal formulas. This condition prevents the composability and normalization of derivations, and therefore modifications of the rule have been suggested. It is shown that both properties hold if, instead of changing the rule of necessitation, all elimination rules are formulated in the manner of disjunction elimination, i.e. with an arbitrary consequence. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

A spatial modal logic (SML) is introduced as an extension of the modal logic S4 with the addition of certain spatial operators. A sound and complete Kripke semantics with a natural space (or location) interpretation is obtained for SML. The finite model property with respect to the semantics for SML and the cut-elimination theorem for a modified subsystem of SML are also presented. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In this paper we study the modal behavior of Σ-preservativity, an extension of provability which is equivalent to interpretability for classical superarithmetical theories. We explain the connection between the principles of this logic and some well-known properties of HA, like the disjunction property and its admissible rules. We show that the intuitionistic modal logic given by the preservativity principles of HA known so far, is complete with respect to a certain class of frames. [ABSTRACT FROM AUTHOR]

Our purpose is to present some connections between modal incompleteness andmodal logics related to the Gödel-Löb logic GL. One of our goals is to prove that for all m, n, k, l ∈ ℕ the logic K + $\bigwedge ^{n} _{i=m}$□i($\bigwedge ^{l} _{j=k}$) □jp ↔ p) → $\bigwedge ^{n} _{i=m}$□ip is incomplete and does not have the fixed point property. As a consequence we shall obtain that the Boolos logic KH does not have the fixed point property. [ABSTRACT FROM AUTHOR]

We find an explicit basis for all admissible rules of the modal logic S4. Our basis consists of an infinite sequence of rules which have compact and simple, readable form and depend on increasing set of variables. This gives a basis for all quasi-identities valid in the free modal algebra ℱS4(ω) of countable rank. [ABSTRACT FROM AUTHOR]

The article demonstrates the completeness of a theorem for an extension of K (Kripke frame) by a definable operator in the graded infinitary system plus suitable axioms to rule it. It mentions the application of the method of consistency properties for modal systems to show this. It discusses the consistency properties of finite character, the restriction of a consistency property, and the satisfiability theorem.

The article focuses on the finite model property of normal intuitionistic modal logic over the modal intuitionistic propositional calculus (MIPC), an intuitionistic modal logic introduced by authors, A. Prior and R. A. Bull. It demonstrates that if the intuitionistic modal logic is Kripke-complete, or characterized by a class of Kripke frames, and universal, then every normal intuitionistic modal logic over MIPC has the finite model property.

The article investigates into the finite model property (FMP) with respect to admissibility. It presents general sufficient conditions for absence of FMP with respect to admissibility that are applicable to modal logics. It states that FMP plays an important role in the research of non-standard logics, and in showing the decidability of modal logics.

The article discusses the problem of mixing predicate modal logics in a-multi-modal logics. It states that mixing of Kripke-complete predicate modal logics with Barcan formula to other predicate modal logics without Barcan formula will results to Kripke-incomplete system due to incompleteness of predicate modal logics. It also states that this problem is under investigation and not addressed at all though there are some results found from studies in the last few years.

The article offers information on the consideration of finding the characterization for a finite Kripke frame in the ambit of modal logic. It says that the modal logic corresponds to the modal algebras such as Boolean algebras. It states the characterization for finite Kripke frame by finding an axiomatization of its theory. Moreover, the finite transitive frame allows a minimal characterization over finite Kripke frames.

The article focuses on developing tree-sequent calculi for normal modal logics (NLs). It shows the direct relation of modal rules to modal axioms as well as the Kripke availability relation in calculus. It states that the modal operators correspond to the movement of formulas along trees. Moreover, it exhibits the proof methods and cut-elimination theorems for main NLs.

The article discusses the properties of tense logics. It says that a finitely axiomatizable tense logic is complete in terms of Kriple semantics, d-persistent, r-persistent and has the finite model property. It defines tense logic as a normal bimodal logic containing the bimodal logic Lin.t of the class of weak orderings. It adds that tense logics are formulated in the propositional language Lwwherein with propositional variables and modal operators.

The article offers information on the use of idea of k-filter of proposition to explain the weakly aggregative necessity of common idiom and neighbourhood semantics. It states the presentation of proof on the modal logic of k-ary frame theory through language-independent terms. It mentions the development of elementary theory on the k-filters and its application on ultrafilter extension.

The article focuses on the infinitary extension of the basic graded normal system which allows countable disjunctions and conjunctions. It states that a completeness theorem was used to prove the extension. It mentions that this graded normal system has an obvious interest since it allows to treat modalities to traditional mathematical concepts as finite and infinite.

The article discusses a structure theorem for free temporal algebras. It analyzes an algebraic version for temporal algebras of the logical filtrations for temporal and modal logics. It mentions the connection of temporal logic with some areas of computer science. It explains the method of filtrations which is the standard method introduced by E. J. Lemmon and K. Segerberger for Modal Logic to prove has the finite model property (f.m.p.).

The article discusses the all finitely axiomatizable normal modal logics containing K4.3. It notes on the classes of finite frames and the application of Harropstyle argument. It mentions the chains of clusters with irreflexive points as well as the constitution of Noetherian refutation frames. It tackles the decidability result of all finitely axiomatizable logics.

The article discusses the topological model theory and evaluates topological modal logic. It tackles the relationship between neighbourhood and Kripke semantics. It also evaluates the classical correspondence theory and notes on the application of topological model theory to interpolation in modal logic.

The article presents a variety of modal logics that are based on the relevant logic represented by the variable R. The author notes that all modal logics created has proven that each logic is a conservative extension of its classical logic counterpart. He mentions adding several modal principles including Brouwersche System (Br), S4, and S5 modal logics.

The article presents a Gentzen-like calculi for normal modal logics based on modal sequents and a cut elimination theorem for the minimal modal system K. The Hilbert-style theorems are used in proving the calculus of modal sequents. Modal rules called K-rules are introduced to develop the calculus and by adding such rule to the logical, structural and duality rules, the sequent calculus can be obtained. The duality rule is proved through the cut formula.

The article focuses on the formalization of Sambin's normalization of theorem for GL, the modal logic of provability. As Sambin's proof is a decision procedure, it is formalized as a recursive function and the recursiveness is proved in an arithmetically formalizable way. It is found that the normalization of GL can be formalized in Peano Arithmetic (PA).

The article discusses a study regarding the properties of the proofs in PRA of provability logic. The study involved normal form theorem in order to obtain syntactical results of the PRA-completeness of modal logic and completeness theorem for Boolean functions. Results show that it is possible to split the proof-trees of provability logic sequents.

The article discusses the inadequate relational semantic for the until operator. It states that the consideration of modal logics with the binary operator Until has shown that the continuum of consistent U-logics without Kripke frames exists and each U-logic whose class of order does not contain the finite frame property. It says that the logics with binary operators Until and Since (US-logics) is complete in terms of its class of US-general frames.

The article discusses the aspects of modal logics with n-ary connectives and binary operators in relation to the principles of mathematical logic. The authors look into modal logics and related Kripke-style semantics, in their attempt to approach the subject in a unitary point of view. They also show results for multipreopder logic, as well as distributive linear logic.

The article offers information on modal set theory, formalized in modal logic, and its consequences in relation to its simple axiomatization. It states that for formalizing the modal operator, usual classical set-theoretical language is extended with the help of new unary logical connective, which should be an epistemic modality, and the language is the modal predicate calculus with identity.

The article discusses the axiomatization of matrices. It proves the mathematical theorem of the axiomatization of matrices through formulas of the Hilbert calculus, substitution, and modus ponens. It also cites the theorems of about congruences for finite, intermediate, and modal logics as well as the intuitionistic propositional logic in the set of connectives.

The article offers information on modal logic as an important tool in the fields of the Computer Science and Artificial Intelligence. It mentions that modal logic is used in the processing of natural language, programming languages and information retrieval. It presents information on the semantic version of the Herbrand's theorem which is one of the simplest modal systems.

The article focuses on the description and usage of finite model property and semicomplemented lattices. It states that the finite model property and semicomplemented lattices are known to be a Boolean complementation in operation. It also says that semicomplemented lattices can be taken as algebraic models for standard system and through Makinson's strategy, it found that certain system of modal logic lacked the finite model property.

The article offers information about the theory and foundation the modal logic Grz. It mentions that the formulation of Grz, the authors consider to obtain by adding to classical propositional logic (PC) the modal rules concerning the antecedent GRZa and in the consequent GRZc. Moreover, it notes that a path in P is called A-explicit if its first sequent is A+ of A.

The article offers information on the study to determine the number of non-equivalent modalities in the different modal systems. It mentions that semantic test help in determining the number and the chart of the non-equivalent irreducible modalities. It offers information on Kripke model with formula and propositional variable.

The article discusses a study on the atoms in the equational class of boolean algebras' subvarieties. It analyzes an open problem regarding α-atomicity's sufficient and necessary conditions for the extension of least normal modal logic. It also investigates the α-atomicity of equational class of boolean algebras' extensions, which do not have finite model property.

The article focuses on the role of modal logics in the theory related to information systems. It mentions that the information system is the field of computer science helps in the representation, manipulation, and acquisition of information related to computer applications. It offers information on variables that represents the set of attributes.

The article discusses the modal logic in finite model property. It describes the modal logic as a class of formulas that contains all classical tautologies and closed under the rule of substitution and material detachment. It also explains the property of sentential calculus which has a finite characteristic of matrix in the presence of positive integers.