http://hdl.handle.net/11089/17643 Mon, 06 Apr 2026 06:53:29 GMT 2026-04-06T06:53:29Z https://dspace.uni.lodz.pl:443/bitstream/id/dab6f476-f91e-438d-8947-f86303706e8f/ http://hdl.handle.net/11089/17643 http://hdl.handle.net/11089/17909 A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics Gao, Feng; Tourlakis, George A well established technique toward developing the proof theory of a Hilbert-style modal logic is to introduce a Gentzen-style equivalent (a Gentzenisation), then develop the proof theory of the latter, and finally transfer the metatheoretical results to the original logic (e.g., [1, 6, 8, 18, 10, 12]). In the first-order modal case, on one hand we know that the Gentzenisation of the straightforward first-order extension of GL, the logic QGL, admits no cut elimination (if the rule is included as primitive; or, if not included, then the rule is not admissible [1]). On the other hand the (cut-free) Gentzenisations of the first-order modal logics M3 and ML3 of [10, 12] do have cut as an admissible rule. The syntactic cut admissibility proof given in [18] for the Gentzenisation of the propositional provability logic GL is extremely complex, and it was the basis of the proofs of cut admissibility of the Gentzenisations of M3 and ML3, where the presence of quantifiers and quantifier rules added to the complexity and length of the proof. A recent proof of cut admissibility in a cut-free Gentzenisation of GL is given in [5] and is quite short and easy to read. We adapt it here to revisit the proofs for the cases of M3 and ML3, resulting to similarly short and easy to read proofs, only slightly complicated by the presence of quantification and its relevant rules. Thu, 01 Jan 2015 00:00:00 GMT http://hdl.handle.net/11089/17909 2015-01-01T00:00:00Z http://hdl.handle.net/11089/17907 On Halldén Completeness of Modal Logics Determined by Homogeneous Kripke Frames Kostrzycka, Zofia Halldén complete modal logics are defined semantically. They have a nice characterization as they are determined by homogeneous Kripke frames. Thu, 01 Jan 2015 00:00:00 GMT http://hdl.handle.net/11089/17907 2015-01-01T00:00:00Z http://hdl.handle.net/11089/17905 Minimal Sequent Calculi for Łukasiewicz’s Finitely-Valued Logics Pynko, Alexej P. The primary objective of this paper, which is an addendum to the author’s [8], is to apply the general study of the latter to Łukasiewicz’s n-valued logics [4]. The paper provides an analytical expression of a 2(n−1)-place sequent calculus (in the sense of [10, 9]) with the cut-elimination property and a strong completeness with respect to the logic involved which is most compact among similar calculi in the sense of a complexity of systems of premises of introduction rules. This together with a quite effective procedure of construction of an equality determinant (in the sense of [5]) for the logics involved to be extracted from the constructive proof of Proposition 6.10 of [6] yields an equally effective procedure of construction of both Gentzen-style [2] (i.e., 2-place) and Tait-style [11] (i.e., 1-place) minimal sequent calculi following the method of translations described in Subsection 4.2 of [7]. Thu, 01 Jan 2015 00:00:00 GMT http://hdl.handle.net/11089/17905 2015-01-01T00:00:00Z http://hdl.handle.net/11089/17904 Tense Polyadic N × M-Valued Łukasiewicz–Moisil Algebras Figallo, Aldo V.; Pelaitay, Gustavo In 2015, A.V. Figallo and G. Pelaitay introduced tense n×m-valued Łukasiewicz–Moisil algebras, as a common generalization of tense Boolean algebras and tense n-valued Łukasiewicz–Moisil algebras. Here we initiate an investigation into the class tpLMn×m of tense polyadic n × m-valued Łukasiewicz–Moisil algebras. These algebras constitute a generalization of tense polyadic Boolean algebras introduced by Georgescu in 1979, as well as the tense polyadic n-valued Łukasiewicz–Moisil algebras studied by Chiriţă in 2012. Our main result is a representation theorem for tense polyadic n × m-valued Łukasiewicz–Moisil algebras. Thu, 01 Jan 2015 00:00:00 GMT http://hdl.handle.net/11089/17904 2015-01-01T00:00:00Z