共查询到20条相似文献，搜索用时 187 毫秒
1.
This is an investigation of the implications of IPC which remain provable when one weakens intuitionistic logic in various ways. The research is concerned with logics with Kripke models as introduced by G. Corsi in 1987, and others like G. Restall, Do?en, Visser. This leads to conservativity results for IPC with regard to classes of implications in some of these logics. Moreover, similar results are reached for some weaker subintuitionistic systems with neighborhood models introduced by the authors in 2016. In addition, the relationship between two types of neighborhood models introduced in that work is clarified. This clarification leads also to modal companions for weaker logics. 相似文献
2.
Guido Bertolotti Pierangelo Miglioli Daniela Silvestrini 《Mathematical Logic Quarterly》1996,42(1):501-536
We provide results allowing to state, by the simple inspection of suitable classes of posets (propositional Kripke frames), that the corresponding intermediate propositional logics are maximal among the ones which satisfy the disjunction property. Starting from these results, we directly exhibit, without using the axiom of choice, the Kripke frames semantics of 2No maximal intermediate propositional logics with the disjunction property. This improves previous evaluations, giving rise to the same conclusion but made with an essential use of the axiom of choice, of the cardinality of the set of the maximal intermediate propositional logics with the disjunction property. Mathematics Subject Classification: 03B55, 03C90. 相似文献
3.
Kosta Do&#x;en 《Mathematical Logic Quarterly》1992,38(1):179-187
Models for the Lambek calculus of syntactic categories surveyed here are based on frames that are in principle of the same type as Kripke frames for intuitionistic logic. These models are extracted from the literature on models for relevant logics, in particular the ternary relationed models introduced in the early seventies. The purpose of this brief survey is to locate some open completeness problems for variants of the Lambek calculus in the context of completeness results based on various types of ternary relational models. 相似文献
4.
5.
Norihiro Kamide 《Mathematical Logic Quarterly》2005,51(4):331-341
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) 相似文献
6.
The decision problem for provability logic remains PSPACE-complete even if the number of propositional atoms is restricted to one.
This paper was supported by grant 401/01/0218 of the Grant Agency of the Czech Republic. 相似文献
7.
扰动模糊命题逻辑的代数结构及其广义重言式性质 总被引：4，自引：1，他引：4
着眼于扰动模糊命题逻辑的代数结构,为研究二维扰动模糊命题逻辑最大子代数I2R及其广义重言式提供了一些代数理论基础,最后研究了子代数间广义重言式的关系. 相似文献
8.
本文基于中介命题逻辑的扩张系统 MP*之命题联结词含量的完全性结果 ,进一步证明了 Lukasiwicz三值逻辑系统 L*3 、Post三值逻辑系统 P*3 、Slupecki三值逻辑系统 S*3 和 Woodruff三值逻辑系统 W*3 等的命题联结词的含量也是完全的 .从而着眼于形式系统 ,可知 MP*、L*3 、P*3 、S*3 、W*3 的语言表达的能力也都是等效的 .又若这些三值系统都是可靠的完备的 ,则可进一步证明这些三值系统立足于形式推理也都是互相等价的 . 相似文献
9.
10.
Ben Ellison Jonathan Fleischmann Dan McGinn Wim Ruitenburg 《Mathematical Logic Quarterly》2007,53(3):311-320
We define two notions for intuitionistic predicate logic: that of a submodel of a Kripke model, and that of a universal sentence. We then prove a corresponding preservation theorem. If a Kripke model is viewed as a functor from a small category to the category of all classical models with (homo)morphisms between them, then we define a submodel of a Kripke model to be a restriction of the original Kripke model to a subcategory of its domain, where every node in the subcategory is mapped to a classical submodel of the corresponding classical model in the range of the original Kripke model. We call a sentence universal if it is built inductively from atoms (including ? and ⊥) using ∧, ∨, ?, and →, with the restriction that antecedents of → must be atomic. We prove that an intuitionistic theory is axiomatized by universal sentences if and only if it is preserved under Kripke submodels. We also prove the following analogue of a classical model‐consistency theorem: The universal fragment of a theory Γ is contained in the universal fragment of a theory Δ if and only if every rooted Kripke model of Δ is strongly equivalent to a submodel of a rooted Kripke model of Γ. Our notions of Kripke submodel and universal sentence are natural in the sense that in the presence of the rule of excluded middle, they collapse to the classical notions of submodel and universal sentence. (© 2007 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim) 相似文献
11.
Modal logics with the binary operator Until are considered. It is shown that there exists a continuum of consistent U-logics without Kripke frames, and that each U-logic whose class of order does not have the finite frame property. 相似文献
12.
We present an alternative, purely semantical and relatively simple, proof of the Statman's result that both intuitionistic propositional logic and its implicational fragment are PSPACE-complete.This paper was supported by grant 401/01/0218 of the Grant Agency of the Czech Republic. %
Mathematics Subject Classification (2000): 相似文献
13.
Giacomo Bonanno 《Mathematical Logic Quarterly》1996,42(1):305-311
We investigate an axiomatization of the notion of common belief (knowledge) that makes use of no rules of inference (apart from Modus Ponens and Necessitation) and highlight the property of the set of accessibility relations that characterizes each axiom. Mathematics Subject Classification: 03B45, 68T25. 相似文献
14.
15.
Olivier Gasquet 《Mathematical Logic Quarterly》1998,44(1):45-49
The problem of completeness for predicate modal logics is still under investigation, although some results have been obtained in the last few years (cf. [2, 3, 4, 7]). As far as we know, the case of multimodal logics has not been addressed at all. In this paper, we study the combination of modal logics in terms of combining their semantics. We demonstrate by a simple example that in this sense predicate modal logics are not so easily manipulated as propositional ones: mixing two Kripke-complete predicate modal logics (one with the Barcan formula, and the other without) results in a Kripke-incomplete system. 相似文献
16.
Morteza Moniri 《Mathematical Logic Quarterly》2002,48(1):157-160
In the first section of this paper we show that i Π1 ≡ W⌝⌝lΠ1 and that a Kripke model which decides bounded formulas forces iΠ1 if and only if the union of the worlds in any (complete) path in it satisflies IΠ1. In particular, the union of the worlds in any path of a Kripke model of HA models IΠ1. In the second section of the paper, we show that for equivalence of forcing and satisfaction of Πm‐formulas in a linear Kripke model deciding Δ0‐formulas it is necessary and sufficient that the model be Σm‐elementary. This implies that if a linear Kripke model forces PEMprenex, then it forces PEM. We also show that, for each n ≥ 1, iΦn does not prove ℋ︁(IΠn's are Burr's fragments of HA. 相似文献
17.
We consider the problem of finding, in the ambit of modal logic, a minimal characterization for finite Kripke frames, i.e., a formula which, given a frame, axiomatizes its theory employing the lowest possible number of variables and implies the other axiomatizations. We show that every finite transitive frame admits a minimal characterization over K4, and that this result can not be extended to K. 相似文献
18.
Is it possible to give an abstract characterisation of constructive real numbers? A condition should be that all axioms are valid for Dedekind reals in any topos, or for constructive reals in Bishop mathematics. We present here a possible first‐order axiomatisation of real numbers, which becomes complete if one adds the law of excluded middle. As an application of the forcing relation defined in [3, 2], we give a proof that the formula which specifies the maximum function is not provable in this theory. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim) 相似文献
19.
R. Alonderis 《Lithuanian Mathematical Journal》2008,48(2):123-136
The paper deals with a coding method for a sequent calculus of the propositional logic. The method is based on the sequent calculus. It allows us to determine if a formula is derivable in the calculus without constructing a derivation tree. The main advantage of the coding method is its compactness in comparison with derivation trees of the sequent calculus. The coding method can be used as a decision procedure for the propositional logic. 相似文献
20.