Borja Sierra Miranda (University of Bern) выступит с докладом на семинаре НУГ "Доказательства и модели"

Borja Sierra Miranda (University of Bern, Institute of Computer Science, Logic and Theory Group) выступит с докладом "Non-wellfounded master modality: from cut admissibility to cut elimination" на семинаре "Современные проблемы математической логики" 11 октября 2024 г.

Доклад будет на английском языке. Для получения ссылки на зум необходимо заранее написать А.В. Кудинову на почту kudinov.andrey at gmail.com

Abstract:

In a previous talk, we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The method consisted of splitting the proof into nicely behaved fragments. This paper extends our method to proofs based on simple trace conditions. The main idea is to split the system with the trace condition into infinitely many local-progress calculi that together are equivalent to the original trace-based system. This provides cut elimination, via cut admissibility, using only basic tools  of structural proof theory and corecursion, which is needed due to the non-wellfounded character of proofs. We will employ our method to obtain syntactic cut elimination for K+, the system of modal logic with the master modality.