A First Order System with Finite Choice of Premises
Kai Bruennler, Alessio Guglielmi · 2004
We present an inference system for classical first order logic in which each inference rule, including the cut, only has a finite set of premises to choose from. The main conceptual contribution of this paper is the possibility of separating different sources of infinite choice, which happen to be entangled in the traditional cut rule.