Natural Deduction

A Calculus $\mathcal{ND}_0$ which tries to mimic human argumentation for theorem proving. It uses these Inference Rules to introduce and eliminate connecitves:

For the implication introduction rule we use a Local Hypothesis $A$ which we use to derive $B$ by natural deduction. We then discharge the local hypothesis by introducing the implication. This mode of reasoning is also called Hypothetical Reasoning.

We also write $\mathcal{H} \vdash_{\mathcal{ND_0}} \mathrm{C}$ when there is a natural deduction derivation tree whose leaves are in the assumptions $\mathcal{H}$ and the root is the conclusion $C$.

If we have some assumptions and the assumption $A$ we can conclude $B$ if and only if we can conclude $A\rightarrow B$ from the assumptions.

Some more Inference Rules: