Semantic A-translation and Super-consistency entail Classical Cut Elimination

Lisa Allali, Olivier Hermant

We show that if a theory R defined by a rewrite system is super-consistent, the classical sequent calculus modulo R enjoys the cut elimination property, which was an open question.…