A1 Refereed original research article in a scientific journal
Characterizing intermediate tense logics in terms of Galois connections
Authors: Dzik W, Jarvinen J, Kondo M
Publisher: OXFORD UNIV PRESS
Publication year: 2014
Journal: Logic Journal of the IGPL
Journal name in source: LOGIC JOURNAL OF THE IGPL
Journal acronym: LOG J IGPL
Volume: 22
Issue: 6
First page : 992
Last page: 1018
Number of pages: 27
ISSN: 1367-0751
DOI: https://doi.org/10.1093/jigpal/jzu024
Abstract
We propose a uniform way of defining for every logic L intermediate between intuitionistic and classical logics, the corresponding intermediate tense logic LKt. This is done by building the fusion of two copies of intermediate logic with a Galois connection LGC, and then interlinking their operators by two Fischer Servi axioms. The resulting system is called L2GC+FS. In the cases of intuitionistic logic Int and classical logic Cl, it is noted that Int2GC+FS is syntactically equivalent to intuitionistic tense logic IKt by W. B. Ewald and Cl2GC+FS equals classical tense logic Kt. This justifies calling L2GC+FS the L-tense logic LKt for any intermediate logic L. We define H2GC+FS-algebras as expansions of HK1-algebras, introduced by E. Orlowska and I. Rewitzky. For each intermediate logic L, we show algebraic completeness of L2GC+FS and its conservativeness over L. We prove relational completeness of Int2GC+FS with respect to the models defined on IK-frames introduced by G. Fischer Servi. We also prove a representation theorem stating that every H2GC+FS-algebra can be embedded into the complex algebra of its canonical IK-frame.
We propose a uniform way of defining for every logic L intermediate between intuitionistic and classical logics, the corresponding intermediate tense logic LKt. This is done by building the fusion of two copies of intermediate logic with a Galois connection LGC, and then interlinking their operators by two Fischer Servi axioms. The resulting system is called L2GC+FS. In the cases of intuitionistic logic Int and classical logic Cl, it is noted that Int2GC+FS is syntactically equivalent to intuitionistic tense logic IKt by W. B. Ewald and Cl2GC+FS equals classical tense logic Kt. This justifies calling L2GC+FS the L-tense logic LKt for any intermediate logic L. We define H2GC+FS-algebras as expansions of HK1-algebras, introduced by E. Orlowska and I. Rewitzky. For each intermediate logic L, we show algebraic completeness of L2GC+FS and its conservativeness over L. We prove relational completeness of Int2GC+FS with respect to the models defined on IK-frames introduced by G. Fischer Servi. We also prove a representation theorem stating that every H2GC+FS-algebra can be embedded into the complex algebra of its canonical IK-frame.
UTU Research Portal