tag:blogger.com,1999:blog-4987609114415205593.post8949694074502772571..comments2021-06-19T18:51:04.369+01:00Comments on M-Phi: Cut Elimination and ContractionJeffrey Ketlandhttp://www.blogger.com/profile/01753975411670884721noreply@blogger.comBlogger1125tag:blogger.com,1999:blog-4987609114415205593.post-61542854855015997632011-04-19T00:16:34.400+01:002011-04-19T00:16:34.400+01:00I'm probably missing something, since I don...I'm probably missing something, since I don't know the background, but just to get things rolling... If the contraction rule is only admissible (not explicit), then the proof can be rewritten without contraction. So you can forget about all the instances of contraction in proving cut elimination. An example of this approach is Negri & Plato's proof of cut admissibility for G3ip. Indeed, most (all?) of the proofs of cut admissibility in Negri & Plato involve induction on both height of the cut and weight (e.g. complexity) of the cut formula. Is this the kind of thing you have in mind, following Petersen?timhttps://www.blogger.com/profile/02753779297869692581noreply@blogger.com