Cut for Classical Core Logic

Abstract In an earlier paper in this journal I provided detailed motivation for the constructive and relevant system of Core Logic ; explained its main features; and established that, even though Cut is not a rule of the system, nevertheless Cut is admissible for it, and indeed with potential epistemic gain. If Π is a proof of the sequent Δ : A , and Σ is a proof of the sequent Г, A : θ , then there is a computable reduct Π, Σ of some subsequent of the ‘overall target sequent’ Δ, Г : θ . In the constructive case the potential epistemic gain consists in the possibility that the subsequent in question be a proper subsequent of Δ, Г : θ , and indeed even logically stronger than Δ, Г : θ . In this paper it is established that Cut is likewise admissible for Classical Core Logic, which is obtained from Core Logic by adding a suitably relevantized form of the rule of Classical Dilemma. In the classical case there is an additional feature of potential epistemic gain: the proof Π, Σ might have a lower degree of non-constructivity than do Π and Σ.