A Heyting algebra is supplemented if each element a has a dual pseudo-complement \, and a Heyting algebra is centrally supplement if it is supplemented and each supplement is central. We show that each Heyting algebra has a centrally supplemented extension in the same variety of Heyting algebras as the original. We use this tool to investigate a new type of completion of Heyting algebras arising in the context of algebraic proof theory, the so-called hyper-MacNeille completion. We show that the (...) hyper-MacNeille completion of a Heyting algebra is the MacNeille completion of its centrally supplemented extension. This provides an algebraic description of the hyper-MacNeille completion of a Heyting algebra, allows development of further properties of the hyper-MacNeille completion, and provides new examples of varieties of Heyting algebras that are closed under hyper-MacNeille completions. In particular, connections between the centrally supplemented extension and Boolean products allow us to show that any finitely generated variety of Heyting algebras is closed under hyper-MacNeille completions. (shrink)

We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on substructural logics over the full Lambek Calculus [34], Galatos and Ono [18], Galatos et al. [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show that the logic associated (...) with and is algebraizable, with the variety of residuated lattice-ordered groupoids with unit serving as its equivalent algebraic semantics. Overcoming technical complications arising from the lack of associativity, we introduce a generalized version of a logical matrix and apply the method of quasicompletions to obtain an algebra and a quasiembedding from the matrix to the algebra. By applying the general result to specific cases, we obtain important logical and algebraic properties, including the cut elimination of and various extensions, the strong separation of , and the finite generation of the variety of residuated lattice-ordered groupoids with unit. (shrink)

Grishin algebras are a generalisation of Boolean algebras that provide algebraic models for classical bilinear logic with two mutually cancelling negation connectives. We show how to build complete Grishin algebras as algebras of certain subsets (“propositions”) of cover systems that use an orthogonality relation to interpret the negations. The variety of Grishin algebras is shown to be closed under MacNeille completion, and this is applied to embed an arbitrary Grishin algebra into the algebra of all propositions of some cover system, (...) by a map that preserves all existing joins and meets. This representation is then used to give a cover system semantics for a version of classical bilinear logic that has first-order quantifiers and infinitary conjunctions and disjunctions. (shrink)

The logic of (commutative integral bounded) residuated lattices is known under different names in the literature: monoidal logic [26], intuitionistic logic without contraction [1], H BCK [36] (nowadays called by Ono), etc. In this paper we study the -fragment and the -fragment of the logical systems associated with residuated lattices, both from the perspective of Gentzen systems and from that of deductive systems. We stress that our notion of fragment considers the full consequence relation admitting hypotheses. It results that this (...) notion of fragment is axiomatized by the rules of the sequent calculus for the connectives involved. We also prove that these deductive systems are non-protoalgebraic, while the Gentzen systems are algebraizable with equivalent algebraic semantics the varieties of pseudocomplemented (commutative integral bounded) semilatticed and latticed monoids, respectively. All the logical systems considered are decidable. (shrink)

Starting from an arbitrary MTL-chain, two constructions are considered: the MacNeille completion of the underlying order with suitable extensions of the other operations, and a finite embeddability construction. The preservation of properties via these constructions is investigated, that is, if a property that holds in the initial MTL-chain also holds in the constructed MTL-chain. General syntactic descriptions are given of terms s and t for which the inequality s ≤ t is preserved.

It is proved that the variety of relevant disjunction lattices has the finite embeddability property. It follows that Avron's relevance logic RMImin has a strong form of the finite model property, so it has a solvable deducibility problem. This strengthens Avron's result that RMImin is decidable.

This paper establishes several algebraic embedding theorems, each of which asserts that a certain kind of residuated structure can be embedded into a richer one. In almost all cases, the original structure has a compatible involution, which must be preserved by the embedding. The results, in conjunction with previous findings, yield separative axiomatizations of the deducibility relations of various substructural formal systems having double negation and contraposition axioms. The separation theorems go somewhat further than earlier ones in the literature, which (...) either treated fewer subsignatures or focussed on the conservation of theorems only. (shrink)

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]. (shrink)

This paper deals with substructural nuclear (image-based) logics and their algebraic and Kripke-style semantics. More precisely, we first introduce a class of substructural logics with connective _N_ satisfying nucleus property, called here substructural _nuclear_ logics, and its subclass, called here substructural _nuclear image-based_ logics, where _N_ further satisfies homomorphic image property. We then consider their algebraic semantics together with algebraic characterizations of those logics. Finally, we introduce _operational Kripke-style_ semantics for those logics and provide two sorts of completeness results for (...) them, one of which is based on algebraic completeness for all the logics and the other of which is based on set-theoretic one for the nuclear image-based logics. (shrink)