 ‘Natural deduction’ designates a type of logical system described initially in Gentzen (1934) and Jaśkowski (1934). 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. That is, we are justified in concluding without any assumption that “if A then X”, i.e., \((A\rightarrow X)\), because we could create this subproof. This assumption-making can occur also within some previously-made assumption, so there needs to be some method that prevents mixing up of embedded conclusions. That example is but one of a number of different types of “subordinate proof” types that can be found in textbooks as well as in research contributions. In the Suppes-Lemmon style of proof — which is often or even usually called a style of natural deduction — the proofs can and probably should instead be seen as operating with sequents, and so (by our stipulative definition) is not really a system of natural deduction, but (i) it resembles other forms of natural deduction (as in Gentzen’s sequent calculi \(\mathcal{NJ}\) and \(\mathcal{NK}\)) by having elimination rules, rather than the rules for the introduction of formulas on the left side of sequence (in this it mirrors Gentzen’s sequent calculi), and (ii) when one works with it in practice it feels like natural deduction. (We discuss this style in Section 4.) Various of these different styles will be illustrated in this survey.