共查询到20条相似文献,搜索用时 15 毫秒
1.
G. Mints 《Archive for Mathematical Logic》1998,37(5-6):415-425
We describe a natural deduction system NDIL for the second order intuitionistic linear logic which admits normalization and has a subformula property. NDIL is an extension of the system for !-free multiplicative linear logic constructed by the author and elaborated by A. Babaev.
Main new feature here is the treatment of the modality !. It uses a device inspired by D. Prawitz' treatment of S4 combined
with a construction introduced by the author to avoid cut-like constructions used in -elimination and global restrictions employed by Prawitz. Normal form for natural deduction is obtained by Prawitz translation
of cut-free sequent derivations.
Received: March 29, 1996 相似文献
2.
3.
Brouwer’s views on the foundations of mathematics have inspired the study of intuitionistic logic, including the study of the intuitionistic propositional calculus and its extensions. The theory of these systems has become an independent branch of logic with connections to lattice theory, topology, modal logic, and other areas. This paper aims to present a modern account of semantics for intuitionistic propositional systems. The guiding idea is that of a hierarchy of semantics, organized by increasing generality: from the least general Kripke semantics on through Beth semantics, topological semantics, Dragalin semantics, and finally to the most general algebraic semantics. While the Kripke, topological, and algebraic semantics have been extensively studied, the Beth and Dragalin semantics have received less attention. We bring Beth and Dragalin semantics to the fore, relating them to the concept of a nucleus from pointfree topology, which provides a unifying perspective on the semantic hierarchy. 相似文献
4.
5.
6.
R. Alonderis 《Archive for Mathematical Logic》2013,52(7-8):759-778
A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure. 相似文献
7.
We introduce a probabilistic extension of propositional intuitionistic logic. The logic allows making statements such as P≥sα, with the intended meaning “the probability of truthfulness of α is at least s”. We describe the corresponding class of models, which are Kripke models with a naturally arising notion of probability, and give a sound and complete infinitary axiomatic system. We prove that the logic is decidable. 相似文献
8.
9.
I. G. Simonova 《Mathematical Notes》1990,47(5):483-490
Translated from Matematicheskie Zametki, Vol. 47, No. 5, pp. 88–99, May 1990. 相似文献
10.
Norihiro Kamide 《Mathematical Logic Quarterly》2003,49(5):519-524
Dual‐intuitionistic logics are logics proposed by Czermak (1977), Goodman (1981) and Urbas (1996). It is shown in this paper that there is a correspondence between Goodman's dual‐intuitionistic logic and Nelson's constructive logic N?. 相似文献
11.
12.
We discuss a propositional logic which combines classical reasoning with constructive reasoning, i.e., intuitionistic logic augmented with a class of propositional variables for which we postulate the decidability property. We call it intuitionistic logic with classical atoms. We introduce two hypersequent calculi for this logic. Our main results presented here are cut-elimination with the subformula property for the calculi. As corollaries, we show decidability, an extended form of the disjunction property, the existence of embedding into an intuitionistic modal logic and a partial form of interpolation. 相似文献
13.
Ivan Chajda 《Central European Journal of Mathematics》2011,9(5):1185-1191
We introduce two unary operators G and H on a relatively pseudocomplemented lattice which form an algebraic axiomatization of the tense quantifiers “it is always
going to be the case that” and “it has always been the case that”. Their axiomatization is an extended version for the classical
logic and it is in accordance with these operators on many-valued Łukasiewicz logic. Finally, we get a general construction
of these tense operators on complete relatively pseudocomplemented lattice which is a power lattice via the so-called frame. 相似文献
14.
15.
16.
V. V. Rybakov 《Siberian Mathematical Journal》1991,32(2):297-308
Krasnoyarsk. Translated fromSibirskii Matematicheskii Zhurnal, Vol. 32, No. 2, pp. 140–153, March–April, 1991. 相似文献
17.
Katsumasa Ishii 《Mathematical Logic Quarterly》2018,64(3):183-184
An answer to the following question is presented: given a proof in classical propositional logic, for what small set of propositional variables p does it suffice to add all the formulae to Γ in order to intuitionistically prove A? This answer is an improvement of Ishihara's result for some cases. 相似文献
18.
Agata Ciabattoni 《Archive for Mathematical Logic》2005,44(4):435-457
We perform a proof-theoretical investigation of two modal predicate logics: global intuitionistic logic GI and global intuitionistic fuzzy logic GIF. These logics were introduced by Takeuti and Titani to formulate an intuitionistic set theory and an intuitionistic fuzzy set theory together with their metatheories. Here we define analytic Gentzen style calculi for GI and GIF. Among other things, these calculi allows one to prove Herbrands theorem for suitable fragments of GI and GIF.Work Supported by C. Bühler-Habilitations-Stipendium H191-N04, from the Austrian Science Fund (FWF). 相似文献
19.
《Indagationes Mathematicae (Proceedings)》1982,85(2):227-235
It is shown that for every formula which cannot be proved in intuitionistic predicate logic, and for every metrizable space X without isolated points one can find a sheaf model over X in which is not valid. 相似文献
20.
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): 相似文献