Proof Theory Virtual Seminar

Videos & Slides

This page contains a list of past talks. Where available, there is a link to the speaker's slides and to a video of the talk on the seminar's Youtube channel.

Keita Yokoyama (JAIST), 17 February 2021
Forcing interpretation, conservation and proof size
Slides |
The notion of relative interpretation is one of the essential tools of proof theory. In [1], Avigad demonstrated how forcing can be understood in the context of proof theory and how it is related to relative consistency or conservation proofs. Indeed, one may see that forcing is a generalization of a relative interpretation by means of the Kripke semantics.
Moreover, such an interpretation usually provides a feasible (polynomial) proof transformation as digested in [2]. In this talk, we will overview such ideas and show that many conservation theorems for systems of second-order arithmetic can be converted to non-speedup theorems.

[1] J. Avigad, Forcing in proof theory. Bull. Symbolic Logic 10 (2004), no. 3, 305-333.
[2] J. Avigad, Formalizing forcing arguments in subsystems of second-order arithmetic. Ann. Pure Appl. Logic 82 (1996), no. 2, 165-191.
[3] L. A. Kolodziejczyk, T. L. Wong and K. Yokoyama, Ramsey's theorem for pairs, collection, and proof size, submitted.
Sara Negri (Genova), 3 February 2021
A proof-theoretic approach to formal epistemology
Slides |
(joint work with Edi Pavlovic) Ever since antiquity, attempts have been made to characterize knowledge through belief augmented by additional properties such as truth and justification. These characterizations have been challenged by Gettier counterexamples and their variants.
A modern proposal, what is known as defeasibility theory, characterizes knowledge through stability under revisions of beliefs on the basis of true or arbitrary information (Hintikka (1962), Stalnaker (1998)). A formal investigation of such a proposal calls for the methods of dynamic epistemic logic: well-developed semantic approaches to dynamic epistemic logic have been given through plausibility models of Baltag and Smets (2008) and Pacuit (2013), but a corresponding proof theory is still in its beginning.
We shall recast plausibility models in terms of the more general neighbourhood models and develop on their basis complete proof systems, following a methodology introduced in Negri (2017) and developed for conditional doxastic notions in Girlando et al. (2018).
An inferential treatment of various epistemic and doxastic notions such as safe belief and strong belief will give a new way to study their relationships; among these, the characterization of knowledge as belief stable under arbitrary revision will be grounded through formal labelled sequent calculus derivations.
Georg Moser (U Innsbruck), 20 January 2021
Herbrand Complexity and Hilbert's Epsilon Calculus
Slides | Video |
In the talk I will make use of two results on the epsilon calculus over a language with equality. First, I'll show how the epsilon calculus can be used to derive upper bounds on the Herbrand complexity of first-order logic with equality, independent on the propositional structure of the first-order proof. Second, I'll indicate how to obtain (non-elementary) upper bounds on the Herbrand complexity, if first-order logic is extended by equality axioms of epsilon terms. This follows from a careful study of the complexity of the epsilon elimination procedure in the presence of epsilon equality axioms.
This is joint work with Kenji Miyamoto.
Matthias Baaz (TU Vienna), 16 December 2020
Cut Elimination as Error Correcting Device
Slides | Video |
In mathematical proofs axioms and intermediary results are often represented by their names. It is however undecidable whether such a description corresponds to an underlying proof. This implies that there is sometimes no recursive bound of the complexity of the simplest underlying proof in the complexity of the abstract proof description, i.e. the abstract proof description might be non-recursively simpler. This however does not apply to cut-free proofs, where it is easy to decide whether there is a corresponding proof and it is easy to reconstruct a most general proof in case there is one. This means that cut elimination on an abstract proof description might be considered as error correcting device. We compare various elimination procedures on abstract proof descriptions and describe their relation to the first epsilon-theorem.
Ulrich Kohlenbach (TU Darmstadt), 2 December 2020
Proof Mining and the Lion-Man game
Slides | Video |
We analyze, based on an interplay between ideas and techniques from logic and geometric analysis, a pursuit-evasion game. More precisely, we focus on a discrete lion and man game with an epsilon-capture criterion.
We prove that in uniformly convex bounded domains the lion always wins and, using ideas stemming from proof mining, we extract a uniform rate of convergence for the successive distances between the lion and the man. As a byproduct of our analysis, we study the relation among different convexity properties in the setting of geodesic spaces.
Joint work with Genaro López-Acedo and Adriana Nicolae.
Albert Visser (Utrecht University), 18 November 2020
Fixed Points meet Löb's Rule
Slides | Video |
The modal part of the work reported in this talk is in collaboration with Tadeusz Litak.
For a wide class of theories we have the Second Incompleteness Theorem and, what is more, Löb's rule, also in cases where the third Löb Condition L3 *provable implies provably provable* (aka 4) fails. We will briefly indicate some examples of this phenomenon. What happens when we do have Löb's Rule but not L3? It turns out that we still have a lot. For example, the de Jongh-Sambin-Bernardi Theorem on the uniqueness of fixed points remains valid. So, e.g., Gödel sentences are unique modulo provable equivalence. On the other hand, explicit definability of fixed points fails. An arithmetical example of the non-explicit-definability of the Gödel sentence is still lacking. (I do have an arithmetical example where the Gödel sentence is equivalent to the consistency of inconsistency but not to consistency.)
We discuss the relevant logic: the Henkin Calculus, to wit, K plus Löb's rule plus boxed fixed points. This logic turns out to be synonymous to the mu-calculus plus the minimal Henkin sentence, which expresses well-foundedness. So, results concerning the mu-calculus, like uniform interpolation, can be transferred to the Henkin Calculus.
Valeria de Paiva (Topos Institute Berkeley), 4 November 2020
Benchmarking Linear Logic
Slides | Video |
Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. The availability of such libraries of problems for non-classical logics is very limited. So in work with Olarte, Pimentel, and Reis (2018) we proposed a library for benchmarking Girard's (propositional) intuitionistic linear logic, starting from Kleene's initial collection of intuitionistic theorems. However, we want to use these theorems not for checking the efficiency of different theorem provers for the logic, but instead, I wanted to investigate the structure of the space of proofs of linear theorems, in different variants of linear logic. Having learned of Tarau's work on 'generating' intuitionistic implication theorems, I suggested to him that we could calculate the 'linear' implicational theorems. His program turned out to be very adept and in a few hours produces almost 8 billion "small" implicational linear theorems. Given this scale, we decided we could do some machine learning of intuitionistic linear logic, and the results seem impressive.
(This is joint work with Paul Tarau, presented by him at ICLP2020, CLA2020)
Michael Rathjen (University of Leeds), 21 October 2020
Far beyond Goodman's Theorem?
Slides | Video |
Goodman's Theorem says that Heyting arithmetic in all finite types, HA^\omega, augmented by the axiom of choice for all finite types, AC(FT), is conservative over HA. This classical result has been extended to many other intuitionistic theories (e.g. by Beeson) and even to intuitionistic Zermelo-Fraenkel set theory with large set axioms (by Friedman and Scedrov). The question I'll be pondering in this talk is whether the finite types are the limit. What about adding the axiom of choice for all the transfinite dependent types as they appear in Martin-Löf type theory (actually already in Hilbert's "Über das Unendliche")?
Sam Buss (University of California at San Diego), 7 October 2020
Propositional proof systems and bounded arithmetic for logspace and nondeterministic logspace
Slides | Video |
We discuss logics for proof systems that correspond to deterministic logspace computation and to nondeterministic logspace computation. The first component is propositional proof systems in which lines are either decision diagrams, represented as decision trees with extension variables, or nondeterministic decision diagrams, represented by decision trees with nondeterministic choices and extension variables. The second component is the bounded arithmetic theories VL and VNL.
This is part of a program of developing logics for weak classes of computational complexity. A highlight of this kind of work is tight relationships between propositional proof systems, (second-order) theories of bounded arithmetic, and computational complexity. Our results are in part revamped versions of prior theories for logspace and nondeterministic logspace due to Zambella, Cook, Nguyen, and Perron. The talk will survey past results, and report on joint work-in-progress with Anupam Das and Alexander Knop.