
Authors:
Norihiro KAMIDE
Title:A Note on Decision Problems for Implicational Sequent Calculi
Pages:129138
File:bibtex
Abstract ( + )
We investigate cuteliminability and decidability for implicational sequent calculi with prime contraction. The prime contraction is a restricted version of the contraction rule in LJ (the rule does not permit the contraction of implication formulas). Decision problems for the implicational sequent calculi LBB'IW (the system for the logic BB'IW) and FL_{c>} (the implicational fragment of the full Lambek calculus with the contraction rule) are wellknown open problems. We show the partial results that the calculi with prime contraction instead of the usual contraction are decidable.

Authors:
Francisco SALTO, Jose M. MENDEZ and Gemma ROBLES
Title:Restricting the Contraction Axiom in Dummett's LC: LC with the Converse Ackermann Property
Pages:139146
File:bibtex
Abstract ( + )
LC^{o} with the Converse Ackermann Property is defined as the result of restricting Contraction in LC. Intuitionistic and Superintuitionistic Negation is shown to be compatible with the CAP.

Authors:
Takahiro SEKI
Title:Some Remarks on Maehara's Method
Pages:147154
File:bibtex
Abstract ( + )
In proving the interpolation theorem in terms of sequent calculus, Maehara's method is usually used. This paper shows that the interpolation theorem for substructural logics obtained by deleting constants from FL, FL_{e}, FL_{ec}, CFL_{e} and CFL_{ec} can be proved by putting some restriction on partitions in Maehara's method.

Authors:
Gabor SAGI
Title:NonComputability of the Equational Theory of Polyadic Algebras
Pages:155164
File:bibtex
Abstract ( + )
Daigneault and Monk proved that the class of (ω dimensional) representable polyadic algebras (RPA_{ω} for short) is axiomatizable by finitely many equationschemas. However, this result does not imply that the equational theory of RPA_{ω} would be recursively enumerable; one simple reason is that the language of RPA_{ω} contains a continuum of operation symbols. Here we prove the following. Roughly, for any reasonable generalization of computability to uncountable languages, the equational theory of RPA_{ω} remains nonrecursively enumerable, or noncomputable, in the generalized sense. This result has some implications on the noncomputational character of Keisler's completeness theorem for his ``infinitary logic''.

Authors:
Larry WOS and Ruediger THIELE
Title:Hilbert's New Problem
Pages:165175
File:bibtex
Abstract ( + )
Throughout the twentieth century, the worlds of logic and mathematics were well aware of Hilbert's twentythree problems and the challenge they offered. Although not known until very recently, there existed yet one more challenge offered by Hilbert, his twentyfourth problem. This problem focuses on finding simpler proofs, on the criteria for measuring simplicity, and on the ``development of a theory of the method of proof in mathematics in general''. Of the three themes of Hilbert's twentyfourth problem, the first two are central to this article. We visit various areas of logic, showing that some of the studies of the masters are indeed strongly connected to this newly discovered problem. We also demonstrate that the use of an automated reasoning program (specifically, W. McCune's OTTER) enables one to address this challenging problem. We offer questions that remain unanswered.