A Fitch-style Proof Theory

A number of proof theories are possible. We present first a Fitch-style system of natural deduction, $\cal F$. (Such systems are commonly referred to simply as ``natural" systems.) In $\cal F$, each of the truth-functional connectives has a pair of corresponding inference rules, one for introducing the connective, and one for eliminating the connective. Proofs (or, as we will call them derivations) proceed in sequence line by line, each line number incremented by 1. Each line not only includes a line number, but also a formula (the one deduced at this line) and, in the rightmost column, a rule cited in justification for the deduction. We use a vertical elipsis $\vdots$ to indicate the possible presence of 0 or more lines in the derivation. Here is the rule for elminating a conjunction:

$$\begin{array}{r\vert ll} \vdots & \vdots & \vdots\\ k & \ph... ... \wedge \mbox{ Elim}\\ \vdots & \vdots & \vdots\\ \end{array}$$

Intuitively, what does this rule say? It says that if at line k in some derivation you have somehow obtained a conjunction $\phi \wedge \psi$, then at a subsequent line m, one can infer to either of the conjuncts alone.^3.1 Now here is the rule that allows a conjunction to be introduced; intuitively, it formalizes the notion that from the fact that two propositions are the case it follows that the conjunction of these two propositions is also true.

$$\begin{array}{r\vert ll} \vdots & \vdots & \vdots\\ k & \ph... ...\wedge \mbox{ Intro}\\ \vdots & \vdots & \vdots\\ \end{array}$$

A key rule in $\cal F$ is supposition, according to which you are allowed to assume any wff at any point in a derivation. The catch is that you must signal your use of supposition by setting it off typographically. Here is the template for supposition:

$$\begin{array}{r\vert lll} \vdots & & \!\!\! \hspace{.05in} \... ... \!\!\!\vline \hspace{.05in} \vdots & \:\:\vdots\\ \end{array}$$

Often a derivation will be used to establish that from some set $\Phi$ of propositional formulas a particular formula $\phi$ can be derived. In such a case, $\Phi$ will be given as suppositions, and the challenge will be to derive $\phi$ from these suppositions. To say that that $\phi$ can be derived from a set of formulas $\Phi$ in $\cal F$ we will write

$$\Phi \vdash_{{\tiny\mbox{$\cal F$}}} \phi.$$

Here is a derivation that puts to use the rules presented above and establishes that $\{(P \wedge Q) \wedge R\} \vdash_{{\tiny\mbox{$\cal F$ }}} Q$:

$$\begin{array}{r\vert ll} 1 & (P \wedge Q) \wedge R & \mbox{g... ...\mbox{ Elim}\\ 3 & Q & 2 \: \wedge \mbox{ Elim}\\ \end{array}$$

Now here is a slightly more complicated rule, one for introducting a conditional. It basically says that if you can carry out a sub-derivation in which you suppose $\phi$ and derive $\psi$ you are entitled to close this sub-derivation and infer to the conditional $\phi \rightarrow \psi$.

$$\begin{array}{r\vert lll} \vdots & & \!\!\!\!\!\! \vdots &\\... ...tarrow \psi & & k-m \: \rightarrow \mbox{ Intro}\\ \end{array}$$

As we said, in a Fitch-style system of natural deduction, the rules come in pairs. Here is the rule for eliminating conditionals:

$$\begin{array}{r\vert ll} k & \phi \rightarrow \psi &\\ \vdo... ...s\\ m & \psi & k, l \: \rightarrow \mbox{ Elim}\\ \end{array}$$

Here is the rule for introducing $\vee$:

$$\begin{array}{r\vert ll} \vdots & \vdots & \vdots\\ k & \ph... ...: \vee \mbox{ Intro}\\ \vdots & \vdots & \vdots\\ \end{array}$$

And here is the rule for eliminating a disjunction:

$$\begin{array}{r\vert lll} \vdots & & \!\!\!\!\!\! \vdots &\\... ...p & \chi & & \: k, l-m, n-o \: \vee \mbox{ Elim}\\ \end{array}$$