Logic Journal of IGPL Advance Access published online on October 20, 2009
Logic Journal of IGPL, doi:10.1093/jigpal/jzp057
Intuitionistic Propositional Logic with Galois Connections
Institute of Mathematics, University of Silesia, ul. Bankowa 12, 40-007 Katowice, Poland.
E-mail: dzikw{at}silesia.top.pl
Department of Information Technology, University of Turku, FI-20014 Turku, Finland.
E-mail: Jouni.Jarvinen{at}utu.fi
School of Information Environment, Tokyo Denki University, Inzai, 270-1382, Japan.
E-mail: kondo{at}sie.dendai.ac.jp
| Abstract |
|---|
In this work, an intuitionistic propositional logic with a Galois connection (IntGC) is introduced. In addition to the intuitionistic logic axioms and inference rule of modus ponens, the logic contains only two rules of inference mimicking the performance of Galois connections. Both Kripke-style and algebraic semantics are presented for IntGC, and IntGC is proved to be complete with respect to both of these semantics. We show that IntGC has the finite model property and is decidable, but Glivenko's Theorem does not hold. Duality between algebraic and Kripke semantics is presented, and a representation theorem for Heyting algebras with Galois connections is proved. In addition, an application to rough L-valued sets is presented.
Key Words: Galois connection Intuitionistic logic Algebraic semantics Kripke-semantics Representation