
Authors:
Fernando FERREIRA and Gilda FERREIRA
Title:An Elementary Proof of Strong Normalization for Atomic F
Pages:116
File:bibtex
Abstract ( + )
We give an elementary proof (in the sense that it is formalizable in Peano arithmetic) of the strong normalization of the atomic polymorphic calculus F at (a predicative restriction of Girard’s system F).

Authors:
G. TOURLAKIS
Title:A New Arithmetically Incomplete First Order Extension of Gl All Theorems of Which Have Cut Free Proofs
Pages:1732
File:bibtex
Abstract ( + )
Reference \cite{SchTou1} introduced a novel formula to formula translation tool (``formulators'') that enables syntactic metatheoretical investigations of firstorder modal logics, bypassing a need to convert them first into Gentzen style logics in order to rely on cut elimination and the subformula property. In fact, the formulator tool, as was already demonstrated in loc.\ cit., is applicable even to the metatheoretical study of logics such as QGL, where cut elimination is (provably, \cite{Avr}) unavailable. This paper applies the formulator approach to show the independence of the axiom schema □→□ ∀x A of the logics M^{3} and ML^{3} of \cite{TKpaper1, TKpaper2, SchTou, SchTou2}. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations. In particular, the so modified ML^{3} is, similarly to QGL, an arithmetically incomplete firstorder extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics (compare with the more complex proofs in \cite{Avr, samval}).

Authors:
Mirjana ILIC
Title:An Alternative Natural Deduction for the Intuitionistic Propositional Logic
Pages:3351
File:bibtex
Abstract ( + )
A natural deduction system NI, for the full propositional intuitionistic logic, is proposed. The operational rules of NI are obtained by the translation from Gentzen's calculus LJ and the normalization is proved, via translations from sequent calculus derivations to natural deduction derivations and back.

Authors:
Young Bae Jun, Eun Hwan Roh and Seok Zun Song
Title:Commutative Energetic Subsets of BCKAlgebras
Pages:5364
File:bibtex
Abstract ( + )
The notions of a Cenergetic subset and (anti) permeable Cvalue in BCKalgebras are introduced, and related properties are investigated. Conditions for an element t in [0,1] to be an (anti) permeable Cvalue are provided. Also conditions for a subset to be a Cenergetic subset are discussed. We decompose BCKalgebra by a partition which consists of a Cenergetic subset and a commutative ideal.