Gallery
One main ambition of my work is
to understand how formal proofs
should be written down.
This simple question is related to a myriad
of fascinating problems at the
interface of proof theory,
games semantics, n-dimensional algebra,
and mathematical physics.
For instance, I like to think that « game semantics »
is not just another « semantics » for proofs.
I prefer to see it as a « syntax ».
Of course, this « game syntax »
is a new kind of syntax, which does not look
like the previous ones -- especially if one thinks
of Frege's ideography, Gentzen's sequent calculus,
or even Girard's proof-nets.
This new brand of diagrammatic syntax
is at the same time
a « combinatorics »
of proofs, akin to the familiar structure
of topological knots in mathematics.
The wonderful thing is that we have
at our disposal, today, a large amount
of tools coming from algebra and
mathematical physics, to analyze that kind
of diagrammatic situation.
I am confident that this point of view
will deeply transform Proof Theory
as well as Programming Language Semantics.
There are also good reasons to believe
that this fresh air coming from algebra
and mathematical physics will not be confined to Proof Theory:
it should also benefit the other fields
of mathematical logic.
Here, I will limit myself to showing you
a few diagrams which I have drawn in my work.
Some of them describe proofs,
others describe structures of connectives
or modalities.
I have decided to show them here
mainly to entertain my non-mathematician friends.
However, I will briefly indicate to the specialist
reader what kind of mathematical structures
are depicted below.
A proof in string diagrams
This is the proof that the conjunction of
the double negations of two formulas
A and B implies the double negation
of the conjunction of the two formulas.
Note that the trajectories of the negations
R and L coincide with the strategy associated
to the proof in « game semantics ».
Modalities as boxes
I like to draw modalities as boxes, surrounding proofs:
intuitively, the modality encapsulates the proof, and
indicates a modal attitude to the external world.
Interestingly, these modal boxes have a clear
algebraic meaning: they model various kinds
of (monoidal) functors between (monoidal) categories.
I use this diagrammatic language to describe how
a proof duplicates another proof in linear logic.
This leads to nice diagrams, as this one above,
describing a contraction node interacting with
the principal door of an exponential box in linear logic.
The methodology extends quite nicely to broader
territories -- leading to natural extensions of
flowchart diagrams in programming language design.
The structure of recursion
Martin Hyland and Masahito Hasegawa have
shown around 1996 that this construction
defines a (parametric) fixpoint operator
in any cartesian category with a trace operator --
typically, the category of Scott domains
and continuous functions.
This amounts to showing that the diagram above
is equal to the diagram below.
Can you guess the diagrammatic rules
which enable to transform the first
diagram into the second one?
The solution appears
here.
The structure of logical implication
The diagram shows that every adjunction
does not simply define a monad, but in
fact what I like to call a «parametric monad ».
This structure captures precisely
the property of a logical implication
defined by negative translation --
as in the case of language defined by continuations.
Associativity of the parametric monad
is established thanks
to a series of diagrams, involving this one:
