# Proof, Computation, Complexity 2018

## Seventeenth International Workshop

July 19-20, 2018, Bonn, Germany

General Information    Invited Speakers    Programme    Contributing Talks    Important Dates    Registration    Past workshops

### News

last-minute changes to programme (none has been rescheduled), programme ends earlier on Thursday

### General Information

#### Aims and Scope

The aim of PCC is to stimulate research in proof theory, computation, and complexity, focusing on issues which combine logical and computational aspects. Topics may include applications of formal inference systems in computer science, as well as new developments in proof theory motivated by computer science demands. Specific areas of interest are (non-exhaustively listed) foundations for specification and programming languages, logical methods in specification and program development including program extraction from proofs, type theory, new developments in structural proof theory, and implicit computational complexity.

#### Venue

The workshop is organized as extra workshop (besides the three major workshops) of the trimester on "Types, Sets and Constructions" of the Hausdorff Research Institute for Mathematics (HIM), see the official announcement on the HIM site. All talks are held in HIM lecture hall, Poppelsdorfer Allee 45, Bonn.

#### Accommodation

Most participants will have arrangements with the HIM. We will therefore refrain from giving further indications.

### Invited speakers

in alphabetic order
Hugo Herbelin: Computing with Gödel's Completeness Theorem
Krivine, followed by Berardi and Valentini, explored in the 90's how to compute with Gödel's completeness using "exploding models" and A-translation. We later gave with Ilik a direct computational formulation of Henkin's proof.
In the talk, we shall study yet another approach to compute with Gödel's completeness theorem by observing that the Kripke forcing translation of the statement of completeness is a statement of completeness with respect to Kripke semantics. Going then the other way round, looking at direct-style provability for the Kripke forcing translation the same way as classical logic can be seen as direct-style provability for the double-negation translation, we obtain a proof of Gödel's completeness with "side effects" whose computational content is to "reify" a proof of validity into a proof of derivability.
Hajime Ishihara: Constructive reverse mathematics: an introduction and recent results
This talk presents an introduction to constructive reverse mathematics (CRM) with some recent results. The aim of CRM is to classify various theorems in intuitionistic, constructive recursive and classical mathematics by logical principles, function existence axioms and their combinations. We review some results in classical reverse mathematics (Friedman-Simpson program), and axioms of intuitionistic and constructive recursive mathematics with their consequences to motivate CRM. Then we present some results of CRM with and without countable choice, and recent results in CRM without countable choice.
Oliver Kullmann: The Science of Brute Force
In SAT solving we have the New and the Old, modern SAT solving versus old-fashioned backtracking (and look-ahead). As the success of the solution of the Pythagorean Triples Problem https://en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem shows, indeed the combination of Old and New can be best in many cases, and I will discuss the landscape of these ideas.
Michael Rathjen: The ubiquity of Schütte's search trees
Progressions of theories along paths through Kleene's $\mathcal O$, adding the consistency of the previous theory at every successor step, can deduce every true $\Pi^0_1$-statement. This was shown by Turing in his 1938 thesis who called these progressions ordinal logics. In 1962 Feferman proved the amazing theorem that progressions based on the uniform reflection principle can deduce every true arithmetic statement. In contrast to Turing's, Feferman's proof is very complicated, involving several cunning applications of self-reference via the recursion theorem.
Using Schütte's method of search trees (or decomposition trees) for ω-logic, however, one can give a rather transparent proof. If time permits, I shall present a general proof-theoretic machinery, based on search trees, for investigating statements about well-orderings from the point of view of reverse mathematics.
Giuseppe Rosolini: Quotient completions and applications
The notion of elementary quotient completion of a Lawvere elementary doctrine introduced by Maietti and Rosolini proved to be a generalization of the notion of the exact completion of a category with finite products and weak equalizers which is a crucial step in the construction of computational models such as Hyland's Effective Topos.
We describe that completion and focus on the special class of elementary doctrines called triposes, introduced by Hyland, Johnstone, and Pitts. We characterize those triposes whose elementary quotient completion is an arithmetic quasitopos, i.e. a quasitopos equipped with a natural number object.
This suggests that the notion of elementary topos may be too strong to model computational aspects of mathematics.

### Programme

The accepted contributed talks:
Thursday July 19, 2018

9.00-10.30 Opening
Invited Speaker 1: Hajime Ishihara
David Cerna

10.30-11.00 coffee break

11.00-13.10 Invited Speaker 2: Hugo Herbelin
Amirhossein Akbar Tabatabai
Tatsuji Kawai

lunch

15.15-16.00 Invited Speaker 3: Giuseppe Rosolini

16.00-16.30 coffee break

16.30-17.50 Hannes Diener & Robert Lubarsky
Josef Berger & Gregor Svindland

Friday July 20, 2018

9.00-10.30 Invited Speaker 4: Michael Rathjen
David Natingga

10.30-11.00 coffee break

11.00-12.20 Takako Nemoto
Iosif Petrakis

lunch

14.30-16.00 Invited Speaker 5: Oliver Kullmann
Lars Kristiansen

16.00-16.30 coffee break

There will also be the opportunity to join the organizers for a dinner on Thursday evening at 7 p.m., in the restaurant Zum Treppchen (the reservation has been confirmed). The participants will be asked if they intend to join (everybody has to pay for herself/himself) before lunch on Thursday.

### Contributing talks

We solicit contributions in the fields of PCC, non-exhaustively described above. Please register a contribution at the EasyChair site for PCC 2018: https://easychair.org/conferences/?conf=pcc20180 (please note the trailing zero). This consists in a title, a short text-only abstract and the PDF file of a LaTeX abstract that fits on one page in format A4. (The latter PDF file is not compulsory on first submission.)

PCC is intended to be a lively forum for presenting and discussing recent work. Progress on a not yet satisfactorily solved problem may well be worth presenting - in particular if the discussions during the workshop might lead towards a solution.

### Important Dates

• Deadline for proposing a contributed talk: May 28, 2018 (AoE), but the submission server remained still open for some days
• Notification of acceptance: June 18, 2018

### Registration

There is no specific registration procedure, and no registration fee will be charged - the coffee breaks are taken care of by the HIM. Lunches and dinners have to be organized by the participants individually, however, there is a suggestion for dinner on Thursday, see above.

### Committees

#### Organizing Committee

Reinhard Kahle, Ralph Matthes, and Peter Schuster

### Past PCC workshops

• PCC 2017 was held in Göttingen, Germany, including an unveiling ceremony of a commemorative plaque for Paul Bernays on his former house.
• PCC 2016 was held in Munich, Germany, including a day-long special session to celebrate the 60th birthday of Ulrich Berger.
• PCC 2015 was held in Oslo, Norway, colocated with the Symposium on the occasion of the retirements of Herman Ruge Jervell and Dag Normann.
• PCC 2014 was held in Paris, France, colocated with TYPES 2014.
• PCC 2013 was held in Toulouse, France, colocated with TYPES 2013.
• PCC 2012 was held in Copenhagen, Denmark.
• PCC 2011 was held in Ghent, Belgium.
• PCC 2010 was held in Bern, Switzerland.
• PCC 2009 was held at LORIA - Nancy, France.
• PCC 2008 was held in Oslo, Norway.
• PCC 2007 was held in Swansea, Wales, colocated with the British Mathematical Colloquium 2007.
• PCC 2006 was held in Ilmenau, Germany.
• PCC 2005 was held in Lisbon as affiliated Workshop to ICALP'05.
• PCC 2004 was held in Dresden in conjunction with the Summer School on Proof Theory and Automated Theorem Proving.
• PCC 2003 was held in Dresden, in conjunction with the Summer School on Proof Theory, Computation, and Complexity.
• PCC 2002 was held in Tübingen.

Page maintained by:

Ralph Matthes
https://www.irit.fr/~Ralph.Matthes/