Intuitionistic logic with two Galois connections combined with Fischer Servi axioms

TL;DR

This paper extends intuitionistic logic with dual Galois connections and Fischer Servi axioms, providing semantics, algebraic models, and showing equivalence to intuitionistic tense logic IKt.

Contribution

It introduces the Int2GC+FS logic, combining two Galois connections with Fischer Servi axioms, and proves its completeness and equivalence to IKt.

Findings

Presented Kripke-style and algebraic semantics for the logics.

Proved completeness of Int2GC and Int2GC+FS with respect to these semantics.

Established algebraic models using rough lattice-valued fuzzy sets on Heyting algebras.

Abstract

Earlier, the authors introduced the logic IntGC, which is an extension of intuitionistic propositional logic by two rules of inference mimicking the performance of Galois connections (Logic J. of the IGPL, 18:837-858, 2010). In this paper, the extensions Int2GC and Int2GC+FS of IntGC are studied. Int2GC can be seen as a fusion of two IntGC logics, and Int2GC+FS is obtained from Int2GC by adding instances of duality-like connections $\Diamond(A \to\ B) \to (\Box A \to \Diamond B)$ and $(\Diamond A \to \Box B) \to \Box(A \to B)$, introduced by G. Fischer Servi (Rend. Sem. Mat. Univers. Politecn. Torino, 42:179-194, 1984), for interlinking the two Galois connections of Int2GC. Both Kripke-style and algebraic semantics are presented for Int2GC and Int2GC+FS, and the logics are proved to be complete with respect to both of these semantics. We show that rough lattice-valued fuzzy sets defined on complete Heyting algebras are proper algebraic models for Int2GC+FS. We also prove that Int2GC+FS is equivalent to the intuitionistic tense logic IKt, and an axiomatisation of IKt with the number of axioms reduced to the half of the number of axioms given by W. B. Ewald (J. Symb. Log, 51:166-179, 1986) is presented.