Natural deduction presents logic through introduction and elimination rules for each logical connective.
The rule with premises and conclusion retains the first derivation while allowing an unused second assumption. Under the Curry-Howard correspondence, the output term is the first premise term, with the enlarged context. This allows a lambda abstraction whose bound variable does not occur in its body.
From and , implication elimination derives . Under the Curry-Howard correspondence, this is application: from lambda terms and form .
The implication introduction rule discharges a temporary assumption from a derivation of , producing . Under the Curry-Howard correspondence, a body under gives the lambda abstraction . Unused assumptions may also be discharged.
Articles by others on the same topic
Natural deduction is a formal system in logic used to derive conclusions from premises using a set of inference rules. It was developed in the mid-20th century and is widely used in mathematical logic, philosophy, and computer science. The main idea behind natural deduction is to model how humans typically reason about propositions and their relationships. In natural deduction, a proof is structured as a sequence of statements, where each statement is either an assumption (premise) or a conclusion derived from previous statements using inference rules.