Related papers: On the Provability Logic of HA
In this paper, we study a new Kripke-style semantics for classical modal logic, named as provability models. We study provability models for the propositional modal logics K, K4, S4 GL, GLP and the interpretability logic ILM. Provability…
Propositional term modal logic is interpreted over Kripke structures with unboundedly many accessibility relations and hence the syntax admits variables indexing modalities and quantification over them. This logic is undecidable, and we…
The branch of provability logic investigates the provability-based behavior of the mathematical theories. In a more precise way, it studies the relation between a mathematical theory $T$ and a modal logic $L$ via the provability…
Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers \forall p, \exists p over propositions. In the context of Kripke semantics, a proposition is a subset of the worlds in a…
This paper studies the modal logical aspects of provability predicates and consistency statements for theories of arithmetic. First, we provide an overview of previous works on the correspondence between various derivability conditions for…
This paper belongs to the field of probabilistic modal logic, focusing on a comparative analysis of two distinct semantics: one rooted in Kripke semantics and the other in neighbourhood semantics. The primary distinction lies in the…
This article aims to present a neighborhood semantic for a modal logic, namely, propositional logic of the plausible. As a subnormal character modal logic, not admits a Kripke semantics. However, the authors show that this neighborhood…
The provability logic of a theory T is the set of modal formulas, which under any arithmetical realization are provable in T . We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $\Gamma$.…
The Kripke semantics of classical propositional normal modal logic is made algebraic via an embedding of Kripke structures into the larger class of pointed stably supported quantales. This algebraic semantics subsumes the traditional…
In this paper we introduce a modal theory $H_{\sigma}$, which is sound and complete for arithmetical $\Sigma$_1 substitutions in ${\bf HA}$, in other words, we will show that $H_{\sigma}$ is the $\Sigma$_1-provability logic of ${\bf HA}$.…
We consider the question of extending propositional logic to a logic of plausible reasoning, and posit four requirements that any such extension should satisfy. Each is a requirement that some property of classical propositional logic be…
For the Heyting Arithmetic HA, HA* is defined as the theory $\{A\mid {\sf HA}\vdash A^{\Box}\}$, where $A^{\Box}$ is called the box translation of $A$. We characterize the $\Sigma_1$-provability logic of HA* as a modal theory ${\sf…
Nonmonotonic logics are usually characterized by the presence of some notion of 'conditional' that fails monotonicity. Research on nonmonotonic logics is therefore largely concerned with the defeasibility of argument forms and the…
The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely…
This paper studies relative unification and admissibility in the intuitionistic logic. We generalize results of [Ghilardi, 1999; Iemhoff, 2001a] and prove them relative in NNIL(par) propositions, the class of propositions with No Nested…
We study local consequence relations in modal extensions of product logic over Kripke models with either valued (fuzzy) or crisp accessibility relations. In both settings, we consider semantics over the full class of product algebras as…
In 1933, G\"odel considered two modal approaches to describing provability. One captured formal provability and resulted in the logic GL and Solovay's Completeness Theorem. The other was based on the modal logic S4 and led to Artemov's…
In 1933, G\"odel introduced a provability interpretation of the propositional intuitionistic logic to establish a formalization for the BHK interpretation. He used the modal system, $\mathbf{S4}$, as a formalization of the intuitive concept…
Possibilistic logic, an extension of first-order logic, deals with uncertainty that can be estimated in terms of possibility and necessity measures. Syntactically, this means that a first-order formula is equipped with a possibility degree…
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…