The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them

Ekaterina Komendantskaya, Dmitry Rozplokhas, Henning Basold

In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen's classical and intuitionistic calculi…