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}{⊢}_{\mathcal{N}{\mathcal{D}}_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\to B$ from the assumptions.

Some more Inference Rules: