Contributed Talks 18
Chair: Takako Nemoto
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
14:00 
Alexis Saurin, CraigLyndon interpolation as cutintroduction 
After Craig’s seminal results on interpolation theorem [1], a number and variety of prooftechniques, be they semantical or prooftheoretical, have been designed to prove interpolation theorems. Among them, Maheara’s method [3] is specific due to its wide applicability to a range of logics admitting cutfree complete proof systems. We reconsider here Maehara’s method and show how, by a close inspection of the proof, one can extract a “proofrelevant” interpolation theorem for firstorder linearlogic stated as follows: if \(\pi\) is a cutfree proof of \(A \vdash B\), we can find (i) a formula \(C\) in the common vocabulary of \(A\) and \(B\) and (ii) proofs \(\pi_1\) of \(A \vdash C\) and \(\pi_2\) of \(C \vdash B\) the proof \(\pi'\) obtained from \(\pi_1\) and \(\pi_2\) with a cut inference on \(C\) cutreduces \(\pi\). We then show that this can be decomposed in two phases: (i) a bottomup phase which decorates the sequents followed by (ii) a top down phase which solves the interpolation problem, synthesizing the interpolant by introducing cuts. We then consider extensions of the approach to other settings (classical and intuitionistic logics, or the \(\mu\)calculus) and discuss the computational content of the result which is related to a proofrelevant refinement of Prawitz’ proof of the interpolation theorem [4] in natural deduction already investigated by Čubrić in the 90’s [2] for the simply typed \(\lambda\)calculus. Details are provided in an extended version [5]. Bibliography


14:25 
Ricardo JaimesUrbán, Cut elimination for provability logic. An unmechanized proof. 
Authors: Ricardo JaimesUrbán and Favio E. MirandaPerea In 2015, Brighton proved the cut elimination theorem for provability logic using regress trees [1]. Six years later, Goré, Ramanayake and Shillito pointed out that Brighton’s proof is indirect and has some technical problems and presented a computer assisted proof (CAP), for the sequent calculus GLS, using the Coq proof assistant [2]. To achieve this, they defined an auxiliary sequent calculus (PSGLS) wich has a terminating proof search procedure. Even though CAPs have became more popular lately, they are not universally accepted. Thus, in the aim of conciliating CAPs and traditional proofs, and due to the fact that a general translation between both seems to be impossible, González Huesca and MirandaPerea proposed the concept of transitional proofs [3] which provides a translation methodology suitable for particular cases. As a first step towards the construction of a transitional proof, we try to unmechanize the proof of cut elimination for GLS, but since Coq has received several updates, many of the libraries and tactics used by the authors have been deprecated. Due to this and other retrocompatibility issues, we were not able to review the whole proof script and consequently we were not able to complete the transitional proof. Therefore, we opted to do a new proof, based on the sketches presented in [2], by proving all the lemmas and previous results that are enunciated without proof and including all the steps omitted by the authors in the main proof. The success of this approach shows that all the reasoning done by the proof assistant can in fact be translated to a traditional proof. Another remarkable difference is that we proved cut elimination for PSGLS and concluded it for GLS as a corollary, unlike the original Coq proof where the authors worked in GLS and invoked PSGLS instances of the rules when needed. Bibliography


14:50 
Oriola Gjetaj, A Goodstein independence result for $ID_2$ 
Authors: David FernandezDuque, Oriola Gjetaj and Andreas Weiermann The Goodstein principle is a natural numbertheoretic theorem. The original process works by writing natural numbers into nested exponential kbase normal form, then successively raising the base to k + 1 and subtracting 1 from the result. Such sequences always reach zero, but this fact is unprovable in Peano arithmetic. Drawing from previous results in the literature, we consider canonical representations with respect to the FastGrowing Extended Grzegorczyk hierarchy \(\{F_{a}\}_{a<\psi_0(\varepsilon_{\Omega+1})}\). Normal forms are written as basek representations and the component \(a\) is written as base\(\psi_0(\cdot)\) collapsing function up to BachmannHoward ordinal. We use an ordinal assignment to show that this sequence terminates and yields an independence result from the theory of \(ID_2\). This is part of joint work with A. Weiermann and D. Fern'andezDuque on exploring normal form notations for the Goodstein principle. Bibliography


15:15 
Joost Joosten, Feferman interpretability and applications 
Authors: Joost Joosten, Luka Mikec and Albert Visser Given two theories \(U,V\) with axiomsets that are polytime decidable so that \(U\) interprets \(V\) – we write \(U\rhd V\) – we will define a theory \(V'\) in the spirit of Feferman provability so that \(V'\) is extensionally the same as \(V\) and so that \(U\rhd V \to \Box_{ {\sf S}^1_2} (U\rhd V')\) becomes a trivial matter. We apply this technique to prove the two hierarchies of principles from [1] to be arithmetically sound in any theory containing \({\sf S}^1_2\). Bibliography


15:40 
Vlad Lazar, Modal logic semantics for ordinal analysis of bar induction 
There has been a notable increase in the utilization of provability logic within prooftheory, most of which is derived form Giorgi Japaridze’s polymodal logic (GLP) [2]. An interesting restriction of GLP called reflection calculus (RC) [3] was developed by Lev Beklemishev to facilitate the prooftheoretic analysis of PA. This method proved to be quite powerful, and has since been expanded upon. Our work is primarily focused on an extension of reflection calculus called \(\omega\)RC, whose motivation comes from recent developments in ordinal analysis by iterated reflection principles [4]. The grammar of \(\omega\)RC is as follows: \[A:= p\;\;\top\;\;A\wedge B\;\; \Diamond^1_{\alpha\geq 1} A\;\;\Diamond^2_{\alpha\geq 2}\;\; \downarrow A \text{ , where } \alpha\leq \omega.\]Intended arithmetical interpretation:
where M ranges over the countably coded \(\omega\)models of ACA\(_0\). Given the equivalence between bar induction and \(\omega\)model reflections [1], the aim of this modal logic is to aid in the prooftheoretic analysis of the theory of bar induction (BI). Our current results are on the semantic development of \(\omega\)RC. We have managed to prove Kripkecompleteness for this logic, and are currently working on combinatorial techniques for analyzing the relationship between formulas. Bibliography
