
Authors:
Roma J. ADILLON and Ventura VERDU
Title:On a Substructural Gentzen System, its Equivalent Variety Semantics and its External Deductive System
Pages:125134
File:bibtex
Abstract ( + )
It was shown that the Gentzen system G_{LJ*\c}, the deductive system IPC*\c and the equational system < L,_{RL}> associated with the variety of residuated lattices are equivalent in a given sense. In this paper we show that if we delete the rules for the implication connective from the sequent calculus LJ*\c, then the Gentzen system G" obtained from this sequent calculus is algebraizable and the variety of bounded commutative integral lmonoids is its equivalent algebraic semantics. As a consequence of this result we obtain that the contraction rule is not derivable in G", so we can say that G" is a substructural Gentzen system. It is also shown that there is no deductive system equivalent to G" or to < L,_{BCILM}> and that the variety of BCILM is an algebraic semantics for the just obtained external deductive system S_{G"}^{0} associated with G", with defining equation p~1. Finally we prove that this deductive system S_{G"}^{0} is not protoalgebraic.

Authors:
Jacek MALINOWSKI
Title:On Generalizations of Consequence Operation
Pages:135143
File:bibtex
Abstract ( + )
We define some classes of operation generalizing the notion of logical consequence operation. Then we investigate them in terms of properties of their theories.

Authors:
George WEAVER and Benjamin GEORGE
Title:Quasifinitely Characterizable and Finitely Characterizable Dedekind Algebras
Pages:145157
File:bibtex
Abstract ( + )
A Dedekind algebra is an ordered pair (B,h) where h is a similarity transformation on the nonempty set B. Among these is the sequence of the positive integers. An algebra is finitely characterizable provided some finite subset of its secondorder theory is categorical. Dedekind showed that the sequence of the positive integers is finitely characterizable. Here a condition is presented that is both necessary and sufficient for a Dedekind algebra to be finitely characterizable. It is also shown that a weaker condition is both necessary and sufficient for a Dedekind algebra to be quasifinitely characterizable (i.e. that some finite subset of its secondorder theory is categorical in all powers). Finally, it is shown that there is a number theoretic condition both necessary and sufficient for a countably infinite Dedekind algebra to be finitely characterizable.

Authors:
Andrzej INDRZEJCZAK
Title:Resolution Based Natural Deduction
Pages:159170
File:bibtex
Abstract ( + )
The paper is an introductory presentation of a hybrid formal system that mix some features of Natural Deduction systems and Resolution. Resulting system, called RND (Resolution based ND), allows to build derivations in particularly simple and natural manner. Moreover, in RND one can simulate other methods of proof. It seems to make RND particularly useful frame for comparison of efficiency of several proofsearch strategies.

Authors:
Eunsuk YANG
Title:TR, TER, TEcR
Pages:171181
File:bibtex
Abstract ( + )
In this paper we investigate the relevance logic TR of the Ticket Entailment T without the reductio (R), and its extensions TER, TEcR: TER is the TR with the expansion (E) and TEcR the TER with the chain (c). We give completeness for each TR, TER, and TEcR by using RoutleyMeyer semantics.