A Coinductive Approach to Proof Search

TL;DR

This paper introduces a coinductive framework for proof search in intuitionistic logic, representing all proofs as solution spaces using a novel lambda calculus extension with fixed points.

Contribution

It develops a coinductive approach to proof search, including a finitary calculus with fixed points and a method to handle complex contexts via co-contraction.

Findings

Reduction of coinductive solution spaces to finitary fixed-point calculus.

Effective handling of Horn formulas within the coinductive framework.

Insights into the semantic role of fixed points and co-contraction in proof representations.

Abstract

We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin's LJT for the implicational fragment. We introduce a variant of lambda calculus with potentially infinitely deep terms and a means of expressing alternatives for the description of the "solution spaces" (called B\"ohm forests), which are a representation of all (not necessarily well-founded but still locally well-formed) proofs of a given formula (more generally: of a given sequent). As main result we obtain, for each given formula, the reduction of a coinductive definition of the solution space to a effective coinductive description in a finitary term calculus with a formal greatest fixed-point operator. This reduction works in a quite direct manner for the case of Horn formulas. For the general case, the naive extension would not even be true. We need to study "co-contraction" of contexts (contraction bottom-up) for dealing with the varying contexts needed beyond the Horn fragment, and we point out the appropriate finitary calculus, where fixed-point variables are typed with sequents. Co-contraction enters the interpretation of the formal greatest fixed points - curiously in the semantic interpretation of fixed-point variables and not of the fixed-point operator.