Journée RÉSEAUX DE
PREUVES
vendredi 22 janvier 2021 LIRMM + online
10:00 - Handsome proof nets
Christian RETORE (Université de Montpellier, LIRMM)
Handsome proof nets identify equivalent proofs as much as possible
--- order of rules, commutativity and associativity of the
connectives. They are simply defined as and edge bicoloured graph
over atoms, consisting in a Red cograph decipting the conclusion
formula and a Blue perfect matching of the whole graph. The
correctness criterion is quite simple: for every cycle alternating
Red and Blue edges the R and B graph contains at lest a chord. Cut
elimination results from the fact that some graph rewriting rules
preserve correctness. So far, this view of proof nets is the only
one to apply to pomset logic, a non commutative extension of
classical logic issued form coherence semantics.
10:30 TBA
Thomas ERHARD (Université Paris 7)
11:15 - A complexity gap between pomset logic and system BV (
joint work with Lutz Strassburger)
Lê Thành Dũng NGUYEN (Université Sorbonne Paris nord, LIPN)
Pomset logic and BV are both logics that extend multiplicative
linear logic (with Mix) with a third connective which is self-dual
and non-commutative. The former uses proof nets while the latter
was the first exampke of a deep inference system. It has long been
conjectured that these two logics are the same. We show that non
only this conjecture is false - there is an explicit counter
example - but there is a fundamental complexity-theoretic reason
for this: provability is a stricly harder problem in pomset logic
than in BV unless NP=coNP.
11:45 - Fantastic connectives and Where to Find Them
Matteo ACCLAVIO (Luxembourg University)
Fantastic connectives and Where to Find Them represents the fruit
of many years' travel and research. [...] The definition of a
'generalised connectives' has caused controversy for decades.
Though this might surprise some first-time students of logic, the
problem might come into clear focus if we take a moment to
consider three types of generalised connectives: synthetic
connectives, connectives-as-partitions and connectives-as-graphs.
[...] We now ask ourselves: which of these creatures is a 'being'
-- that is to say, a creature worthy of legal rights and voice in
logic -- and which is a 'beast'? [...] Jean-Yves Girard, the
founder of Linear Logic, decreed that any connective which admits
a linear and context-free introduction rule, would henceforth be
granted the status of 'multiplicative connective'. [...] As we
see, the mere possession of such a rule, was no guarantee that a
connectives could or would well-behave with respect to
cut-elimination. In a recent joint work with Ross Horne and Lutz
Strassburger, we define 'connectives-as-graphs' in the hope of
creating closer ties between multiplicative linear logic and our
graphical proof system GS. [...] Let us now turn on the one
question that linear logicians ask more than any other when the
conversation turns to our connectives: why do you say that these
objects describe new connectives? ( This talk is based on https://arxiv.org/abs/2012.01102
and https://drops.dagstuhl.de/opus/volltexte/2020/11649/pdf/LIPIcs-CSL-2020-6.pdf
)
12:15- Lunch break
13:30 - Proof nets: representation of syllogisms, representation
of law of categorial grammar
Vito Michele ABRUSCI (Università Roma tre)
I will show and discuss how to represent in terms of (non
commutative) proof-nets:
- the syllogisms considered in ancient, medieval and
modern logic;
- the laws of categorial grammar.
14:00 - Strong Normalization of Elementary Proof-Nets
Olivier LAURENT (ENS Lyon)
We present a proof of strong normalization of proof-nets for
elementary linear logic. It follows the simple pattern of
assigning an ordinal to each proof-net, and proving that this
ordinal value decreases under any reduction step. As it is often
the case with light logic systems, types play no role and only the
geometry (i.e. paths) of the proof-net matters.
14:30 - A reading of Girard's Transcendental Syntax
Boris ENG (Université Sorbonne Paris nord, LIPN)
Following the Geometry of Interaction
programme, Girard's Transcendental Syntax gives the outline of a
finitary, homogeneous and interactive architecture of logic based
on computation. Thomas Seiller and I suggest an attempt at a first
technical development of this programme. As a first step, we
encode multiplicative proof-structures into the Stellar
Resolution, a model of computation based on Robinson's first-order
resolution. We then show how cut-elimination and logical
correctness can be naturally expressed as a non-deterministic
resolution of constraints on addresses refering to the physical
locations of a proof-structure.