| 1. Antonio M. SETTE and Elias H. ALVES, On the equivalence between some systems of non-classical logic | 68 [Abstract] [PDF] |
| 2. Roma J. ADILLON and Ventura VERDU, A Gentzen system equivalent to the BCK-logic | 73 [Abstract] [PDF] |
| 3. Piotr LUKOWSKI, Modal interpretation of Heyting-Brouwer logic | 80 [Abstract] [PDF] |
| 4. Alexander YASHIN, On Novikov's approach to the notion of a new intuitionistic connective: two negative examples | 84 [Abstract] [PDF] |
| 5. Jean-Yves BEZIAU, Identity, structure and logic | 89 [Abstract] [PDF] |
| 6. Andrzej INDRZEJCZAK, Cut-free sequent calculus for S5 | 95 [Abstract] [PDF] |
| 7. Janusz CZELAKOWSKI, Filtered subdirect products | 103 [Abstract] [PDF] |
1. Antonio M. SETTE and Elias H. ALVES,
On the equivalence between some systems of non-classical logic
Loparic and da Costa define three systems of propositional logic, called
β0, β1 and β2. In β0
neither the principle of excluded middle nor the principle of non-contradiction
is valid, in general. System β1 is an extension of β0,
where the principle of non-contradiction is valid, but the principle of
excluded-middle is not. System β2 is also an extension of
β0, where the principle of excluded middle is valid, but the
principle of non-contradiction is not. Systems such as β2 are
called paraconsistent systems. Systems such as β1 are
called by Loparic and da Costa paracomplete systems. Loparic and da Costa
mentioned that system β2 is equivalent to system P1, introduced by
Sette. On the other hand, Sette and Carnielli study a system, called I1, which is,
according to them, weakly-intuitionistic, that is, where the law of excluded
middle cannot be proved. (This corresponds to the notion of paracompleteness
of Loparic and da Costa.) According to Sette and Carnielli, system I1 is a counterpart
of the paraconsistent calculus P1. We will show, here, that system β2
is, in fact, equivalent to P1. In addition, we will show that β1 is
equivalent to I1.
2. Roma J. ADILLON and Ventura VERDU, A Gentzen system
equivalent to the BCK-logic
The sequent calculus LBCK is obtained by deleting the contraction rule
and the introduction rules of the connectives of meet, join and negation from the
sequent calculus for the Intuitionistic Propositional logic, LJ. In this paper we
show that the Gentzen system GBCK, naturally associated with
LBCK, is equivalent to the Hilbert-style logic BCK, in the sense that
GBCK and BCK are interpretable one another, the interpretations being
essentially inverse in each other. This result is a strengthening of the one
obtained by H. Ono and Y. Komori, which concerned only the derivable sequents of
LBCK and the theorems of BCK. We obtain, as a corollary of this result,
that the quasivariety of BCK-algebras is the equivalent quasivariety semantics of
GBCK.
3. Piotr LUKOWSKI, Modal interpretation of
Heyting-Brouwer logic
Long before the presentations of semantics for intuitionistic logic and
modal system S4, Goedel as the first interpreted the intuitionism in S4.
The intuitionistic logic is however "only one half" of the Heyting-Brouwer
logic. This paper introduces the enlarged translation interpreting H-B logic
in some modal system for which, S4 is "one half", only.
4. Alexander YASHIN, On Novikov's approach
to the notion of a new intuitionistic connective: two negative
examples
About 35 years ago P. Novikov suggested the so-called syntactic
approach to the notion of a new intuitionistic logical connective.
In this paper we shall consider two examples of additional connectives,
which were intensively studied but, however, are useless in the sense of
P.Novikov's definition.
5. Jean-Yves BEZIAU, Identity, structure
and logic
The concept of identity is a central idea of thought. We will see how modern
mathematics can give a precise analysis of this concept and how logic can deal
with this analysis. We will define three kinds of identity: the Bourbaki identity,
the logical identity and the diagonal identity (in short B-, l-, d-identity
respectively) and study the connections between them.
6. Andrzej INDRZEJCZAK, Cut-free sequent
calculus for S5
We aim at an exposition of some nonstandard cut-free Gentzen formalization
for S5, called DSC (double sequent calculus). DSC operates on two types of
sequents instead of one, and shifting of wffs from one side of sequent to
another is regulated by special rules and subject to some restrictions.
Despite of this apparent inconvenience it seems to be simpler than other,
known Gentzen-style systems for S5. The number of additional, formal
machinery is kept in reasonable bounds and proofs are quite simple. A
by-product of the completeness theorem for this calculus is an automated
proof-search procedure.
7. Janusz CZELAKOWSKI, Filtered subdirect
products
The operation PfS of forming filtered subdirect
products is examined. It is shown that for any class K of models,
PfS is the least quasivariety which contains K.