After Craig’s seminal results on interpolation theorem [1], a number and variety of proof-techniques, be they semantical or proof-theoretical, 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 cut-free complete proof systems.

We reconsider here Maehara’s method and show how, by a close inspection of the proof, one can extract a “proof-relevant” interpolation theorem for first-order linear-logic stated as follows: if \(\pi\) is a cut-free 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\) cut-reduces \(\pi\).

We then show that this can be decomposed in two phases: (i) a bottom-up 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 proof-relevant 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

1. William Craig,Three uses of the Herbrand-Gentzen theorem in relating model theory andproof theory,Journal of Symbolic Logic,vol. 22(3) (1957), pp. 269–285.
2. Djordje Čubrić,Results in categorical proof theory,PhD thesis, McGill University,1993.
3. Shoji Maehara,On the interpolation theorem of Craig,Sûgaku, vol 12(4) 1960.
4. Dag Prawitz,Natural Deduction: A Proof-Theoretical Study,Dover Publications, Mineola, N.Y., 1965.
5. Alexis Saurin, Interpolation as cut introduction,draft, 2024, www.irif.fr/_media/users/saurin/pub/interpolation_as_cut_introduction.pdf

Authors: Ricardo Jaimes-Urbán and Favio E. Miranda-Perea

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 Miranda-Perea 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.
This research is being supported by UNAM-DGAPA-PAPIIT grant IN101723.

Bibliography

1. J. Brighton,Cut Elimination for GLS Using the Terminability of its Regress Process,Journal of Philosophical Logic,vol. 45 (2), pp.147–153.
2. R. Goré, R. Ramanayake, I. Shillito,Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq,Automated Reasoning with Analytic Tableaux and Related Methods(Anupam Das and Sara Negri, editors),Springer International Publishing,Cham,2021,pp.299–313.
3. F. E. Miranda-Perea, L. d. C. González Huesca,On the Conciliation of Traditional and Computer-Assisted Proofs,Philosophy of Computing(Bj{"o}rn Lundgren and Nancy Abigail Nu{ {n}}ez Hernández, editors),Springer International Publishing,Cham,2022,pp.73–112.

Authors: David Fernandez-Duque, Oriola Gjetaj and Andreas Weiermann

The Goodstein principle is a natural number-theoretic theorem. The original process works by writing natural numbers into nested exponential k-base 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 Fast-Growing Extended Grzegorczyk hierarchy \(\{F_{a}\}_{a<\psi_0(\varepsilon_{\Omega+1})}\). Normal forms are written as base-k representations and the component \(a\) is written as base-\(\psi_0(\cdot)\) collapsing function up to Bachmann-Howard 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'andez-Duque on exploring normal form notations for the Goodstein principle.

Bibliography

1. T. Arai, S. Wainer, and A. Weiermann, Goodstein sequences based on a parametrized Ackermann-Péter function, The Bulletin of Symbolic Logic, vol. 27 (2021), no. 2, pp. 168–186.
2. W. Buchholz, E. A. Cichon, and A. Weiermann, A uniform approach to fundamental sequences and hierarchies, Mathematical Logic Quarterly, vol. 40 (1994), pp. 273–286.
3. A. Weiermann,Investigations on slow versus fast growing: how to majorize slow growing functions nontrivially by fast growing ones,Arch. Math. Logic,vol. 34 (1995), no. 5, pp. 313–330.
4. R.L. Goodstein, On the restricted ordinal theorem, J. Symbolic Logic,vol. 9, (1944), pp. 33–41.
5. L. Kirby and J. Paris., On the restricted ordinal theorem, Bulletin of The London Mathematical Society, 14 ,(1982), no. 4, pp. 285–293.

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

1. E. Goris, and J. J. Joosten.,Two new series of principles in the interpretability logic of all reasonable arithmetical theories,Journal of Symbolic Logic,vol. 85 (1), pp. 1–25, 2020.

There has been a notable increase in the utilization of provability logic within proof-theory, most of which is derived form Giorgi Japaridze’s poly-modal logic (GLP) [2]. An interesting restriction of GLP called reflection calculus (RC) [3] was developed by Lev Beklemishev to facilitate the proof-theoretic 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:

Intended arithmetical interpretation:

• \(\top\) is the system ACA\(_0\).
• \(\Diamond^1_\alpha A\) is ACA\(_0\) + RFN\(_{\Pi^1_\alpha} (A)\).
• \(\Diamond^2_\alpha A\) is ACA\(_0\) + \(\omega\)-RFN\(_{\Pi^1_\alpha} (A)\).
• \(\downarrow A\) is the theory: \(\{\varphi\in\Pi^1_\infty\;|\;A\vdash \forall M(M\models \varphi)\},\)

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 proof-theoretic analysis of the theory of bar induction (BI). Our current results are on the semantic development of \(\omega\)RC. We have managed to prove Kripke-completeness for this logic, and are currently working on combinatorial techniques for analyzing the relationship between formulas.

Bibliography

1. Friedman, Harvey, Some systems of second order arithmetic and their use, Proceedings of the international congress of mathematicians (Vancouver, BC) (1975), pp. 235–242.
2. Japaridze, Giorgi K, The polymodal logic of provability, Intensional Logics and Logical Structure of Theories: Material from the fourth Soviet–Finnish Symposium on Logic, Telavi (1985), pp. 16–48.
3. Beklemishev, Lev, Positive provability logic for uniform reflection principles, Annals of Pure and Applied Logic,vol. 165 (2014), no. 1, pp. 82–105.
4. Pakhomov, Fedor and Walsh, James, Reflection ranks and ordinal analysis, The Journal of Symbolic Logic,vol. 86 (2021), no. 4, pp. 1350–1384.