Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Christoph Wernhard

Abstract

We present a Maehara-style construction of Craig interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's $G_3$. The method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of a sequent calculus for HT by Mints. 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 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.

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

Abstract

We present a Maehara-style construction of Craig interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's . The method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of a sequent calculus for HT by Mints. 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 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.
Paper Structure (10 sections, 18 equations, 1 figure)

This paper contains 10 sections, 18 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Considered Logics
  3. Considered Sequent Systems
  4. Restrictions of Mints' Axioms.
  5. Axioms and Rules for Truth Value Constants.
  6. Axioms and Rules for $\mathsf{nh}$.
  7. A Third New Rule for Implication.
  8. Completeness.
  9. Interpolating Sequent Systems -- "Maehara's Method"
  10. An Interpolating Sequent System for HT with HTnh Interpolants

Figures (1)

  • Figure 1: Truth tables for the considered logic operators. They extend the valuations for HT by the specification of $\mathsf{nh}(A)$.