SD 2014 INFORMAL PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. We present a new correctness criterion for Multiplicative Linear Logic (MLL) proof nets. Our criterion generalizes a criterion recently introduced by Mogbil and Jacobé de Naurois in order to characterize the space complexity of the correctness problem for M(E)LL: while the Mogbil-Naurois criterion relies on a single switching, our criterion completely abstracts from the notion of switchings.

This is done in two steps. First we define dependency graphs on proof nets rather than correction graphs, as in Mogbil-Naurois, making them switching-independent. Then, we partition our criterion in two parts: one part deals exclusively with tensor, axiom and cut inferences while the other one deals with the structure of par inferences by requiring dependency graphs to be acyclic flowgraphs (or SDAG). We finally compare both notions of dependency graphs.

ABSTRACT. In the paper ``Structural Cut Elimination'', Pfenning gives a proof of the admissibility of cut for intuitionistic and classical logic. The proof is remarkable in that it does not rely on difficult termination metrics, but rather a nested lexicographical induction on the structure of formulas and derivations. A crucial requirement for this proof to go through is that contraction is not an inference rule of the system. Because of this, it is necessary to change the inference rules so that contraction becomes an admissible rule rather than an inference rule. This change also requires that weakening is admissible, hence it is not directly applicable to logics in which only contraction is admissible (e.g. relevance logic).

We present a sequent calculus which admits a unified structural cut elimination proof that encompasses Intuitionistic MALL and its affine, strict and intuitionistic extensions. A nice feature of the calculus is that, for instance, moving from linear to strict logic is as simple as allowing the presence of a rule corresponding to contraction.

ABSTRACT. Ludics is a theory that may be considered, at first glance, as a Brouwer-Heyting- Kolmogorov interpretation of Logic as a formula is denoted by the set of its proofs. More primitively, Ludics is a theory of interaction that models (a variant of) secondorder multiplicative-additive Linear Logic. A formula is denoted by a set of objects called a behaviour, a proof by an object that satisfies some criteria. Our aim is to analyze the structure of behaviours in order to better understand and refine the usual notion of formula or type. More precisely, we study properties that guarantee a behaviour to be multiplicatively decomposable.

ABSTRACT. "...mathematicians care no more for logic than logicians for mathematics." - Augustus de Morgan, 1868

Formal proofs are traditionally syntactic, build inductively from symbolic inference rules. This paper reformulates classical first-order logic with proofs which are combinatorial rather than syntactic. A combinatorial proof of a formula F is a graph on a variant formula F′ which satisfies geometric properties. For example, an edge between the two Ps in ∀xPx ⇒ ∀yPy constitutes a combinatorial proof o ∃x(P ⇒∀yPy).

Combinatorial proofs provide a canonical abstraction of Gentzen’s sequent calculus LK: the correctness of a combinatorial proof can be verified in polynomial time (conjectured linear), and there is a function from LK proofs to combinatorial proofs which identifies many LK proof.

This paper summarizes ongoing work on a sequel to Proofs Without Syntax [Annals of Mathematics, 2006], which introduced propositional combinatorial proofs.

ABSTRACT. We construct a categorical model of Linear Logic, whose objects are all the locally convex and separated topological vector spaces endowed with their weak topology. Linear proofs are interpreted as continuous linear functions, and non-linear proofs as sequences of monomials. The duality in this interpretation of Linear Logic does not come from an orthogonality relation, thus we do not complete our constructions by a double-orthogonality operation. This yields into an interpretation of polarities with respect to weak topologies.