Učitavanje video playera...
01:21:02
Borja Sierra Miranda: Local-progress proof theory
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.
