Na Seminaru za matematičku logiku i računarstvo, u ponedjeljak 31. ožujka 2025. u 17:15 sati, 

Borja Sierra Miranda (University of Bern) održat će predavanje 

 

Local-progress proof theory: admissibility implies eliminability

 

Sažetak: Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is local progress: enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL, Grz or IL.

 

Note that, in non-wellfounded proof theory, the usual proof of admissibility of a rule implying eliminability cannot be performed. This proof relies in finding top-most applications of the rules, which is something that may not exist in non-wellfounded proofs. In this talk, we introduce a method of corecursive translations between local progress calculi which allows us to introduce a new natural definition of admissible rule. This new notion corresponds to eliminability in local-progress calculi, thus providing an easy method to prove cut-elimination. As an example, we will show cut elimination for a non-wellfounded proof calculus of Grz, a result previously proven by Savateev and Shamkanov which follows straightforwardly from our methodology.

 

Seminar će se održati putem aplikacije Zoom. Link i potrebni podaci su ovdje:

 

https://zoom.us/j/96512929513?pwd=pFI2geuwfkXNI71hbidi0T0IMJ5Ssa.1

Meeting ID: 965 1292 9513