
Authors:
Maria MANZANO and Manuel A. MARTINS and Antonia HUERTAS
Title:A Semantics for Equational Hybrid Propositional Type Theory
Pages:121138
File:bibtex
Abstract ( + )
The definition of identity in terms of other logical symbols is a recurrent issue in logic. In particular, in FirstOrder Logic (FOL) there is no way of defining the global relation of identity, while in standard SecondOrder Logic (SOL) this definition is not only possible, but widely used. In this paper, the reverse question is posed and affirmatively answered: Can we define with only equality and abstraction the remaining logical symbols? Our present work is developed in the context of an equational hybrid logic (i.e. a modal logic with equations as propositional atoms enlarged with the hybrid expressions: nominals and the @ operator). Our logical base is propositional type theory. We take the propositional equality, λ abstraction, nominals, ◊ and @ operators as primitive symbols and we demonstrate that all of the remaining logical symbols can be defined, including propositional quantifiers and equational equality.

Authors:
Andrzej INDRZEJCZAK
Title:Contraction Contracted
Pages:139154
File:bibtex
Abstract ( + )
This short article is mainly of methodological character. We are concerned with the problem of elimination of the rule of contraction from the set of primitive rules of a sequent calculus. It is desirable since this rule is technically embarassing in cut elimination proofs. It appears that simple change in the way of reading composition of contexts in sequents allows for eliminating contraction in some types of sequent calculi. In particular we do not need to prove it as an admissible rule in contrast to what is deserved in known Dragalin's construction. For simplicity sake we consider only the case of propositional classical logic but the proposed solution may be applied also to sequent formalizations of other logics, in particular to extensions of classical logic.

Authors:
Kordula SWIETORZECKA
Title:An Argument for the Existence of God by Bolzano. A Formalization with a Distinction between Menge and Inbegriff
Pages:155172
File:bibtex
Abstract ( + )
Bernard Bolzano is the author of a text considered by him as an argument for the existence of God, originally published in the ``Lehrbuch der Religionwissenschaft" (1834). His disquisition was formalized by H. Ganthaler and P. Simons in 1987 who based their approach on the wellknown set theoretical interpretation of Bolzano's idea of multiplicity. The authors formulated a theory expressed in set theoretical language extended by some specific terms and constructed a proof as a formalization of the reasoning given by Bolzano. A problematic aspect of the proposal of Ganthaler and Simons is that it passes over the distinction of two different types of multiplicities which enable to point some interesting formal and material details of Bolzano's revised argumentation. In the frame of the presented proposal we invent two special meanings of Bolzano's notion of multiplicity: distributive and collective. In connection with this distinction we reconstruct the argument analyzed by Ganthaler and Simons and discuss the formal and philosophical power of the obtained formalization. The inspiration for our approach comes from the fact that Bolzano used in his text two terms Menge and Inbegriff in probably different meanings. However the main aim of this proposal is to take a new look at Bolzano's argument, rather than to provide historical investigations.

Authors:
Janusz CIUCIURA
Title:Paraconsistent heap. A Hierarchy of mbC^{n}systems
Pages:173182
File:bibtex
Abstract ( + )
There is no consensus on what paraconsistency is. There are several definitions of paraconsistent logic. One of them is that paraconsistent logic is a logic which is not closed under the rule P, ¬ P / Q (known as the rule of explosion). The pair of the formulas P and ¬ P entails any Q. But this definition is too broad because it includes some logics which have nothing in common with paraconsistency (provided that someone else would not read it differently from the intentions of their authors).
In 2007, Carnielli, Coniglio and Marcos presented a study on the Logics of Formal Inconsistency. The study begins with a logical system called bC that is the basic logic of inconsistency.
Here we focus on a system weaker than bC (mbC for short) which appears as the result of deleting the law of double negation from the set of axioms of bC and present an axiomatization of mbC formulated directly in the language of classical propositional logic. This makes the connective of consistency redundant and enables to build a hierarchy of mbC^{n}systems in which (different variants of) the rule of explosion play(s) the key role.

Authors:
Piotr KULICKI
Title: A Note on the Adequacy of Jerzy Kalinowski’s K_{1} Logic
Pages:183190
File:bibtex
Abstract ( + )
Jerzy Kalinowski's K_{1} logic is one of the first systems of deontic logic. Kalinowski presented it in two forms: as an axiomatic system and with the use of deontic tables analogous to Łukasiewicz's theevalued propositional logic. Adequacy of those two approaches is proven.

Authors:
A. V. FIGALLO, E. PICK and S. SAAD
Title:A Representation for Finite Hilbert Algebras
Pages:191202
File:bibtex
Abstract ( + )
In this work we show, that given a finite Hilbert algebra A, there exists an antiisomorphism of A in a subreduct of the algebra D(A) of the deductive systems of A, where D(A) is endowed with the implication defined between sets given by Horn.

Authors:
Szymon FRANKOWSKI
Title:About Simulating Polyadic Frames
Pages:203214
File:bibtex
Abstract ( + )
This paper is devoted to the problem of expressivity of polyadic frame by the frame containing unary modalities only. Our approach differs from [2] because it provides different coding of frame properties. However, we add exactly one nominal, to make the the class of simulating frames definable.