Information of Workshop

<< IS COE Project: Verifiable and Evolvable e-Society >>

COE Workshop on Logic and Algebra

26th January (Wed), 2005 JAIST, Collaboration Room No.6, IS 3rd bldg. 5th floor

Program

9:30 - 10:00 Hitoshi Kihara and Hiroakira Ono (JAIST): Notes on pseudo-relevance property of commutative substructural logics

We will show that algebraic characterization of pseudo-relevance property (PRP) given by L. Maksimova works well also for commutative substructural logics, i.e. extensions of FLe. More precisely, a commutative substructural logic L has the pseudo-relevance property iff the joint embeddability property (JEP) holds in the corresponding variety V(L). We will discuss also how weakening rules have an effect on relations between PRP and the deductive interpolation property, or equivalently, between JEP and amalgamation property.

10:00 - 10:50 Felix Bou (JAIST): Some reducts on (commutative integral bounded) residuated lattices

The talk analyzes the variety of algebras generated by the subreducts of (commutative integral bounded) residuated lattices in the language with disjunction, fusion, negation, falsum and verum (and also with conjunction). An axiomatization of the variety is presented. Although it holds that every algebra in this variety is embeddable in a complete residuated lattice, it results that there are algebras in the variety that are not completely embedabble in a complete residuated lattices. This last fact provides a difference with what happens for residuated lattices. Finally, we study the lattice of congruences for the algebras in this variety.

11:00 - 11:50 Clint van Alten (Univ. of the Witwatersrand) : Varieties of residuated lattices with EDPC

The Full Lambek Calculus is known to lack both the deduction theorem and the local deduction theorem. Algebraically, this says that the equivalent algebraic semantics, namely the variety of residuated lattices, lacks EDPC (equationally definable principal congruences) and the CEP (congruence extension property).

I shall discuss term based characterizations of the varieties of residuated lattices that have EDPC (which correspond to extensions of the Full Lambek Calculus that have a deduction theorem). A weaker version of EDPC, called EDPC*, is shown to be equivalent to EDPC for varieties of residuated lattices. Morevoer, we show that if a particular residuated lattice satisfies EDPC*, then so does the variety it generates. Similar results are given for varieties with the CEP. Using the fact that residuated lattices are ideal determined we may focus on ideals rather than congruences. We also present a finite basis of ideal terms which is a useful aid in the study of ideals and EDPC. Some examples illustrating these results will be given.

Lunch

13:10 - 14:00 T. Litak (JAIST): On strong completeness

For well-behaved propositional logics, such as normal modal logics or intermediate logics, the notion of weak completeness (for theorems) or strong completeness (for the consequence operator) does not seem to be of much interest from general algebraic point of view. One may easily prove weak and strong completeness results via the standard Lindenbaum technique. But when we are interested only in algebras which have some special properties, such as lattice-completeness, the situation changes a lot. The completeness results cannot be taken for granted any more, and also weak completeness may fail to imply strong completeness.

We would like to:
# define the notion of strong completeness with respect to a class of algebras with a given property and prove that several intuitive definitions result in the same notion if the property in question is sufficiently well-behaved;
# study some interesting properties for which weak and strong completeness coincide and
# study some other interesting properties which give rise to a notion of consequence which is inherently second-order.

14:00 - 14:50 K. Terui (National Institute of Informatics): Which structural rules preserve cut elimination? -- a semantic criterion

Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a logic without any structural rules. The aim of this work is to give such a condition by using algebraic semantics.

We consider full Lambek calculus (FL) as our basic framework. Residuated lattices are the algebraic structures corresponding to FL. In this setting, we introduce a criterion, called the propagation property, that can be stated both in syntactic and algebraic terminology. We then show that, for any set S of structural rules, the cut elimination theorem holds for FL enriched with S if and only if S satisfies the propagation property.

As an application, we show that any set S of structural rules can be "completed" into another set S*, so that the cut elimination theorem holds for FL enriched with S*.

Coffee Break

15:00 - 15:50 N. Galatos (Vanderbilt University): Equivalence of closure operators: an order-theoretic perspective -- preliminary report. [Joint work with Constantine Tsinakis]

The notion of algebraizability of a consequence relation on a set of formulas was defined by Blok and Pigozzi. This definition was further expanded to consequence relations on sets of sequents by the Barcelona school. These definitions seem ad hoc at first glance. Jonsson and Blok, in a joint series of talks, define a more general notion of equivalence between consequence relation that covers the first case and can be modified to cover the second, as well. We expand the ideas in their work to a general setting that includes hypersequents and give an order-theoretic perspective to the notion of equivalence. We believe that the level of generality we chose makes the ideas clearer.

========================================================================
The Workshop is organized by LCCC project team in JAIST, and is partly supported by JAIST International Joint Research Program.

For additional information, please contact

Hiroakira Ono : ono@jaist.ac.jp
Hitoshi Kihara : h-kihara@jaist.ac.jp