Cached on July 10, 2011, from the University of Turku, Finland:
http://staff.cs.utu.fi/kurssit/comp_sci_logic/GaloisLogic.html

Galois Connections and Modal Logics

Credits:
2 points
Teaching methods:
Lectures (10 h)
Modes of study:
Exam
Evaluation:
0 - 5
Person in charge:
Jouni Järvinen

Lecturers

Description

Modal logics deal with modalities. For instance, if it is true that "Matti is happy," we might qualify this statement by saying that "Matti is very happy", in which case the term "very" is a modality. Traditionally, there are two modalities, namely, possibility and necessity. The basic modal operators are usually written box (square) for necessarily and diamond (diamond) for possibly. Then, for example, diamondP can be read as "it is possibly the case that P".

Temporal logic is a system for representing and reasoning about time. Some expressions, such as "2 + 3 = 5" are true at all times, while tensed expressions such as "Matti is happy" are true only sometimes. Tense constructions are treated in terms of two pairs of modalities, one for the past and one for the future:

Galois connections are pairs of maps which enable us to move back and forth between two ordered sets. Galois connections tie different structures firmly and when a Galois connection is found between two structures, we immediately know that they have much in common. Formally, let (A, ≤) and (B, ≤) be two partially ordered sets. A Galois connection between these ordered sets consists of two maps f: A → B and g: B → A such that for all a in A and b in B, we have

f(a) ≤ b  if and only if  a ≤ g(b).

In [3], Information Logic of Galois Connections (ILGC) suited for approximate reasoning about knowledge is introduced. ILGC is just classical propositional logic with two connectives f and g mimicking the performance of Galois connection maps on ordered sets. More precisely, ILGC is defined by adding to classical propositional logic the following two rules of inference:

In this course, we present the basics of propositional logic and intuitionistic logic. Also the essential part of modal logics is presented and especially we study the minimal tense logic Kt. Kripke semantics is defined for modal logics, and completeness and decidability of Kt is shown.

The logic ILGC is introduced with a Kripke-style semantics. The semantics is based on information relations enabling us to perform rough set style reasoning. Interestingly, we show that with respect to provability, ILGC is equivalent to minimal tense logic Kt.

In [4], an intuitionistic propositional logic with a Galois connection (IntGC) is introduced as an intuitionistic version of ILGC. We give Kripke-style and algebraic semantics 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. Also, a representation theorem for Heyting algebras with Galois connections is proved, and an application to rough lattice-valued sets is presented.

The logic IntGC is not same as the intuitionistic tense logic (IntKt) presented in [5]. At the end of the course, we will study how IntGC should be modified to obtain IntKt. Galois connections in mono-modal logic and their semantics will be also studied.

Literature

  1. Brian A. Davey, Hilary A. Priestley: Introduction to Lattices and Order (2nd Edition), Cambridge University Press, 2002.

  2. Patrick Blackburn, Maarten de Rijke, Yde Venema: Modal Logic, Cambridge University Press, 2001.

  3. Jouni Järvinen, Michiro Kondo, Jari Kortelainen: Logics from Galois connections, International Journal of Approximate Reasoning 49 (2008) pp. 595−606. doi: 10.1016/j.ijar.2008.06.003

  4. Wojciech Dzik, Jouni Järvinen, Michiro Kondo: Intuitionistic propositional logic with Galois connections, Logic Journal of the IGPL (article in press). doi: 10.1093/jigpal/jzp057

  5. W. B. Ewald: Intuitionistic Tense and Modal Logic, The Journal of Symbolic Logic 51 (1986) pp. 166-179. http://www.jstor.org/stable/2273953