Natural Deduction

We extend the Fitch-style system of natural deduction presented for propositional languages by adding rules for the quantifiers and for identity. Our first new rule is universal elimination. In order to present it, we need some new notation: Where $\forall x \phi$ is some universally quantified sentence (recall that a sentence is a formula with no free occurrences of a variable), let $\phi^a_x$ be the result of substituting the constant a for x throughout $\forall x \phi$. Then here is our first new rule:

$$\begin{array}{r\vert ll} k & \forall x \phi &\\ \vdots & \v... ... m & \phi^a_x & k, m \: \: \forall \mbox{ Elim}\\ \end{array}$$

In a Fitch-style system, quantifiers, like the truth-functional connectives, are associated with a pair of rules: one for introducing, and one for eliminating. Accordingly, here is the rule for introducing a universal quantifier (i.e., universal introduction). Notice that this rule includes two restrictions.

Provided that

• a does not occur in an undischarged assumption; and
• a does not occur in $\forall x \phi$:

$$\begin{array}{r\vert ll} k & \phi^a_x &\\ \vdots & \vdots &... ...forall x \phi & k, m \: \: \forall \mbox{ Intro}\\ \end{array}$$