2. Examples using the basic rules

Examples using the basic rules

title: Example 1: Show that $(A \lor B) \rightarrow C \vdash (A \rightarrow C) \land (B \rightarrow C)$.
 
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&(A \lor B) \rightarrow C &&\text{data} \\
			&2. &&(A \rightarrow C) &&\text{subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{C} \\
				&2.1 &&A &&\text{assumption} \\
				&2.2 &&A \lor B &&\text{from } (2.1) \text{ and } (\lor I) \\
				&2.3 &&C &&\text{from } (2.2), (1.) \text{ and } (\rightarrow E)
			\end{aligned}
		} \\
		\begin{aligned}
			&3. &&(B \rightarrow C) &&\text{subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{C} \\
				&3.1 &&B &&\text{assumption} \\
				&3.2 &&A \lor B &&\text{from } (2.1) \text{ and } (\lor I) \\
				&3.3 &&C &&\text{from } (3.2), (1.) \text{ and } (\rightarrow E)
			\end{aligned}
		} \\
		\begin{aligned}
			&4. &&(A \rightarrow C) \land (B \rightarrow C) &&\text{from } (2.), (3.) \text{ and } (\land I)
		\end{aligned}
	\end{array}
$$

title: Example 2: Show that $A \lor B, \neg B \vdash A$.
 
In this case, we use the [[Natural Deduction elimination of disjunction]].
 
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&A \lor B &&\text{data} \\
			&2. &&\neg B &&\text{data} \\
			&3. &&A \rightarrow A &&\text{subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{A} \\
				&3.1 &&A &&\text{assumption} \\
				&3.2 &&A &&\text{from } (3.1)
			\end{aligned}
		} \\
		\begin{aligned}
			&4. &&B \rightarrow A &&\text{subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{array}{l}
				\begin{aligned}
					& && && &&\underline{A} \\
					&4.1 &&B &&\text{assumption} \\
					&4.2 &&\neg A \rightarrow B &&\text{subcomputation below}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{B} \\
						&4.2.1 &&\neg A &&\text{assumption} \\
						&4.2.2 &&B &&\text{from } (4.1)
					\end{aligned}
				} \\
				\begin{aligned}
					&4.3 &&\neg A \rightarrow \neg B &&\text{subcomputation below}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{\neg B} \\
						&4.3.1 &&\neg A &&\text{assumption} \\
						&4.3.2 &&\neg B &&\text{from } (2.)
					\end{aligned}
				} \\
				\begin{aligned}
					&4.4 &&A &&\text{from } (4.2), (4.3), and (\neg E)
				\end{aligned} \\
			\end{array}
		} \\
		\begin{aligned}
			&5. &&A &&\text{from } (1.), (3.), (4.), \text{ and } (\lor E)
		\end{aligned} \\
	\end{array}
$$
 
$$
	\frac{A \lor B, \neg B}{A} \, (\lor E2) \text{ will be introduced as a variant rule later}
$$

title: Example 3: Show that $\vdash \neg (A \land \neg A)$ (this shows that $\neg (A \land \neg A)$ is a tautology)
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&A \land \neg A \rightarrow A &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{A} \\
				&1.1 &&A \land \neg A &&\text{assumption} \\
				&1.2 &&A &&\text{from } (1.1) \text{ and } (\land E)
			\end{aligned}
		} \\
		\begin{aligned}
			&2. &&A \land \neg A \rightarrow \neg A &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{A} \\
				&2.1 &&A \land \neg A &&\text{assumption} \\
				&2.2 &&\neg A &&\text{from } (2.1) \text{ and } (\land E)
			\end{aligned}
		} \\
		\begin{aligned}
			&3. &&\neg (A \land \neg A) &&\text{from } (1.), (2.), and (\neg I)
		\end{aligned} \\
	\end{array}
$$

title: Example 4: Show that $A \land \neg A \vdash B$
**This shows you how to derive any conclusion from an inconsistent set.**
 
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&A \land \neg A &&\text{data} \\
			&2. &&\neg B \rightarrow A &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{A} \\
				&2.1 &&\neg B &&\text{assumption} \\
				&2.2 &&A &&\text{from } (1.) \text{ and } (\land E)
			\end{aligned}
		} \\
		\begin{aligned}
			&3. &&\neg B \rightarrow \neg A &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{\neg A} \\
				&3.1 &&\neg B &&\text{assumption} \\
				&3.2 &&\neg A &&\text{from } (1.) \text{ and } (\land E)
			\end{aligned}
		} \\
		\begin{aligned}
			&4. &&B &&\text{from } (2.), (3.), and (\neg E)
		\end{aligned}
	\end{array}
$$