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.
|Title of host publication||First-Order Logic Revisited|
|Editors||V F Hendricks, F Neuhaus, S Andur Pederson, U Scheffler, H Wansing|
|Number of pages||16|
|Publication status||Published - 2004|