
Authors:
Janis CIRULIS
Title:Beniaminov Algebras Revised: One More Algebraic Versionof Firstorder Logic
Pages:140145
File:bibtex
Abstract ( + )
E.M.Benjaminov introduced a class of algebras called by him relational algebras. The term comes from database theory, and it generally refers to algebras of a certain kind suggested by E.F.Codd. Beniaminov described another version of the relational data model and also proposed a set of axioms to characterize abstractly his class of "concrete" relational algebras. However, he did not present any results concerning strength of the axiom system, neither did he compare his algebras with other known algebras of finitary relations. By the way, his axiom set proves to be incomplete in a strong sense. We show here that a slightly restricted class of Beniaminov's relational algebras is interdefinable with that of locally finite cylindric algebras (if the dimensions of the algebras in both classes are concordant) and provides therefore an adequate algebraic version of firstorder logic.

Authors:
Takao INOUE
Title:On the Atomic Formula Property of Hartig's Refutation Calculus
Pages:146150
File:bibtex
Abstract ( + )
It is wellknown that Gentzen's sequent calculus LK enjoys the socalled subformula property: that is, a proof without cut in LK contains only subformulas of the formula occurring in the endsequent. In this paper, we shall propose a similar property, namely the atomic formula property, which is weaker than the subformula property, and we shall remark that for every formula provable in Hartig's refutation calculus HC, there is a proof of it in HC with the proposed property.

Authors:
Maciej KANDULSKI
Title:Axiomatizations of Commutative and Nonassociative Ajdukiewicz Calculus
Pages:151157
File:bibtex
Abstract ( + )
Commutative syntactic calculi used to be introduced in different ways: as unidirectional systems, as bidirectional systems augmented with a structural rule of Permutation and also as unidirectional systems with Permutation. Ajdukiewicz and Lambek syntactic calculi are currently linked with substructural logics, i.e. with systems in which derivability of a formula depends not only on a very set of premises but also on a way in which they are configured (structuralized). If seen from the perspective of substructural logic the productfree commutative Lambek calculus (Lambekvan Benthem calculus) amounts to the implicational fragment of the (sentential) intuitionistic Linear Logic. The bidirectional nonassociative Lambek calculus, when enriched with Permutation as the only structural rule, is equivalent to a unidirectional system (without Permutation), which can be obtained from the previous one by unification of the left and right divisions. An analogous result, however, is in general not valid for the Ajdukiewicz calculus. We show that the equivalence of bidirectional Ajdukiewicz calculus with permutation and unidirectional calculus holds only for a restricted class of formulas with antecedent consisting of types of the order less than 2 and with succedent being a primitive type.The presented in this paper axiomatization of the nonassociative and commutative Lambek calculus NLP refers to other formalisms for different versions of Lambek calculi.

Authors:
S.M. KIM
Title:ωconsistency and Loeb's Theorem
Pages:158162
File:bibtex
Abstract ( + )
Despite the provable equivalence between Loeb's Theorem and Goedel's Second Incompleteness Theorem, the former and its proof do not explicitly involve any assumption of consistency, while the latter and its proof do. This paper establishes some logicomathematical relationship between Loeb's Theorem and ωconsistency.

Authors:
Vladimir L.VASYUKOV
Title:From Ternary to Tetrary?
Pages:163167
File:bibtex
Abstract ( + )
In order to avoid `suspicious' for logicians ternary accessibility relation in the semantic for R there was proposed its `bibinary' (i.e. binary + binary) version. Unfortunately, the incompleteness of such a semantics was proved. A new proposal is to exploit another sense of `bibinariness': now a binary relation is defined on the set of pairs of possible worlds.

Authors:
R. ZUBER
Title:A Note the Logical Dependence of Simple Quantifiers
Pages:168172
File:bibtex
Abstract ( + )
It is shown that the specific property of conservativity known from the study of natural language quantifiers entails an algebraic version of logical dependence.

Authors:
Andrzej INDRZEJCZAK
Title:Natural Deduction System for Tense Logics
Pages:173
File:bibtex
Abstract ( + )
The purpose of this paper is to show natural deduction formalization for standard systems of propositional tense logic, where by `standard' we mean logic of four nonextensional unary operators: H (it has always been thee case), P (it was the case), G (it is always going to be the case), F (it will be the case).