Intuitionistic logic with a Galois connection has the finite model property

TL;DR

This paper proves that the intuitionistic propositional logic with a Galois connection (IntGC) possesses the finite model property, ensuring that every satisfiable formula has a finite model.

Contribution

The authors establish the finite model property for IntGC, a logic combining intuitionistic logic with a Galois connection, which was previously unproven.

Findings

IntGC has the finite model property.

Every satisfiable formula in IntGC has a finite model.

The result enhances understanding of the model theory of IntGC.

Abstract

We show that the intuitionistic propositional logic with a Galois connection (IntGC), introduced by the authors, has the finite model property.