Workshop 2018

Workshop on Proof Theory and its Applications

Ghent, September 6-7, 2018

The 1st Workshop on Proof Theory and its Applications, organised under the auspices of The Proof Society, will bring together researchers on proof theory and its applications. The aim of the meeting is to reflect on the mission of The Proof Society, through a series of invited and contributed talks, as well as panel discussions.

The mission of TPS has been stated as

To support the notion of proof in its broadest sense, through a series of suitable activities; to be therefore inclusive in reaching out to all scientific areas which consider proof as an object in their studies; to enable the community to shape its future by identifying, formulating and communicating it most important goals; to actively promote proof to increase its visibility and representation.

Invited Speakers

The following researchers have accepted to speak at the workshop:

Andrew Arana (Université Paris 1 – Panthéon-Sorbonne)
Rosalie Iemhoff (Utrecht University)
Dale Miller (Inria Saclay and LIX)
Paulo Oliva (Queen Mary University of London)
Pavel Pudlák (Czech Academy of Sciences)
Michael Rathjen (University of Leeds)
Albert Visser (Utrecht University)


Thursday (September 6, 2018):

Time Event
09:00 – 09:10 Opening
09:10 – 10:00 Rosalie Iemhoff (invited): Negative results in proof theory
10:00 – 10:30 Break
10:30 – 10:45 Cerna: A Formalism for Proof Transformation in the Presence of Induction
10:45 – 11:00 Jafarrahmani: Denotational semantics of Linear Logic with least and greatest fixpoints
11:00 – 11:15 Heijltjes: Proof nets for first-order additive linear logic
11:15 – 11:40 Break
11:40 – 12:30 Dale Miller (invited): Focused sequent calculus proof systems
12:30 – 14:30 Lunch
14:30 – 15:20 Andrew Arana (invited): Takeuti’s finitism and his proof of the consistency of arithmetic [slides]
15:20 – 15:30 Break
15:30 – 15:45 Dinis: Proof mining of the proximal point algorithm with multi-parameters [slides]
15:45 – 16:00 Strassburger: Syntactic Proofs versus Combinatorial Proofs
16:00 – 16:15 Cheng: Incompleteness for higher order arithmetic and the limit of incompleteness [slides]
16:15 – 16:30 Setzer: A model for the extended predicative Mahlo Universe [slides]
16:30 – 17:00 Break
17:00 – 18:00 Panel discussion (chair: Matthias Baaz)
18:00 – TPS AGM

Friday (September 7, 2018):

Time Event
09:10 – 10:00 Pavel Pudlák (invited): Incompleteness in the finite domain [slides]
10:00 – 10:30 Break
10:30 – 10:45 Golan: Assertions, Denials, Suppositions, and Uniformity
10:45 – 11:00 Abzianidze: A Natural Tableau System for a Natural Language
11:00 – 11:15 Ilic: A sequent calculus for a positive relevant logic with necessity
11:15 – 11:40 Break
11:40 – 12:30 Paulo Oliva (invited): From intuitionistic affine logic to classical logic, and back
12:30 – 14:30 Lunch
14:30 – 15:20 Michael Rathjen (invited): Bounds for the Strength of the Graph Minor and the Immersion Theorem
15:20 – 15:30 Break
15:30 – 15:45 Pakhomov: Ordinal Analysis of Kripke Platek Set Theory via Schmerl Formula [slides]
15:45 – 16:00 Engler: Conceptual reduction of theories: A strengthening of relative interpretation
16:00 – 16:15 Aguilera: Some short and long games
16:15 – 16:30 Kolmakov: Axiomatizing provable n-provability [slides]
16:30 – 17:00 Break
17:00 – 17:50 Albert Visser (invited): Kindergarten Provability Logic
17:50 – 18:00 Closing


Jozef Plateauzaal, Faculty of Engineering and Architecture, Jozef Plateaustraat 22, 9000 Ghent, Belgium

A map can be found here.

Practical Information and Registration

  • Workshop: September 6-7, 2018
  • Deadline for registration: July 1, 2018
  • Deadline for abstract submission: July 1, 2018
  • No­ti­fi­ca­tion of paper ac­cep­tance: July 15, 2018
  • To register and submit an abstract please download the linked registration form and follow the instructions given there.
  • No fees will be involved.
  • For accommodation we suggest to consult the information of the Visit Ghent website.

Local organizing committee

  • Arnold Beckmann, Swansea University
  • David Belanger, Ghent University
  • David Fernández-Duque, Ghent University
  • Lenny Neyt, Ghent University
  • Rafal Urbaniak, Ghent University
  • Andreas Weiermann, Ghent University (Chair)


For any ques­tion re­garding the event you can con­tact the or­ga­nizing com­mittee at or

Program committee

  • Bahareh Afshari, University of Gothenburg
  • Matthias Baaz, TU Wien
  • Arnold Beckmann, Swansea University (Chair)
  • Lev Beklemishev, Steklov Mathematical Institute
  • Balthasar Grabmayr, Humboldt University Berlin
  • Rosalie Iemhoff, Utrecht University
  • Joost Joosten, University of Barcelona
  • Antonina Kolokolova, Memorial University of Newfoundland
  • Norbert Preining, Accelia Inc.
  • Andreas Weiermann, Ghent University

Traveling to Ghent

Ghent has different names in different languages: “Gent” in Dutch, “Ghent” in English, and “Gand” in French. This is important to know if you are traveling from France (especially if you are buying your ticket in France), where they usually only use the French name “Gand.”

The main train station in Ghent is called:

  • “Gent-Sint-Pieters” in Dutch;
  • “Ghent-Saint-Peter’s” in English;
  • “Gand-Saint-Pierre” in French.

Once you reach the station, you can take Tram Line 1 towards the city center (centrum).

If you are traveling internationally by train, you will get a better price (and an assured place) by buying your ticket in advance.

If you are flying to Brussels Airport, there is a train station in the airport and you can buy a ticket to Ghent on the spot.

Things to watch out for:

  • Some trams in Ghent announce the stops, and some do not.
  • “Genk” with a “k” is a different city entirely; do not go to Genk by mistake!

Impressions from the Workshop