Collegium Logicum 2012: Structural Proof Theory

Theme

The topic of the workshop is structural proof theory and it is open to anyone interested. Proposals for contributed talks, including talks on work in progress and discussions of open problems, are welcome.

Invited Talks

• Alex Simpson: Cyclic Arithmetic (in context)

  In this talk, I shall extend Peano Arithmetic by admitting a class of finitely presented infinite proofs, formalizing a notion of proof by infinite descent (Fermat’s “descente infinie”). The main result is that, in doing so, we get Peano Arithmetic back again.The point of this somewhat circular exercise is to shed light on a more general problem: that of relating “cyclic proofs” to proofs with explicit (co)induction. Insofar as time permits, I shall discuss some instances of this broader problem, by considering various contexts in which notions of “cyclic proof” arise.

• Paulo Oliva: Algorithms from proofs in classical arithmetic and analysis

  In this talk we will see how one can use Gödel’s functional interpretation combined with the negative translation in order to obtain effective algorithms from non-constructive proofs in arithmetic and analysis. We will start by looking at the interpretation of classical principle such as excluded middle and the drinker’s paradox. Then, the technique will be further explained through the analysis of concrete proofs of the following theorems

  • infinite pigeon-hole principle
  • bounded collection
  • no injection from Baire space to natural numbers

  Most of the analysis will make use of the so-called selection functions and their corresponding product [1,2], which are also going to be explained in the talk.

  [1] M. Escardó and P. Oliva. Sequential games and optimal strategies
  Proceedings of the Royal Society A, 467:1519-1545, 2011

  [2] M. Escardó and P. Oliva. Selection functions, bar recursion and backward induction
  Mathematical Structures in Computer Science, 20(2):127-168, 2010

Contributed Talks

• Federico Aschieri: Interactive realizability for Peano Arithmetic with Skolem Axioms
• Matthias Baaz: On the limits of analyticity
• Jaime Gaspar: Completeness of Heyting/Peano arithmetic with the ω-rule
• Stéphane Gimenez: The reducibility method in Calculus of Structures
• Stéphane Graham-Lengrand: Psyche, an implementation of focused sequent calculus used as a generic proof-search platform
• Nicolas Guenot: On the computational contents of proofs in deep inference
• Willem Heijltjes: An Atomic Lambda Calculus
• Alexander Leitsch: CERES for First-Order Schemata
• Tomer Libal: Choosing Most General Unifiers in Higher-order Resolution
• Revantha Ramanayake: Labelled tree sequents, Tree hypersequents and Nested (Deep) Sequents
• Fabien Renaud: News from ProofCert
• Giselle Reis: CERES in Intuitionistic Logic
• Lara Spendier: Automated Support for the Investigation of Paraconsistent and Other Logics
• Lutz Straßburger: From Proof Nets to Virtual Tensors — Making Semi-star-autonomous Categories Free
• Daniel Weller: Deskolemization, Equality and Logical Complexity

Participants

Schedule

Thursday, November 15

Friday, November 16

Support and Organization

This workshop will be hosted by the Laboratoire d’Informatique (LIX) and by INRIA Saclay. Funding is provided by the ANR-FWF project STRUCTURAL and by the Kurt Gödel Society.

The workshop is being organized by Stefan Hetzl and Kaustuv Chaudhuri.