Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System

TL;DR

This paper introduces a novel method for constructing Craig-Lyndon interpolants in the three-valued logic of here and there (HT), adapting recent techniques to operate directly on HT formulas.

Contribution

It presents a variation of Mints' sequent system for HT and a two-stage approach to generate HT-specific Craig-Lyndon interpolants, improving on classical encoding methods.

Findings

The method successfully constructs HT Craig-Lyndon interpolants.

It adapts a recent interpolation technique to a nonclassical logic setting.

The approach operates directly on HT formulas, avoiding classical encodings.

Abstract

We present a variation of Maehara's method to construct Craig-Lyndon interpolants for the three-valued propositional logic of here and there (HT), also known as G\"odel's $G_3$, a superintuitionistic logic of importance in logic programming. Our method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of Mints' sequent system for HT. The approach is characterized by two stages: First, a preliminary interpolant is constructed, a formula that is an interpolant in some sense but not yet the desired HT formula. In the second stage, an actual HT interpolant is obtained from this preliminary interpolant. With the classical encoding, the preliminary interpolant is a classical Craig-Lyndon interpolant for classical encodings of the two input HT formulas. In the presented adaptation, the sequent system operates directly on HT formulas, and the preliminary interpolant is in a nonclassical logic that generalizes HT by an additional logic operator.