 ‘Natural deduction’ designates a type of logical system described initially in Gentzen (1934) and Jaśkowski (1934). It also designates the type of reasoning that these logical systems embody. A fundamental part of natural deduction, and what (according to most writers on the topic) sets it apart from other proof methods, is the notion of a “subproof” — parts of a proof in which the argumentation depends on temporary premises (hypotheses “assumed for the sake of argument”). In the Fitch-Jaśkowski presentation of natural deduction, subproofs are marked off in a way that makes them immediately visible in a written proof; with other presentations it takes a bit more work to pick out the formulas forming a subproof. Although formalisms differ, an underlying idea is that one is able to “make an assumption A and see that it leads to conclusion X”, and then conclude that if the A were true, then so would X be. (There are also various other types of subproof that we discuss.) Research in this area has concentrated on such topics as (a) Can all natural deduction proofs be put into some “normal form”?, (b) Do different systems of logic require radically different types of logical rules?, (c) If different logics require radically different types of logical rules, does this show that some logics are “better” than others in some sense?, and (d) Can the features that might make some logics be “better” than others be employed to characterize the meaning of logical terms (and perhaps others) in natural language?