Transitivity of Deducibility
Neil W. Tennant · Oxford University Press eBooks · 2017
We reformulate M, I, and C in our preferred format: parallelized elimination rules whose major premises have no proof-work above them. An effective binary operation [ , ] of reduction is recursively defined on proofs. It secures Cut-Elimination for each of M, I, C, and Classical Core Logic. The common form is: If proof P uses premises X to prove A and proof P′ uses A with other premises Y to prove B, then [P,P′] uses premises in X,Y to prove [either ⊥ or] B. Cut-Elimination for the orthodox systems omits the last bit of bracketed material; while Cut-Elimination for the two core systems includes it. So the core systems can enjoy epistemic gains that the orthodox systems cannot. We end by showing how to extract from any intuitionistic proof a core proof of a result at least as strong; and how to do the same with any classical proof.