[Back]

M. Baaz:
"Cut Elimination as Error Correcting Device";
Talk: Proof Theory Virtual Seminar, online (invited); 2020-12-16.

In mathematical proofs axioms and intermediary results are often represented by their names. It is however undecidable whether such a description corresponds to an underlying proof. This implies that there is sometimes no recursive bound of the complexity of the simplest underlying proof in the complexity of the abstract proof description, i.e. the abstract proof description might be non-recursively simpler. This however does not apply to cut-free proofs, where it is easy to decide whether there is a corresponding proof and it is easy to reconstruct a most general proof in case there is one. This means that cut elimination on an abstract proof description might be considered as error correcting device. We compare various elimination procedures on abstract proof descriptions and describe their relation to the first epsilon-theorem.