For questions concerning natural deduction, a formal proof system studied in proof theory. A natural deduction proof starts with a set of premises and applies introduction and elimination rules to arrive at the conclusion. This tag is not specific to any particular logic, classical or intuitionistic, propositional or allowing quantifiers.
This tag is for questions concerning natural deduction and proofs in natural deduction.
Natural deduction is a formalization in proof theory. A proof in natural deduction starts from a set of assumptions (formulae) and applies a series of introduction and elimination rules to arrive at the conclusion.
There are separate introduction rules and elimination rules for each logical connective (such as and ($\land$) or not ($\lnot$)). The introduction rules give some conditions under which we may assert the connective: for example, from $A$ and $B$ we may assert $A \land B$. The elimination rules give some conclusions we may assert from the connective: for example, from $A \land B$, we may conclude $A$. Thus in forming a proof, the introduction rules are used to introduce new logical connectives, and elimination rules are used to eliminate logical connectives.
The specific introduction and elimination rules used vary, depending on what logic (for example, classical, intuitionistic or minimal) we are working in.
