Bulletin of the Section of Logic 45/1 (2016)http://hdl.handle.net/11089/201432024-11-04T17:23:27Z2024-11-04T17:23:27ZCommutative Energetic Subsets of BCK-AlgebrasJun, Young BaeRoh, Eun HwanSong, Seok Zunhttp://hdl.handle.net/11089/216232019-03-14T10:50:11Z2016-01-01T00:00:00ZCommutative Energetic Subsets of BCK-Algebras
Jun, Young Bae; Roh, Eun Hwan; Song, Seok Zun
The notions of a C-energetic subset and (anti) permeable C-value in BCK-algebras are introduced, and related properties are investigated. Conditions for an element t in [0, 1] to be an (anti) permeable C-value are provided. Also conditions for a subset to be a C-energetic subset are discussed. We decompose BCK-algebra by a partition which consists of a C-energetic subset and a commutative ideal.
2016-01-01T00:00:00ZAn Alternative Natural Deduction for the Intuitionistic Propositional LogicIlić, Mirjanahttp://hdl.handle.net/11089/216222018-02-01T11:21:13Z2016-01-01T00:00:00ZAn Alternative Natural Deduction for the Intuitionistic Propositional Logic
Ilić, Mirjana
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.
2016-01-01T00:00:00ZA New Arithmetically Incomplete First- Order Extension of Gl All Theorems of Which Have Cut Free ProofsTourlakis, Georgehttp://hdl.handle.net/11089/216212018-02-01T11:21:13Z2016-01-01T00:00:00ZA New Arithmetically Incomplete First- Order Extension of Gl All Theorems of Which Have Cut Free Proofs
Tourlakis, George
Reference [12] introduced a novel formula to formula translation tool (“formulators”) that enables syntactic metatheoretical investigations of first-order 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, [2]) unavailable. This paper applies the formulator approach to show the independence of the axiom schema _A ! _8xA of the logics M3 and ML3 of [17, 18, 11, 13]. 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 ML3 is, similarly to QGL, an arithmetically incomplete first-order 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 [2, 8]).
2016-01-01T00:00:00ZElementary Proof of Strong Normalization for Atomic FFerreira, FernandoFerreira, Gildahttp://hdl.handle.net/11089/216202019-03-14T10:31:05Z2016-01-01T00:00:00ZElementary Proof of Strong Normalization for Atomic F
Ferreira, Fernando; Ferreira, Gilda
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ₐₜ (a predicative restriction of Girard’s system F).
2016-01-01T00:00:00Z