共查询到20条相似文献,搜索用时 0 毫秒
1.
Injectives in several classes of structures associated with logic are characterized.
Among the classes considered are residuated lattices, MTL-algebras, IMTL-algebras, BL-algebras,
NM-algebras and bounded hoops. 相似文献
2.
M. Spinks 《Algebra Universalis》2004,51(2-3):125-136
We exhibit explicit ternary and quaternary deductive terms for the variety of
Nelson algebras. The results partially answer a question of Blok and Pigozzi. 相似文献
3.
Agata Ciabattoni 《Annals of Pure and Applied Logic》2012,163(3):266-290
We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.We introduce the substructural hierarchy — a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that a stronger form of cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N2 in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent calculus rules, are also provided.Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory. 相似文献
4.
M. Kapetanović 《Algebra Universalis》2007,57(1):127-129
A property is defined which generalizes both the disjunction property and the instantiation property of Horn clause theories.
A necessary and sufficient condition is given for a theory in order to have that property and examples are used to show its
applicability.
Presented by M. Valeriote.
Received July 12, 2005; accepted in final form January 6, 2006. 相似文献
5.
Thomas Vetterlein 《Algebra Universalis》2008,58(2):129-143
Weak effect algebras are based on a commutative, associative and cancellative partial addition; they are moreover endowed
with a partial order which is compatible with the addition, but in general not determined by it. Every BL-algebra, i.e. the
Lindenbaum algebra of a theory of Basic Logic, gives rise to a weak effect algebra; to this end, the monoidal operation is
restricted to a partial cancellative operation.
We examine in this paper BL-effect algebras, a subclass of the weak effect algebras which properly contains all weak effect
algebras arising from BL-algebras. We describe the structure of BL-effect algebras in detail. We thus generalise the well-known
structure theory of BL-algebras.
Namely, we show that BL-effect algebras are subdirect products of linearly ordered ones and that linearly ordered BL-effect
algebras are ordinal sums of generalised effect algebras. The latter are representable by means of linearly ordered groups.
This research was partially supported by the German Science Foundation (DFG) as part of the Collaborative Research Center
“Computational Intelligence” (SFB 531). 相似文献
6.
It is proved that in the variety of positive Sugihara monoids, every finite subdirectly irreducible algebra is a retract of
a free algebra. It follows that every quasivariety of positive Sugihara monoids is a variety, in contrast with the situation
in several neighboring varieties. This result shows that when the logic R-mingle is formulated with the Ackermann constant t, then its full negation-free fragment is hereditarily structurally complete.
Presented by R. W. Quackenbush.
Received August 28, 2005; accepted in final form July 31, 2006. 相似文献
7.
P. Jipsen 《Annals of Pure and Applied Logic》2009,161(2):228-234
It is shown that the Boolean center of complemented elements in a bounded integral residuated lattice characterizes direct decompositions. Generalizing both Boolean products and poset sums of residuated lattices, the concepts of poset product, Priestley product and Esakia product of algebras are defined and used to prove decomposition theorems for various ordered algebras. In particular, we show that FLw-algebras decompose as a poset product over any finite set of join irreducible strongly central elements, and that bounded n-potent GBL-algebras are represented as Esakia products of simple n-potent MV-algebras. 相似文献
8.
《Quaestiones Mathematicae》2013,36(1-4):69-94
ABSTRACT This paper generalizes the concept of a power alge bra to that of a power structure, and gives three application of power structures to logic. 相似文献
9.
We show that the two-sorted algebra of Booleans and naturals with conjunction, addition and inequality is not finitely based. If addition is removed, or negation is included, then the resulting algebra is finitely based.Received November 16, 2001; accepted in final form August 4, 2004. 相似文献
10.
We present a general construction of a family of ordinal sums of a sequence of structures and prove an elimination theorem for the class of ordinal sums in an expanded language. From this we deduce the decidability of the class of -ordinal sums of models of a decidable theory T. As an application of this result we prove that the theory of BL-chains is decidable.In Celebration of the Sixtieth Birthday of Ralph N. McKenzieReceived June 9, 2002; accepted in final form June 19, 2003. 相似文献
11.
Vardanyan's theorem states that the set of PA-valid principles of Quantified Modal Logic, QML, is complete Π02. We generalize this result to a wide class of theories. The crucial step in the generalization is avoiding the use of Tennenbaum's
Theorem. 相似文献
13.
We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs. 相似文献
14.
Willem Heijltjes 《Annals of Pure and Applied Logic》2010,161(11):1346-1366
Classical proof forests are a proof formalism for first-order classical logic based on Herbrand’s Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of first-order and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or ‘bureaucracy’.This paper presents classical proof forests as a graphical proof formalism and investigates the possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given.Cut-elimination, in the form of a weak normalisation theorem, is obtained using a modified version of the rewrite relation inspired by the game-theoretic interpretation of the forests. It is conjectured that the modified reduction relation is, in fact, strongly normalising. 相似文献
15.
16.
Steffen Lewitzka 《Annals of Pure and Applied Logic》2019,170(2):218-250
In previous work [15], we presented a hierarchy of classical modal systems, along with algebraic semantics, for the reasoning about intuitionistic truth, belief and knowledge. Deviating from Gödel's interpretation of IPC in S4, our modal systems contain IPC in the way established in [13]. The modal operator can be viewed as a predicate for intuitionistic truth, i.e. proof. Epistemic principles are partially adopted from Intuitionistic Epistemic Logic IEL [4]. In the present paper, we show that the S5-style systems of our hierarchy correspond to an extended Brouwer–Heyting–Kolmogorov interpretation and are complete w.r.t. a relational semantics based on intuitionistic general frames. In this sense, our S5-style logics are adequate and complete systems for the reasoning about proof combined with belief or knowledge. The proposed relational semantics is a uniform framework in which also IEL can be modeled. Verification-based intuitionistic knowledge formalized in IEL turns out to be a special case of the kind of knowledge described by our S5-style systems. 相似文献
17.
Minimal varieties of residuated lattices 总被引:2,自引:0,他引:2
Nikolaos Galatos 《Algebra Universalis》2005,52(2-3):215-239
In this paper we investigate the atomic level in the lattice of subvarieties of residuated lattices. In particular, we give infinitely many commutative atoms and construct continuum many non-commutative, representable atoms that satisfy the idempotent law; this answers Problem 8.6 of [12]. Moreover, we show that there are only two commutative idempotent atoms and only two cancellative atoms. Finally, we study the connections with the subvariety lattice of residuated bounded-lattices. We modify the construction mentioned above to obtain a continuum of idempotent, representable minimal varieties of residuated bounded-lattices and illustrate how the existing construction provides continuum many covers of the variety generated by the three-element non-integral residuated bounded-lattice.In Celebration of the Sixtieth Birthday of Ralph N. McKenzieReceived August 1, 2003; accepted in final form April 27, 2004. 相似文献
18.
Nick Bezhanishvili 《Algebra Universalis》2004,51(2-3):177-206
In [2] we investigated the lattice (Df2) of all
subvarieties of the variety Df2 of two-dimensional diagonal free
cylindric algebras. In the present paper we investigate the
lattice (CA2) of all subvarieties of the variety
CA2 of two-dimensional cylindric algebras.
We prove that the cardinality of (CA2) is that of the
continuum, give a criterion for a subvariety of CA2 to be locally
finite, and describe the only pre locally nite subvariety of CA2. We also characterize nitely generated subvarieties of CA2 by describing all
fteen pre nitely generated subvarieties of CA2. Finally, we give a
rough picture of (CA2), and investigate algebraic properties
preserved and reected by the reduct functors
. 相似文献
19.
G. Gierz 《Algebra Universalis》1996,35(4):570-576
In this paper, we show that two quasi-primal algebras are Morita equivalent if and only if their inverse semigroups of inner automorphisms are isomorphic, and if they have the same one-element subalgebras. The proof of this statement uses the representation theory of algebras by sections in sheaves.Presented by H. P. Gumm. 相似文献
20.
Let
be finite relational structure of finite type, and let CSP
denote the following decision problem: if
is a given structure of the same type as
, is there a homomorphism from
to
? To each relational structure
is associated naturally an algebra
whose structure determines the complexity of the associated decision problem. We investigate those finite algebras arising
from CSP’s of so-called bounded width, i.e., for which local consistency algorithms effectively decide the problem. We show that if a CSP has bounded width then
the variety generated by the associated algebra omits the Hobby-McKenzie types 1 and 2. This provides a method to prove that
certain CSP’s do not have bounded width. We give several applications, answering a question of Nešetřil and Zhu [26], by showing
that various graph homomorphism problems do not have bounded width. Feder and Vardi [17] have shown that every CSP is polynomial-time
equivalent to the retraction problem for a poset we call the Feder − Vardi poset of the structure. We show that, in the case where the structure has a single relation, if the retraction problem for the
Feder-Vardi poset has bounded width then the CSP for the structure also has bounded width. This is used to exhibit a finite
order-primal algebra whose variety admits type 2 but omits type 1 (provided P ≠ NP).
Presented by M. Valeriote.
Received January 8, 2005; accepted in final form April 3, 2006.
The first author’s research is supported by a grant from NSERC and the Centre de Recherches Mathématiques. The second author’s
research is supported by OTKA no. 034175 and 48809 and T 037877. Part of this research was conducted while the second author
was visiting Concordia University in Montréal and also when the first author was visiting the Bolyai Institute in Szeged.
The support of NSERC, OTKA and the Bolyai Institute is gratefully acknowledged. 相似文献