Natural Deduction, The Logical Basis of Axiom Systems

This book is based upon Gentzen's techniques of natural deduction. The
propositional and quantificational rules on which the exposition pivots are
stated essentially as Gentzen stated them, and even the names used for them
are free translations of his names. Gentzen's techniques constitute a very
natural approach to the study of the proofs occurring in axiom systems as well
as a sound basis for the analysis of the properties of formal systems as such.