Correspondence theory for intuitionistic Lukasiewicz logic

We develop the correspondence theory for $\GBLe$, which can be viewed as the intuitionistic counterpart of propositional {\L}ukasiewicz logic. Our methodology follows \cite{britz2025correspondencetheorymanyvaluedmodal}. We adopt algorithmic correspondence theory method, identify the class of inductive formulas, and develop an algorithm for computing the many-valued first-order correspondents of given inductive formulas. The key step is to find the interpretations of nominals and conominals (whose interpretations are the counterparts of singletons and their complements) in $\GBLe$ which can be translated into many-valued first-order predicate logic.
\keywords{intuitionistic {\L}ukasiewicz logic \and correspondence theory \and inductive formulas}