Search

This paper investigates the implicative conditional, a connective intended to describe the logical behavior of an empirically defined class of natural language conditionals, also named implicative conditionals, which excludes concessive and some other conditionals. The implicative conditional strengthens the strict conditional with the possibility of the antecedent and of the contradictory of the consequent. p ⇒ q is thus defined as ¬ ◊ (p ∧ ¬ q) ∧ ◊ p ∧ ◊ ¬ q . We explore the logical properties of this conditional in a reflexive normal Kripke semantics, provide an axiomatic system and prove it to be sound and complete for our semantics. The implicative conditional validates transitivity and contraposition, which we take to be integral parts of reasoning and communication. But it only validates restricted versions of strengthening the antecedent, right weakening, simplification, and rational monotonicity. Apparent counterexamples to some of these properties are explained as due to contextual factors. Finally, the implicative conditional avoids the paradoxes of material and strict implication, and validates some connexive principles such as Aristotle's theses and weak Boethius' thesis, as well as some highly entrenched principles of conditionals, such as conjunction of consequents, disjunction of antecedents, modus ponens, cautious monotonicity and cut. [ABSTRACT FROM AUTHOR]

In a reactive Kripke model, evaluation of logical operators can cause reconfiguration of the model in which the formula is evaluated. Therefore, in reactive Kripke frames, the evaluation of a logical formula in a world depends both on the world in which the evaluation is made and on the worlds it has passed through previously. The result is an extended semantics, which can specify a class of modal logics more comprehensive than the class specified by ordinary Kripke frames. This paper introduces a metamodel for reactive Kripke frames, based on the concept of categorical sketch. We believe that the categorical sketch is an appropriate metamodel for specifying a Kripke frame model. [ABSTRACT FROM AUTHOR]

Two algebraic structures, the contrapositionally complemented Heyting algebra (ccHa) and the contrapositionally |$\vee $| complemented Heyting algebra (c |$\vee $| cHa), are studied. The salient feature of these algebras is that there are two negations, one intuitionistic and another minimal in nature, along with a condition connecting the two operators. Properties of these algebras are discussed, examples are given and comparisons are made with relevant algebras. Intuitionistic Logic with Minimal Negation (ILM) corresponding to ccHa s and its extension |${\textrm {ILM}}$| - |${\vee }$| for c |$\vee $| cHa s are then investigated. Besides its relations with intuitionistic and minimal logics, ILM is observed to be related to Peirce's logic and Vakarelov's logic MIN. With a focus on properties of the two negations, relational semantics for ILM and |${\textrm {ILM}}$| - |${\vee }$| are obtained with respect to four classes of frames, and inter-translations between the classes preserving truth and validity are provided. ILM and |${\textrm {ILM}}$| - |${\vee }$| are shown to have the finite model property with respect to these classes of frames and proved to be decidable. Extracting features of the two negations in the algebras, a further investigation is made, following logical studies of negations that define the operators independently of the binary operator of implication. Using Dunn's logical framework for the purpose, two logics |$K_{im}$| and |$K_{im-{\vee }}$| are discussed, where the language does not include implication. The |$K_{im}$| -algebras are reducts of ccHa s and are different from relevant algebraic structures having two negations. The negations in the |$K_{im}$| -algebras and |$K_{im-{\vee }}$| -algebras are shown to occupy distinct positions in an enhanced form of Dunn's kite of negations. Relational semantics for |$K_{im}$| and |$K_{im-{\vee }}$| is provided by a class of frames that are based on Dunn's compatibility frames. It is observed that this class coincides with one of the four classes giving the relational semantics for ILM and |${\textrm {ILM}}$| - |${\vee }$|⁠. [ABSTRACT FROM AUTHOR]

Lie between classical logic and Brouwer-Heyting intuitionistic logic proposed in the first third of Rewriting logic is both a logical framework where many logics can be naturally represented and a Represented in the rewriting logic framework symbolic methods are of great importance. Is however limited to finitary logics, i.e. logics with Hilbert-style axiomatization using finitary rules Besides the better-known Nelson's logic and paraconsistent Nelson's logic, in 'Negation and. [Extracted from the article]

We study basic propositional logic |$\operatorname{\textbf{(BPC)}}$| augmented with the law of the weak excluded middle |$\operatorname{\textbf{(WEM)}}$|⁠, i.e. |$\operatorname{\textbf{BPW}} = \operatorname{\textbf{BPC}} + \operatorname{\textbf{WEM}}$|⁠. We show that the variety of the algebraic models of |$\operatorname{\textbf{BPW}}$| is canonical, and its Kripke completeness is proved via cononicity. Moreover, it is also proved that |$\operatorname{\textbf{BPW}}$| has the finite model property and is decidable. It is shown that |$\operatorname{\textbf{BPC}}$| and |$\operatorname{\textbf{BPW}}$| have the same behaviour on the |$\bot $| -free formulas and that |$\operatorname{\textbf{CPC}}$| and |$\operatorname{\textbf{BPW}}$| have the same behaviour on the negated formulas. [ABSTRACT FROM AUTHOR]

We can look at a first-order (or propositional) intuitionistic Kripke model as an ordered set of classical models. In this paper, we show that for a finite-depth Kripke model in an arbitrary first-order language or propositional language, local (classical) truth of a formula is equivalent to non-classical truth (truth in the Kripke semantics) of a Friedman's translation of that formula, i.e. |$ \alpha \Vdash A^\rho \Leftrightarrow \mathfrak{M}_\alpha \models A$|⁠. We introduce some applications of this fact. We extend the result of Ardeshir and Hesaam (2002, Math. Logic Quart. 48, 391–395) and show that semi-narrow Kripke models of Heyting Arithmetic |$ \textsf{HA} $| are locally |$ \textsf{PA} $|⁠. [ABSTRACT FROM AUTHOR]

ONNILLI-formulas were introduced in [2] and were shown to be the set of formulas that are preserved under monotonic images of descriptive or Kripke frames. As a result, ONNILLI is a syntactically defined set of formulas that axiomatize all stable logics. In this paper, among other things, by proving the uniform interpolation property for ONNILLI we show that ONNILLI is exactly the set of formulas that are preserved in monotonic bijections of descriptive or (finite) Kripke models. This resolves an open problem in [2]. [ABSTRACT FROM AUTHOR]

The best we can do is appeal to a set HT ht , the I worlds i of the context. HT ht But perhaps my reasoning was specious on metaphysical grounds - that is, from the very opening move according to which we should see context as selecting a mere set HT ht of candidates for actuality. "Julius" expresses a "cheesy mode of presentation" (Dorr et al., [9]) of one of the available acts HT ht in Figure. Free Choice is provable in this framework given that each embedded disjunct of e.g. (4a) is HT ht -accessible to the agent ( I op. cit i ., Theorem 1). [Extracted from the article]

In two recent articles, Norihiro Kamide introduces unusual variants of Nelson's paraconsistent logic and its classical extension. Kamide's systems, IP and CP , are unusual insofar as double negations in these logics behave as intuitionistic and classical negations, respectively. In this article we present Hilbert-style axiomatizations of both IP and CP. The axiom system for IP is shown to be sound and complete with respect to a four-valued Kripke semantics, and the axiom system for CP is characterized by four-valued truth tables. Moreover, we note some properties of IP and CP , and emphasize that these logics are unusual also because they are contra-classical and inconsistent but nontrivial. We point out that Kamide's approach exemplifies a general method for obtaining contra-classical logics, and we briefly speculate about a linguistic application of Kamide's logics. [ABSTRACT FROM AUTHOR]

Kripke’s theory of truth is arguably the most influential approach to self-referential truth and the semantic paradoxes. The use of a partial evaluation scheme is crucial to the theory and the most prominent schemes that are adopted are the strong Kleene and the supervaluation scheme. The strong Kleene scheme is attractive because it ensures the compositionality of the notion of truth. But under the strong Kleene scheme classical tautologies do not, in general, turn out to be true and, as a consequence, classical reasoning is no longer admissible once the notion of truth is involved. The supervaluation scheme adheres to classical reasoning but violates compositionality. Moreover, it turns Kripke’s theory into a rather complicated affair: to check whether a sentence is true we have to look at all admissible precisification of the interpretation of the truth predicate we are presented with. One consequence of this complicated evaluation condition is that under the supervaluation scheme a more proof-theoretic characterization of Kripke’s theory becomes inherently difficult, if not impossible. In this paper we explore the middle ground between the strong Kleene and the supervaluation scheme and provide an evaluation scheme that adheres to classical reasoning but retains many of the attractive features of the strong Kleene scheme. We supplement our semantic investigation with a novel axiomatic theory of truth that matches the semantic theory we have put forth. [ABSTRACT FROM AUTHOR]

Since the advent of BAN logic, many logics have been proposed for verifying authentication protocols. In one line of research, scholars have presented logics that can be utilized in verifying timed requirements of the protocols. Although many temporal epistemic logics have been developed to this end, there is no complete logic of this kind to prevent logical omniscience. Thus, they may lead to misleading judgments about the properties of the protocol being analyzed. In this paper, we propose a complete and omniscience-free temporal epistemic logic for analyzing authentication protocols. The main challenging issue in devising this logic is formulating intuitive models that on one hand reflect what is naturally meant by a protocol execution and on the other hand make it possible to achieve properties such as completeness. We show that such models can build on interpreted systems and that the resulting logic is useful in analyzing authentication protocols. [ABSTRACT FROM AUTHOR]

Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic called ILGL that gives an account of layering. The logic is a bunched system, combining the usual intuitionistic connectives, together with a non-commutative, non-associative conjunction (used to capture layering) and its associated implications. We give soundness and completeness theorems for a labelled tableaux system with respect to a Kripke semantics on graphs. We then give an equivalent relational semantics, itself proven equivalent to an algebraic semantics via a representation theorem. We utilise this result in two ways. First, we prove decidability of the logic by showing the finite embeddability property holds for the algebraic semantics. Second, we prove a Stone-type duality theorem for the logic. By introducing the notions of ILGL hyperdoctrine and indexed layered frame we are able to extend this result to a predicate version of the logic and prove soundness and completeness theorems for an extension of the layered graph semantics. We indicate the utility of predicate ILGL with a resource-labelled bigraph model. [ABSTRACT FROM AUTHOR]

Kripke frames (and models) provide a suitable semantics for sub-classical logics; for example, intuitionistic logic (of Brouwer and Heyting) axiomatizes the reflexive and transitive Kripke frames (with persistent satisfaction relations), and the basic logic (of Visser) axiomatizes transitive Kripke frames (with persistent satisfaction relations). Here, we investigate whether Kripke frames/models could provide a semantics for fuzzy logics. For each axiom of the basic fuzzy logic, necessary and sufficient conditions are sought for Kripke frames/models which satisfy them. It turns out that the only fuzzy logics (logics containing the basic fuzzy logic) which are sound and complete with respect to a class of Kripke frames/models are the extensions of the Gödel logic (or the super-intuitionistic logic of Dummett); indeed this logic is sound and strongly complete with respect to reflexive, transitive and connected (linear) Kripke frames (with persistent satisfaction relations). This provides a semantic characterization for the Gödel logic among (propositional) fuzzy logics. [ABSTRACT FROM AUTHOR]

Positive modal logic, as introduced by Dunn in 1995, is the negation-free fragment of the standard modal logic of all Kripke frames. Positive coalgebraic logic, introduced by the authors in a previous work, expands the above result from Kripke frames to more general transition systems, namely to coalgebras of weak-pullback preserving functors. We show that this construction is both modular and uniform in the functor giving the type of coalgebra. More precisely, we formalize both Set and Pos-based coalgebraic modal logic as institutions, and we exhibit a morphism of institutions between them giving the positive fragment of coalgebraic modal logic. [ABSTRACT FROM AUTHOR]

We give a separable axiomatization of the Gabbay-de Jongh logic which is different from the Gabbay and de Jongh's one by using an algebraic method with Jankov's characteristic formula (Jankov, 1969, USSR-Izvestiya, 3 17-35). We also show that a variant of the Gabbay and de Jongh's well-known axiomatization is not separable. [ABSTRACT FROM AUTHOR]

A system WF of subintuitionistic logic is introduced, weaker than Corsi's basic subintuitionistic system F. A derivation system with and without hypotheses is given in line with the authors' derivation system for F. A neighbourhood semantics is introduced with a somewhat more complex definition than the neighbourhood semantics for non-normal modal logics. Completeness is proved for WF with respect to this neighbourhood semantics, and similarly for some logics between WF and F which characterize nice frame classes. The study by the authors of the conservativity of IPC over F with respect to some classes of implications is extended to WF, and shows clearly the difference in strength between the two logics. Study of translations of these weak subintuitionistic logics into non-normal modal logics turned out to be hard because of the difference between their respective neighbourhood structures and leaves us with some open problems. [ABSTRACT FROM AUTHOR]

We show that logics based on linear Kripke frames-with or without constant domains-that have a scattered end piece are not recursively enumerable. This is done by reduction to validity in all finite classical models. [ABSTRACT FROM AUTHOR]

Minimal logic, i.e., intuitionistic logic without the ex falso principle, is investigated in its original form with a negation symbol instead of a symbol denoting the contradiction. A Kripke semantics is developed for minimal logic and its sublogics with a still weaker negation by introducing a function on the upward closed sets of the models. The basic logic is a logic in which the negation has no properties but the one of being a unary operator. A number of extensions is studied of which the most important ones are contraposition logic and negative ex falso, a weak form of the ex falso principle. Completeness is proved, and the created semantics is further studied. The negative translation of classical logic into intuitionistic logic is made part of a chain of translations by introducing translations from minimal logic into contraposition logic and intuitionistic logic into minimal logic, the latter having been discovered in the correspondence between Johansson and Heyting. Finally, as a bridge to the work of Franco Montagna a start is made of a study of linear models of these logics. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

This paper introduces a generalized version of inquisitive semantics, denoted as GIS, and concentrates especially on the role of disjunction in this general framework. Two alternative semantic conditions for disjunction are compared: the first one corresponds to the so-called tensor operator of dependence logic, and the second one is the standard condition for inquisitive disjunction. It is shown that GIS is intimately related to intuitionistic logic and its Kripke semantics. Using this framework, it is shown that the main results concerning inquisitive semantics, especially the axiomatization of inquisitive logic, can be viewed as particular cases of more general phenomena. In this connection, a class of non-standard superintuitionistic logics is introduced and studied. These logics share many interesting features with inquisitive logic, which is the strongest logic of this class. [ABSTRACT FROM AUTHOR]

We present a Kripke logical relation for showing the correctness of program transformations based on a region-polymorphic type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation. We also show how to use our model to verify a number of interesting program transformations that rely on effect annotations. In building the model, we extend earlier work by Benton et al. that treated, respectively dynamically allocated first-order references, and higher-order store for global variables. We utilize ideas from region-based memory management, and on Kripke logical relations for higher-order store. One of the key challenges that we overcome in the construction of the model is treatment of masking of regions (conceptually similar to deallocation). Our approach bears similarities to the one used in Ahmed's unary model of a region calculus in her Ph.D. thesis. [ABSTRACT FROM AUTHOR]

The Craig interpolation property and interpolation property for deducibility are considered for special kind of normal extensions of the Brouwer logic. [ABSTRACT FROM AUTHOR]

We consider the language with temporal operators G, H and coderivative operator [d]. G means 'always in the future', H means 'always in the past' and [d] means 'around now but possibly not now'. We finitely axiomatize the logic of this language interpreted over the real line, we prove that this logic is PSPACE-complete, and that it is neither strongly complete nor Kripke-complete (and consequently that it fails the finite model property). [ABSTRACT FROM AUTHOR]

This paper is devoted to study of the logic corresponding to intervals of the real line, where the modality is interpreted as 'after.' Since this logic is finitely axiomatizable, the proof of the finite model property given in the paper implies its decidability. Also, a description of the class of finite rooted Kripke frames corresponding to this logic is provided. [ABSTRACT FROM AUTHOR]

We present Dynamic Epistemic Temporal Logic, a framework for reasoning about operations on multi-agent Kripke models that contain a designated temporal relation. These operations are natural extensions of the well-known 'action models' from Dynamic Epistemic Logic (DEL). Our 'temporal action models' may be used to define a number of informational actions that can modify the 'objective' temporal structure of a model along with the agents' basic and higher-order knowledge and beliefs about this structure, including their beliefs about the time. In essence, this approach provides one way to extend the domain of action model-style operations from atemporal Kripke models to temporal Kripke models in a manner that allows actions to control the flow of time. We present a number of examples to illustrate the subtleties involved in interpreting the effects of our extended action models on temporal Kripke models. We also study preservation of important epistemic-temporal properties of temporal Kripke models under temporal action model-induced operations, provide complete axiomatizations for two theories of temporal action models, and connect our approach with previous work on time in DEL. [ABSTRACT FROM AUTHOR]

Kripke's notion of groundedness plays a central role in many responses to the semantic paradoxes. Can the notion of groundedness be brought to bear on the paradoxes that arise in connection with abstraction principles? We explore a version of grounded abstraction whereby term models are built up in a 'grounded' manner. The results are mixed. Our method solves a problem concerning circularity and yields a 'grounded' model for the predicative theory based on Frege's Basic Law V. However, the method is poorly behaved unless the background second-order logic is predicative. [ABSTRACT FROM AUTHOR]

Primal infon logic (PIL) was introduced in 2009 in the framework of policy and trust management. In the meantime, some generalizations appeared, and there have been some changes in the syntax of the basic PIL. This article is on the basic PIL, and one of our purposes is to 'institutionalize' the changes.We prove a small-model theorem for the propositional fragment of basic primal infon logic (PPIL), give a simple proof of the PPIL locality theorem and present a linear-time decision algorithm (announced earlier) for PPIL in a form convenient for generalizations. For the sake of completeness, we cover the universal fragment of basic PIL. We wish that this article becomes a standard reference on basic PIL. [ABSTRACT FROM AUTHOR]

In this work, we combine features from Justification Logics and Logics of Plausibility-Based Beliefs to build a logic for Multi-Agent Systems where each agent can explicitly state his justification for believing in a given sentence. Our logic is a normal modal logic based on the standard Kripke semantics, where we provide a semantic definition for the evidence terms and define the notion of plausible evidence for an agent, based on plausibility relations in the model. As we deal with beliefs, justifications can be faulty and unreliable. In our logic, agents can disagree not only over whether a sentence is true or false, but also on whether some evidence is a valid justification for a sentence or not. After defining our logic and its semantics, we provide a strongly complete axiomatic system for it, show that it has the finite model property, analyze the complexity of its Model-Checking Problem and show that its Satisfiability Problem has the same complexity as the one from basic modal logics. Thus, this logic seems to be a good first step for the development of a dynamic logic that can model the processes of argumentation and debate in Multi-Agent Systems. [ABSTRACT FROM AUTHOR]

There are several ways to define the notion of submodel for Kripke models of intuitionistic first-order logic. In our approach, a Kripke model A is a submodel of a Kripke model B if the frame of A is a subframe of the frame of B and for each two corresponding worlds Aa and Ba of them, Aa is a classical submodel of Ba. In this case, B is called an extension of A. We characterize formulas that are preserved under taking extensions of Kripke models. [ABSTRACT FROM AUTHOR]

This article presents modal versions of resource-conscious logics. We concentrate on extensions of variants of linear logic with one minimal non-normal modality. In earlier work, where we investigated agency in multi-agent systems, we have shown that the results scale up to logics with multiple non-minimal modalities. Here, we start with the language of propositional intuitionistic linear logic without the additive disjunction, to which we add a modality. We provide an interpretation of this language on a class of Kripke resource models extended with a neighbourhood function: modal Kripke resource models. We propose a Hilbert-style axiomatisation and a Gentzen-style sequent calculus. We show that the proof theories are sound and complete with respect to the class of modal Kripke resource models. We show that the sequent calculus admits cut elimination and that proof-search is in PSPACE. We then show how to extend the results when non-commutative connectives are added to the language. Finally, we put the logical framework to use by instantiating it as logics of agency. In particular, we propose a logic to reason about the resource-sensitive use of artefacts and illustrate it with a variety of examples. [ABSTRACT FROM PUBLISHER]

Motivated from reasoning in rough set theory, we have introduced and studied proof-theoretic properties of a class of logics L(T,I) in the first part of this article. These are logics with models based on 'dynamic I spaces', which are finite sequences of Kripke I frames with a common domain, I being any of the normal modal systems K, K4, T, B, S4, KTB, KB4, S5. This article presents the second part of the study on L(T,I), where we focus on decidability issues. [ABSTRACT FROM AUTHOR]

We study the expressive power of fragments of inclusion and independence logic defined by restricting the number k of universal quantifiers in formulas. Assuming the so-called strict semantics for these logics, we relate these fragments of inclusion and independence logic to sublogics ESOf (k∀) of existential second-order logic, which in turn are known to capture the complexity classes NTIMERAM(nk). [ABSTRACT FROM AUTHOR]

We consider intermediate predicate logics defined by fixed well-ordered (or dually well-ordered) linear Kripke frames with constant domains where the order-type of the well-order is strictly smaller than ωω. We show that two such logics of different order-type are separated by a first-order sentence using only one monadic predicate symbol. Previous results by Minari, Takano and Ono, as well as the second author, obtained the same separation but relied on the use of predicate symbols of unbounded arity. [ABSTRACT FROM AUTHOR]

We consider the Gödel bi-modal logic determined by fuzzy Kripke models where both the propositions and the accessibility relation are infinitely valued over the standard Gödel algebra [0,1], and prove strong completeness of the Fischer Servi intuitionistic modal logic IK plus the prelinearity axiom with respect to this semantics. We axiomatize also the bi-modal analogues of classical T, S4 and S5, obtained by restricting to models over frames satisfying the [0,1]-valued versions of the structural properties which characterize these logics. As an application of the completeness theorems we obtain a representation theorem for bi-modal Gödel algebras. [ABSTRACT FROM AUTHOR]

In Kripke’s classic paper on truth it is argued that by adding a new semantic category different from truth and falsity it is possible to have a language with its own truth predicate. A substantial problem with this approach is that it lacks the expressive resources to characterize those sentences which fall under the new category. The main goal of this paper is to offer a refinement of Kripke’s approach in which this difficulty does not arise. We tackle this characterization problem by letting certain sentences belong to more than one semantic category. We also consider the prospect of generalizing this framework to deal with languages containing vague predicates. [ABSTRACT FROM AUTHOR]

Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics. corresponding to different continuity principles. They form a natural implicational hierarchy. Some of the implications have been shown to be strict, others strict in a weak context, and yet others not at all, using disparate techniques. Here we present a family of related Kripke models which separates all of the as yet identified fan theorems. [ABSTRACT FROM AUTHOR]