Unless stated otherwise, all talks will take place in room A97 of the Exakte Wissenschaft Building (ExWi) at the University of Bern.
Schedule
Date | Time | Speaker | Title |
---|---|---|---|
16.11.2023 | 13:30-15:00 | Borja Sierra-Miranda, University of Bern | Intuitionistic Gödel-Löb Logic: a cyclic view |
30.11.2023 | 13:30-15:00 | Nina Frasa | Relativized proofs and the P ≠ NP-conjecture (Bachelor Thesis) |
4.12.2023 | See at SGSLPS webpage | Mirna Džamonja | Logic Transfer Principles in Mathematics and Computer Science; Abstract Logics, Infinite and Finite Models |
7.12.2023 | 13:30-15:00 | Noah Maggio, Raphael Feer |
Analysing FastPay (Bachelor Thesis) Analysing Inter-Blockchain Communication (Bachelor Thesis) |
14.12.2023 | Set at APT webpage | - | Symposium: Advances in Proof Theory |
Abstracts
Intuitionistic Gödel-Löb Logic: a cyclic view
Borja Sierra-Miranda
Cyclic proofs are finite proofs that are allowed to have some leaves with backedges to an internal node below the leaves. These are called cyclic leaves and provide a controlled form of non-wellfounded reasoning. In this talk we will introduce the well-known logic iGL, an intuitionistic version of Godel-Lob modal logic, and we will define a cyclic proof system for it. Using similar methods to Shamkanov seminal work on cyclic GL we will prove the equivalence of the cyclic and a standard finitary systems. During the process we will notice that, unlike in GL but as usual in cyclic proof theory, there is a necessity of controlling the possible loops appearing in proofs. At the end we will discuss possible extensions of the methodology that we are currently working on.