The motivation for Core Logic is explained. Its system of proof is set out. It is then shown that, although the system has no Cut rule, its relation of deducibility obeys Cut with epistemic gain.

The papers where Gerhard Gentzen introduced natural deduction and sequent calculi suggest that his conception of logic differs substantially from the now dominant views introduced by Hilbert, Gödel, Tarski, and others. Specifically, (1) the definitive features of natural deduction calculi allowed Gentzen to assert that his classical system nk is complete based purely on the sort of evidence that Hilbert called ?experimental?, and (2) the structure of the sequent calculi li and lk allowed Gentzen to conceptualize completeness as a question (...) about the relationships among a system's individual rules (as opposed to the relationship between a system as a whole and its ?semantics?). Gentzen's conception of logic is compelling in its own right. It is also of historical interest, because it allows for a better understanding of the invention of natural deduction and sequent calculi. (shrink)