JAIST Logic Workshop Series

# Workshop on Proofs as Processes II

12–14 July 2015

Noto, Ishikawa, Japan

The Workshop on Proofs as Processes II is a continuation of last years Workshop on Proofs as Processes. It will be held with the support of the Kurt Gödel Society, and a Royal Society Daiwa Anglo-Japanese Foundation International Exchanges Award in Noto, Ishikawa, from 12‐14 July, 2015.

After the successful development of a Hypernatural deduction system (LICS 2015 etc) we will continue our long-term project on extending the classical Curry-Howard correspondence to hypersequent calculus and parallel processes. It will bring together scientists working on the various related fields who are interested in collaborating in the project.

## Participants

• Arnold Beckmann (Swansea University, Wales, UK)
• Matthias Baaz (University of Technology, Vienna, Austria)
• Alexander Leitsch (University of Technology, Vienna, Austria)
• Norbert Preining (JAIST, Nomi, Japan)
• Giselle Reis (INRIA, France)

## Program

• Matthias Baaz: Cut-elimination for prenex cuts in LJ is elementary
• Arnold Beckmann: Hyper Natural Deduction - confluence and term systems
• Alexander Leitsch: Algorithmic introduction of quantified cuts
• Giselle Reis: Linear Logic
• Matthias Baaz: Embarassing Proof Theory

## Discussion and problems (post meeting)

### by Giselle Reis on Linear Logic

• Is linear logic with 2 subexponentials decidable?
• Computational interpretation of linear logic: there is a work on interpreting linear propositions as session types in pi-calculus. More details at this paper.
• Invertibility of inference rules: Following our discussion and the induction proof of invertibility Arnold pointed out, I wrote some notes on the subject (it is mostly for my own reference, but I think it is worth clarifying some details. Link in the email or on request).

### by Alexander Leitsch on Cut Elimination

Note that the problem is fully solved for $\Pi_1$-cuts. The generalization to $\Sigma_1$-cuts and mixtures of $\Pi_1$ and $\Sigma_1$-cuts is easy.
• While the substitutions generated by cut-elimination of $\Pi_2$-cuts have been characterized by some type of grammar (in a recent publication of Afshari, Hetzl and Leigh), the cut-introduction problem remains open - even for a single $\Pi_2$-cut. In particular it is an open question whether there exists a canonic solution (for the second-order problem ) of the schematic extended Herbrand sequent (and if this is not always the case is there a decision procedure for solvability?).
• In the case of general $\Pi_n$-cuts even the syntactic characterization of the substitutions generated by cut-elimination remains an open problem. So far there is no decent grammar formalism known specifying the corresponding set of terms.

### by Matthias Baaz on Proof Theory

• Is there an elementary bound for the complexity of the cut-free proofs wrt the complexity of LK-proofs with only one prenex cut? (Note that such a bound does not exist if the cut is infix.)
• There is an elementary bound for the complexity of cut-free proofs wrt the complexity of LJ-proofs not containing $v$ with prenex cuts only. Show that this result does not hold if $v$ is added.

## Venue

Kinoura Village, 927-1446 Ishikawa, Suzu, Oritomachi Hobu-25

## Contributions and participants

Further participants are asked to contact the organizers.

## Organising Committee

• Arnold Beckmann beckmann at swansea dot ac dot uk
• Norbert Preining preining at jaist dot ac dot jp