3. Introducing variant rules

Variant rules

We can avoid the need for a subcomputation box if we augment our basic set of rules with an extra implication-introduction rule of the form:

$$\frac{B}{A\to B}(\to I2)$$

This variant implication-introduction rule avoids the need for a subcomputation box in the cases where the consequent of the implication is already part of the current proof.

Using the form above, we can write the proof $B⊢A\to B$ as:

$$\begin{array}{rlrlrl}& 1.& & B& & \text{data}\\ & 2.& & A\to B& & \text{from }(1.)\text{ and }(\to I2)\end{array}$$

Variant disjunction elimination rules ($\vee E1$) ($\vee E2$)

Variant disjunction elimination rules

The variant disjunction elimination rules, $\vee E1$ and $\vee E2$ are: ?

$$\frac{A\vee B,\neg A}{B}(\vee E1)\frac{A\vee B,\neg B}{A}(\vee E2)$$Link to original

Variant negation elimination rules ($\neg E1$) ($\neg E2$)

Variant negation elimination rules

The variant negation elimination rules, $\neg E1$ and $\neg E2$ are: ?

$$\frac{\neg \neg A}{A}(\neg E1)\frac{\neg A\to B,A\to B}{B}(\neg E2)$$Link to original

Variant implication introduction rules ($\to I1$) ($\to I2$)

Variant implication introduction rules

With $(\vee I)$, we can get from $\neg A$ to $\neg A\vee B$ and $B$ to $\neg A\vee B$, which we know are equivalent to $A\to B$. Using $(\to I1)$ we can derive an implication whose antecedent is false, and using $(\to I2)$ we can derive an implication whose consequence is true: ?

$$\frac{\neg A}{A\to B}(\to I1)\frac{B}{A\to B}(\to I2)$$Link to original

Variant implication elimination rules ($\to E1$)

Variant implication elimination rules

We can use $(\to E1)$ to write an implication in terms of disjunction and negation: ?

$$\frac{A\to B}{\neg A\vee B}(\to E1)$$Link to original

Examples

title: Example 1
The proof as below:
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&P \lor Q &&\text{data} \\
			&2. &&\neg Q &&\text{data} \\
			&3. &&P \rightarrow R &&\text{data} \\
			&4. &&P \rightarrow P &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{P} \\
				&4.1 &&P &&\text{assumption} \\
				&4.2 &&P &&\text{from } (4.1)
			\end{aligned}
		} \\
		\begin{aligned}
			&5. &&Q \rightarrow P &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{array}{l}
				\begin{aligned}
					& && && &&\underline{P} \\
					&5.1 &&Q &&\text{assumption} \\
					&5.2 &&\neg P \rightarrow Q &&\text{subcomputation box}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{Q} \\
						&5.2.1 &&\neg P &&\text{assumption} \\
						&5.2.2 &&Q &&\text{from } (5.1)
					\end{aligned}
				} \\
				\begin{aligned}
					&5.3 &&\neg P \rightarrow \neg Q &&\text{subcomputation box}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{\neg Q} \\
						&5.3.1 &&\neg P &&\text{assumption} \\
						&5.3.2 &&\neg Q &&\text{from } (2)
					\end{aligned}
				} \\
				\begin{aligned}
					&5.4 &&\neg P &&\text{from } (5.2), (5.3), \text{ and } (\neg E)
				\end{aligned}
			\end{array}
		} \\
		\begin{aligned}
			&6. &&P &&\text{from } (1.), (4.), (5.), \text{ and } (\lor E) \\
			&7. &&R &&\text{from } (3.), (6.), \text{ and } (\rightarrow E)
		\end{aligned}
		\text{ (without variant)}		
	\end{array}
$$
 
Can be represented instead using the variant rule:
$$
	\frac{A \lor B, \neg B}{A} \, (\lor E2)
$$
 
Giving us the new proof:
$$
	\begin{aligned}
		&1. &&P \lor Q &&\text{data} \\
		&2. &&\neg Q &&\text{data} \\
		&3. &&P \rightarrow Q &&\text{data} \\
		&4. &&P &&\text{from } (1.), (2.), \text{ and } (\lor E2) \\
		&5. &&R &&\text{from } (3.), (4.), \text{ and } (\rightarrow E) \\
	\end{aligned}
	\text{ (with variant)}	
$$

title: Example 2: Show that $A \lor B, \neg B \vdash A$
$$
	\begin{aligned}
		&1. &&A \lor B &&\text{data} \\
		&2. &&\neg B &&\text{data} \\
		&3. &&A &&\text{from } (1.), (2.), \text{ and } (\lor E2) \\
	\end{aligned}
$$

title: Example 3: Show that $A \land \neg A \vdash B$
$$
	\begin{aligned}
		&1. &&A \lor \neg A &&\text{data} \\
		&2. &&A &&\text{from } (1.) \text{ and } (\land E) \\
		&3. &&\neg B \rightarrow A &&\text{from } (2.) \text{ and } (\rightarrow I2) \\
		&4. &&\neg A &&\text{from } (1.) \text{ and } (\land E) \\
		&5. &&\neg B \rightarrow \neg A &&\text{from } (4.) \text{ and } (\rightarrow I2) \\
		&6. &&B &&\text{from } (3.), (5.), \text{ and } (\neg E)
	\end{aligned}
$$

title: Example 4: Show that $\neg A, B \rightarrow C \vdash A \rightarrow C$
$$
	\begin{aligned}
		&1. &&\neg A &&\text{data} \\
		&2. &&A \rightarrow C &&\text{from } (1.) \text{ and } (\rightarrow I1)
	\end{aligned}
$$