排序方式: 共有34条查询结果,搜索用时 15 毫秒
11.
The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL
ew
of the substructural logic FL
ew
. The main result of Part I of this series [41] shows that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL
ew
(namely, a certain variety of FL
ew
-algebras) are term equivalent. In this paper, the term equivalence result of Part I [41] is lifted to the setting of deductive
systems to establish the definitional equivalence of the logics N and NFL
ew
. It follows from the definitional equivalence of these systems that constructive logic with strong negation is a substructural
logic.
Presented by Heinrich Wansing 相似文献
12.
We prove that all semisimple varieties of FL
ew-algebras are discriminator varieties. A characterisation of discriminator and EDPC varieties of FL
ew-algebras follows. It matches exactly a natural classification of logics over FL
ew proposed by H. Ono. 相似文献
13.
We consider various classes of algebras obtained by expanding idempotent semirings with meet, residuals and Kleene-*. An investigation of congruence properties (e-permutability, e-regularity, congruence distributivity) is followed by a section on algebraic Gentzen systems for proving inequalities in idempotent semirings, in residuated lattices, and in (residuated) Kleene lattices (with cut). Finally we define (one-sorted) residuated Kleene lattices with tests to complement two-sorted Kleene algebras with tests. 相似文献
14.
The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL
ew
of the substructural logic FL
ew
. In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL
ew
(namely, a certain variety of FL
ew
-algebras) are term equivalent. This answers a longstanding question of Nelson [30]. Extensive use is made of the automated
theorem-prover Prover9 in order to establish the result.
The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL
ew
are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL
ew
.
Presented by Heinrich Wansing 相似文献
15.
Algebraic Aspects of Cut Elimination 总被引:2,自引:2,他引:0
We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille completion. Moreover, the finite model property is obtained for many cases, by modifying our completeness proof. This is an algebraic presentation of the proof of the finite model property discussed by Lafont [12] and Okada-Terui [17]. 相似文献
16.
Substructural logics have received a lot of attention in recent years from the communities of both logic and algebra. We discuss
the algebraization of substructural logics over the full Lambek calculus and their connections to residuated lattices, and
establish a weak form of the deduction theorem that is known as parametrized local deduction theorem. Finally, we study certain
interpolation properties and explain how they imply the amalgamation property for certain varieties of residuated lattices.
Dedicated to the memory of Willem Johannes Blok 相似文献
17.
Minimal Varieties of Involutive Residuated Lattices 总被引:1,自引:0,他引:1
We establish the existence uncountably many atoms in the subvariety lattice of the variety of involutive residuated lattices.
The proof utilizes a construction used in the proof of the corresponding result for residuated lattices and is based on the
fact that every residuated lattice with greatest element can be associated in a canonical way with an involutive residuated
lattice.
Dedicated to the memory of Willem Johannes Blok 相似文献
18.
The main goal of this paper is to explain the link between the algebraic models and the Kripke-style models for certain classes of propositional non-classical logics. We consider logics that are sound and complete with respect to varieties of distributive lattices with certain classes of well-behaved operators for which a Priestley-style duality holds, and present a way of constructing topological and non-topological Kripke-style models for these types of logics. Moreover, we show that, under certain additional assumptions on the variety of the algerabic models of the given logics, soundness and completeness with respect to these classes of Kripke-style models follows by using entirely algebraical arguments from the soundness and completeness of the logic with respect to its algebraic models. 相似文献
19.
A full separation theorem for the derivable rules of intuitionistic linear logic without bounds, 0 and exponentials is proved. Several structural consequences of this theorem for subreducts of (commutative) residuated lattices are obtained. The theorem is then extended to the logic LR
+ and its proof is extended to obtain the finite embeddability property for the class of square increasing residuated lattices. 相似文献
20.
Let
be a finite collection of finite algebras of finite signature such that SP(
) has meet semi-distributive congruence lattices. We prove that there exists a finite collection
1 of finite algebras of the same signature,
, such that SP(
1) is finitely axiomatizable.We show also that if
, then SP(
1) is finitely axiomatizable. We offer new proofs of two important finite basis theorems of D. Pigozzi and R. Willard. Our actual results are somewhat more general than this abstract indicates.While working on this paper, the first author was partially supported by the Hungarian National Foundation for Scientific Research (OTKA) grant no. T37877 and the second author was supported by the US National Science Foundation grant no. DMS-0245622.Special issue of Studia Logica: Algebraic Theory of Quasivarieties Presented by
M. E. Adams, K. V. Adaricheva, W. Dziobiak, and A. V. Kravchenko 相似文献