Small Workshop on "Theory and Application of Deep Inference"
June 21, 2007
(INRIA Sophia Antipolis)
(University of Saskatchewan)
(University of Bath)
Tom E. Gundersen
(University of Bath)
Séverine Maingaud (PPS, Paris)
Michel Parigot (PPS, Paris)
Christian Retoré (LABRI, Bordeaux)
Alexis Saurin (LIX, Palaiseau)
Straßburger (LIX, Palaiseau)
Every speaker has a slot of 40 minutes. These 40 minutes consist of a
talk of 25 minutes and a following discussion of 15 minutes.
Title: Deep sequents for modal logic
Let a pure proof system informally be one in which inference rules
only operate on things which correspond to formulas of the logic.
Gentzen's sequent calculus for classical logic is pure: the commas on
the left are conjunction, the ones on the right conjunction and they
are separated by an implication. All systems in the calculus of
structures are of course pure.
There are many approaches to a proof theory for modal logics. The most
successful, by several criteria, is the one based on labelled
sequents, where in some sense Kripke semantics is built into the proof
system. These proof systems are not pure. The question is whether we
can build a similarly successful pure proof theory. I'll talk about
some progress towards that.
Title: Proof-length speed-ups
in deduction modulo
In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37
years before: there exists arithmetical
formulae that are provable in first order arithmetic, but whose
shorter proof in second order arithmetic is arbitrarily smaller than
any proof in first order. On the other hand, resolution for higher
order logic can be simulated step by step in a first order narrowing
and resolution method based on deduction modulo, whose paradigm is to
separate deduction and computation to make proofs clearer and shorter.
We first prove that it is possible to find formulae whose smaller
proof in natural deduction modulo a very simple rewrite system is
unboundedly smaller than any proof in pure natural deduction. Then, we
show that i+1-th order arithmetic can be linearly simulated into
i-th order arithmetic modulo some confluent and terminating rewrite
system. We also prove that there exists a speed-up between i-th
order arithmetic modulo this system and i-th order arithmetic
without modulo. These two results allows us to prove that the
speed-up conjectured by Gödel does not come from the deductive part of
the proofs, but can be expressed as simple computation, therefore
justifying the use of deduction modulo as an efficient first order
setting simulating higher order.
Tom E. Gundersen
(joint work with Alessio Guglielmi)
Title: Normalisation Control in Deep Inference Via Atomic Flows
We introduce diagrams, called 'atomic flows', that forget much of the
syntactic structure of derivations and only retain causal relations
between atoms. Using atomic flows on propositional logic, we can
design and control several normalisation procedures. In particular, we
can obtain cut elimination as a special case of more general normal
forms. This technique only relies on substituting derivations in the
place of atoms, similarly to natural deduction, and not on permuting
inference steps, as in the sequent calculus. Because they abstract
away from most syntactic details, atomic flows allow for very simple
control of normalisation procedures, which would be otherwise
cumbersome in the bare syntax. We operate in deep inference, a very
general methodology, where normalisation is more difficult to control
than in other syntactic paradigms.
Title: Combinatorial proof invariants
Proofs Without Syntax [Ann. Math. '06]
introduced polynomial-time checkable combinatorial proofs for
classical propositional logic. This sequel approaches Hilbert's
Problem with combinatorial
proofs as abstract invariants for sequent calculus proofs, analogous
to homotopy groups as abstract invariants for topological spaces.
The paper lifts a simple, strongly normalising cut elimination from
combinatorial proofs to sequent calculus, factorising away the
mechanical commutations of structural rules which litter traditional
syntactic cut elimination.
Sequent calculus fails to be surjective onto combinatorial proofs: the
paper extracts a semantically motivated closure of sequent calculus
from which there is a surjection, pointing towards an abstract
combinatorial refinement of Herbrand's
(Article available on the web: Pdf)
Title: Herbrand's Theorem and the sequent calculus
A typical proof of Herbrand's theorem involves Gentzen's Midsequent
theorem (the sharpened Hauptsatz), but such a proof does not yield the
full theorem -- rather, it yields the theorem for sequences of
formulae in prenex normal form.
In "An introduction to proof theory" (Handbook of Proof Theory) Buss
gives a proof of the full theorem using the notion of an "Herbrand
Proof", which is incorrect. I will give a corrected proof: a
procedure which, for any cut-free proof in GS yields an Herbrand proof
of the same conclusion. In order to show admissibility of the
contraction rule we use a notion of "deep contraction" similar to that
of the calculus of structures. I will then extend this procedure to
proofs containing cuts, effectively giving a cut-elimination procedure
for Herbrand proofs.
Finally, I will give some examples of the use of Herbrand proofs as an
invariant on GS derivations, showing which proofs are identified.
Title: Categorical equivalences on derivations in
intuitionistic multiplicative linear logic with unit
Structural proof theory applies to category theory insofar as its
syntactical methods enable the study of terms representing morphisms in free
categories. As to category theory, it provides relevant semantics to
equivalences of derivations usually considered in proof theory. I will
illustrate this interplay by addressing the question of coherence in free
and non-free symmetric monoidal closed categories (SMCCs), and of its
proof-theoretical formulation in the sequent calculus for intuitionistic
multiplicative linear logic (IMLL) with unit. The equality of canonical
natural transformations in a SMCC model induces an equivalence on terms in
the free SMCC that can be formulated as an equivalence on derivations. The
proof-theoretical analysis of such equivalences leads to their
axiomatization by sets of "critical pairs" of derivations. In the free case,
this axiomatization implies that the equivalence induced by the SMCC
structure on cut-free derivations coincides with inter-permutability,
suggesting a way towards the definition of proof-nets for IMLL with unit.
Title: Perfect matchings and directed cographs:
proofnets for pomset logic and the origins of deep inference
In this talk I will recall pomset logic, in a graph theoretical
version which encodes structured contexts a primitive system which
lead Alessio Guglielmi to BV-calculus.
I will present the proof-net calculus with cut-elimination and its
denotational semantics for which we can show that a proofnet is
correct if and only the computation of its semantics is an allowed
I will end with an old but still open graph theoretical conjecture
which would ensure the equivalence of Pomset Logic and BV.
Title: From deep inference to proof nets, revisited
An important observation of "From deep
inference to proof nets" is that cut elimination is losing
information, when seen from the viewpoint of buraucracy A, B, and C in
deep inference derivations.
In this talk I will show that the slogan "cut elimination is losing
information" is independent from deep inference. I will also show how
arbitrary deductive proofs (in sequent calculus, calculus of
structures, or in Frege systems) are translated into proof
graphs. This includes the extension rule, which can be made
independent from the cut.