A Sequent Calculus Proof Search Procedure and Counter-model Generation based on Natural Deduction Bounds

TL;DR

This paper refines a bottom-up sequent calculus proof search procedure for minimal implicational logic, providing improved termination strategies, explicit bounds, and comprehensive soundness and completeness proofs.

Contribution

It introduces a new termination strategy for the sequent calculus, with explicit bounds and an improved completeness proof for proof search in minimal implicational logic.

Findings

Refined proof search termination strategy

Explicit upper bounds on proof search

Complete soundness and completeness proofs

Abstract

In a previously published ENTCS paper (Santos et al. (2016)), we introduced a sequent calculus called $\mathbf{LMT^{\rightarrow}}$ for Minimal Implicational Propositional Logic ($\mathbf{LMT^{\rightarrow}}$). This calculus provides a proof search procedure for $\mathbf{LMT^{\rightarrow}}$ that works in a bottom-up approach. We proved there that $\mathbf{LMT^{\rightarrow}}$ is sound and complete. We also suggested a strategy to guarantee termination of the proof search procedure. In this current paper, we refined this strategy and presented a new strategy for $\mathbf{LMT^{\rightarrow}}$ termination. Considering this new strategy, we also provide a (new) completeness proof for the system, which improves the previous version. Besides that, we present explicit upper bounds on the proof search procedure, derived from this new strategy. We also provide a full soundness proof of the system.