Some Combinatorics behind Proofs

TL;DR

This paper explores the combinatorial structures underlying formal proofs, generalizing the Craig Interpolation Theorem to broader set-based structures and interpreting these in logical and geometrical contexts.

Contribution

It introduces a generalized combinatorial framework for interpolation theorems, linking proof structures to graphs and surfaces, and unifies classical and intuitionistic logic interpretations.

Findings

A geometric formulation of the interpolation theorem

Conditions for combinatorial systems to enjoy interpolation

Connection between proof flow graphs and combinatorial structures

Abstract

We try to bring to light some combinatorial structure underlying formal proofs in logic. We do this through the study of the Craig Interpolation Theorem which is properly a statement about the structure of formal derivations. We show that there is a generalization of the interpolation theorem to much more naive structures about sets, and then we show how both classical and intuitionistic versions of the statement follow by interpreting properly the set-theoretic language. The theorem we present is a geometrical formulation of the well-known logical statement and gives sufficient conditions for a system of combinatorial nature to enjoy interpolation. Its objects might be graphs just as well as formulas or surfaces. The combinatorial mappings we use correspond whenever interpreted in a logical language to the notion of `logical flow graph' (i.e. a graph tracing the flow of occurrences of formulas in a proof; this notion has been introduced in (Buss, 1991). The idea of using the flow of occurrences to study the structure of proofs was already present in (Girard, 1987) with the concept of `proof net'.)