Combinatorial proofs

Hi,

this message is mainly for Francois and Lutz, I guess.

I just had a look at the paper below, which I think is very 
interesting. I think it has a very close relationship with your 
recent work on classical logic's proof nets, and the author should be 
made aware of that, I believe.

More in general, an interesting question could be: is it possible to 
distill a combinatorial proof from a deep inference proof? By 
distillation, I mean some sort of normalisation process that throws 
away the deductive steps and just retains the `essence' of a proof.

For example, suppose you have a proof in KS: colours (again in the 
sense of the paper below) are clearly given by the identity axioms. 
Suppose you start from the top of the proof and remove instances of 
rules one by one, going down this way: you follow the atoms and 
propagate down the colourings, when you have contraction you just 
join them, etc. If you do this to the obvious Pierce's law proof, you 
get the combinatorial proof in the paper. (One has to be careful 
about dealing with edges associated to conjunction; I suspect Hughes 
could simplify a bit his condition, here.)

Is this property true in general? Is it peculiar to CoS or does it 
also work for the sequent calculus? The idea looks neat (getting 
`semantic proofs' by *throwing away* bureaucracy), is it already 
mentioned anywhere else?

Please, give me feedback on this stuff and then perhaps we get in 
touch with Hughes. (By the way, Charles, do you know him? He looks 
like your scientific brother to me.)

Ciao,

-Alessio


Paper: math.LO/0408282
Date: Fri, 20 Aug 2004 17:52:06 GMT   (16kb)

Title: Proofs Without Syntax
Authors: Dominic Hughes
Comments: 6 pages
Subj-class: Logic; Combinatorics
MSC-class: 03B05; 05C99
\\
  ``Mathematicians care no more for logic than logicians for mathematics.''
[Augustus De Morgan, 1868]
  Proofs are traditionally syntactic, inductively generated objects. This paper
presents an abstract mathematical formulation of propositional calculus
(propositional logic) in which proofs are combinatorial (graph-theoretic),
rather than syntactic. It defines a *combinatorial proof* of a proposition P as
a graph homomorphism h : G -> G(P), where G(P) is a graph associated with P,
and G is a coloured graph. The main theorem is soundness and completeness: P is
true iff there exists a combinatorial proof h : G -> G(P).
\\ ( http://arXiv.org/abs/math/0408282 ,  16kb)