Two logic papers

To: linear@cs.stanford.edu
Subject: Two logic papers
From: ale@csdec1.tuwien.ac.at (Alessandra Carbone)
Date: Thu, 4 Apr 1996 11:18:46 +0200
Approved: types@dcs.gla.ac.uk

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]


Both papers can be requested by writing to ale@logic.tuwien.ac.at.


TITLE: Interpolants, Cut Elimination and Flow Graphs for the
Propositional Calculus

AUTHOR: A. Carbone -- ale@logic.tuwien.ac.at

To appear in Annals of Pure and Applied Logic.


ABSTRACT: We analyse the structure of propositional proofs in the
sequent calculus focusing on the well-known procedures of
Interpolation and Cut Elimination.  We are motivated in part by the
desire to understand why a tautology might be `hard to prove'.  Given
a proof we associate to it a logical graph tracing the flow of
formulas in it (Buss, 1991) (The idea of using the flow of occurrences
to study the structure of proofs is fundamental in the work of
Jean-Yves Girard (Girard, 1987)).  We show some general facts about
logical graphs such as acyclicity of cut-free proofs and acyclicity of
contraction-free proofs (possibly containing cuts), and we give a
proof of a strengthened version of the Craig Interpolation Theorem
based on flows of formulas.  We show that tautologies having minimal
interpolants of {\it non-linear} size (i.e. number of symbols) must
have proofs with certain precise structural properties. We then
analyse the transformation of logical flow graphs during the procedure
of cut elimination and show that given a proof $\Pi$ and a cut-free
form $\Pi '$ associated to it (obtained by a particular cut
elimination procedure), certain subgraphs of $\Pi '$ which are logical
graphs (i.e. graphs of proofs) correspond to subgraphs of $\Pi$ which
are logical graphs for the same sequent. This locality property of cut
elimination leads to new results on the complexity of interpolants,
which {\it cannot} follow from the known constructions proving the
Craig Interpolation Theorem.


______________________________________________________________________________


TITLE: Some Combinatorics behind Proofs

AUTHOR: A. Carbone -- ale@logic.tuwien.ac.at

Submitted for publication


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'.)