Mathematical Foundations of Computation Seminar
Mathematical Foundations of Computation Seminar
Welcome to the webpage of the seminar of the Mathematical foundations of computation group. The seminar in this semester usually takes place on Thursdays at 13:15. To join the seminar mailing list, please contact me.
Samson Abramsky
6/11/2025, Anupam Das (School of Computer Science, University of Birmingham)
30/10/2025, Arnold Beckmann (Department of Computer Science, Swansea University): On the Complexity of Confluence and Church-Rosser Proofs, with an application to Bounded Arithmetic
We investigate confluence and the Church-Rosser property - two well-studied properties of rewriting and the $\lambda$-calculus - from the viewpoint of proof complexity. With respect to confluence, our main contribution is that the size, measured in number of symbols, of the smallest rewrite proof is polynomial in the size of the peak. For the Church-Rosser property we obtain exponential lower bounds for the size of the join in the size of the equality proof. The obtained (worst-case) bounds in both cases are precise. We also study the complexity of proving confluence in the context of the $\lambda$-calculus. Here, we establish an exponential (worst-case) lower bound of the size of the join in the size of the peak. We will explain as a motivation an application of a (yet to be achieved) feasible Church-Rosser property to the separation problem in Bounded Arithmetic. This is joint work with Georg Moser, published in the proceedings of MFCS 2024.
23/10/2025, Erfan Khaniki (Department of Computer Science, University of Oxford): Not all Kripke models of HA are locally PA
Let K be an arbitrary Kripke model of Heyting Arithmetic (HA). For every node k in K, we can view the classical structure at k, M_k, as a model of some classical theory of arithmetic. Let T be a classical theory in the language of arithmetic. We say that K is locally T if and only if, for every k in K, M_k is a model of T. A basic question originating from Troelstra et al. (Notre Dame Journal of Formal Logic, 1986) asks whether every Kripke model of HA is locally PA (Peano arithmetic). In this talk, we construct a rooted Kripke model of HA whose root is not a model of PA, thus answering the question of Troelstra et al. in the negative.
18/7/2025, Katsuhiko Sano (Faculty of Humanities and Human Sciences, Hokkaido University): Craig Interpolation for Bi-intuitionistic Stable Tense Logic
Bi-intuitionistic stable tense logic (BiSKt), introduced by Stell et al. (2016), provides a logical framework for mathematical morphology on graphs consisting of nodes and edges. In this talk, we establish the Craig interpolation theorem for BiSKt from a proof-theoretic perspective -- that is, in terms of a sequent calculus for BiSKt. Although our sequent calculus is not cut-free, applications of the cut rule can be restricted to analytic ones -- namely, those in which the cut formula is a subformula of the conclusion of the cut rule. To establish the Craig interpolation theorem for this calculus, we use a symmetric interpolation method originally proposed by Mints (2001) for the multi-succedent calculus of first-order intuitionistic logic. This method can be seen as a generalization of Maehara's method. Our proof-theoretic approach also simplifies the method developed by Kowalski and Ono (2017) for proving the Craig interpolation theorem in bi-intuitionistic logic. This is a joint work with Hiroakira Ono (JAIST).
10/6/2025, Ondra Ježil (Department of Algebra of the Faculty of Mathematics and Physics, Charles University): Prime Factorization in Models of PV_1
Under a hypothesis on the hardness of factoring, we show that the bounded arithmetic PV_1, corresponding to polynomial-time reasoning, cannot prove that every number has some prime divisor. The result holds even when we extend PV_1 by the sharply bounded choice scheme.