**Extension of Formal System ****L****
to ****L**^{*}

Formal system **L**
has three axioms and these are the starting
points for the proof of theorems. Now, the question is what would happen if we
add another axiom in our formal system **L**? We would have more to start from, so
in general we would expect to be able to prove more theorems. All well-formed
formulas which were previously theorems would remain theorems, but perhaps some
well-formed formulas which were not theorems would become theorems.

Definition: Extension

An extension of formal system **L**
is a formal system **L ^{*} **obtained by
altering or enlarging the set of axioms so that all theorem of formal system

((~*A* → ~*B*) →
(*B* → *A*))

without altering the class of theorems.

Note that if we were to extend our formal system **L**
to system with more and more theorems,
the more likely it will be that there will be some well-formed formula * A* such
that both * A* and ~*A* are theorem. Obviously, such a situation will be undesirable.

**Formal Axiomatic Theory L**^{*}

We now extend formal system **L**
to **L**^{*} by replacing Axiom 3 by
above schema. That is, if *A*, *B*, * C* are any well-formed formulas of **L**^{*}, then
following are axioms of **L**^{*}.

Axiom 1. | (A → B) → A |

Axiom 2. | (A → (B → C)) →
((A → B) → (A → C)) |

Axiom 3. | ((~A → ~B) → (B →
A)) |

Deduction Rules of Extend formal system **L**^{*}.

1. Rule of Substitution. | Let A be a formula containing the letter
A.
If A is a well-formed formula, then, after replacing the letter A
everywhere it occurs in it by an arbitrary formula B, w obtain a
well-formed formula. |

2. Rule of Inference. | As before, the only rule of inference of L^{*}
is modus ponens: If A and A → B are well-formed formula, then
B is
also well-formed formula. |

By indicating the axioms and deduction rules of our new formal
system **L**^{*}, we have
completely defined the concept of a well-formed formula in the system **L**^{*}
or of a formula which is deducible in the our extended formal system **L**^{*}.
Utilizing the deduction rules, we can, starting from the new set of axioms,
construct new well-formed formulae and obtain, in this way, every well-formed
formula in our extended formal system **L**^{*}. We now consider some examples in our extend formal system **L**^{*}.

**Lemma 1 ^{*}**. For any well-formed formulas

Proof. We shall construct proof in **L**^{*}.

1. | (~B → (~A → ~B) | Instance of Axiom A1. |

2. | (~A → ~B) → (B → A) | Instance of Axiom A3. |

3. | ((~A→ ~B)→ (B→ A))→ (~B→ ((~A→ ~B)→ (~B→A))) | Instance of Axiom A1. |

4. | (~B → ((~A → ~B) → (B → A))) | From 2 and 3 by modus ponens. |

5. | (~B→((~A→ ~B)→(B→A)))→((~B→(~A→ ~B)→(~B→(B→A))) | Instance of Axiom A2. |

6. | (~B→ (~A → ~B) → (~B → (B → A)) | From 4 and 5 by modus ponens. |

7. | (~B → (B → A) | From 1 and 6 by modus ponens. |

Therefore, for any well-formed formula A and B, (~B → (B →
A) is theorem of **L**^{*}.

This completes the proof.

**Lemma 2 ^{*}**. Show that {~~A}
A holds for any
well-formed formulas A and B of

Proof. We shall construct proof in **L**^{*}.

1. | (~ ~A) | Hypothesis. |

2. | (~ ~A) → ((~ ~ ~ ~A) → (~ ~A)) | Instance of Axiom A1. |

3. | (~ ~ ~ ~A) → (~ ~A) | From 1 and 2 by modus ponens. |

4. | ((~ ~ ~ ~A) → (~ ~A)) → ((~A) → (~ ~ ~A)) | Instance of Axiom A3. |

5. | (~A) → (~ ~ ~A) | From 3 and 4 by modus ponens. |

6. | ((~A) → (~ ~ ~A)) → ((~ ~ A) → A) | Instance of Axiom A3. |

7. | (~ ~ A) → A | From 5 and 6 by modus ponens. |

8. | A | From 1 and 7 by modus ponens. |

Therefore,

{~~A} A

or equivalently,

~~A A

This completes the proof.

The following are the examples of Deductive Proofs in
L^{*}using The Deduction Theorem.

**Lemma 3 ^{*}**. For any well-formed formulas A
and B in

(~B → (B → A))

Note that we have already shown that for any well-formed
formulas A and B,
(~B → (B → A) in Lemma 1^{*}.
[See Above.] But this time we go a little bit differently to illustrate the
simplification produced by the use of the rule 'hypothetical syllogism.'

1. | (~B → (~A → ~B) | Instance of Axiom A1. |

2. | ((~A → ~B) → (B → A) | Instance of Axiom A3. |

7. | (~B → (B → A) | From 1 and 2 by hypothetical syllogism. |

Hope you can see the point I've been making here!

**Lemma 4 ^{*}**. For any well-formed formulas A
and B in

((~A → A) → A)

Proof.

1. | (~A → A) | Hypothesis. |

2. | (~ A → (~ ~ (~A → A) → ~A)) | Instance of Axiom A1. |

3. | (~ ~(~A → A) → ~A) → (A → ~(~A → A)) | Instance of Axiom A3. |

4. | (~ A → (A → ~(~A → A)) | From 2 and 3 by hypothetical syllogism. |

5. | (~A → (A→ ~(~A → A))) → ((~A → A) → (~A → ~(~A → A))) | Instance of Axiom A2. |

6. | (~A → A) → (~A → ~(~A → A)) | From 4 and 5 by modus ponens. |

7. | (~A → ~(~A → A)) | From 1 and 6 by modus ponens. |

8. | (~A → ~(~A → A)) → ((~A → A) → A) | Instance of Axiom A3. |

9. | (~A → A) → A | From 7 and 8 by modus ponens. |

10. | A | From 1 and 9 by modus ponens. |

Hence, (~A → A) A

And by the Deduction Theorem, we have

(~A → A) → A

Therefore, for any well-formed formula A and B, ((~A → A) → A)
is theorem of **L**^{*}.

This completes the proof.

**Lemma 5 ^{*}**. Show that the following well-formed formula is
a theorem of

For any well-formed formulas A and B, ((B → A) → (~A → ~B)).

We shall show the proposition by using the Deduction Theorem and the result {~~A} A [See Example of Proofs.]

Proof.

1. | B → A | Hypothesis. |

2. | ~ ~B → B | By Lemma 2^{*} and the Deduction
Theorem. |

3. | ~ ~B → A | From 2 and 1 by hypothetical syllogism. |

4. | A → ~~A | By the result {~~A} A |

5. | ~~B → ~~A | From 3 and 4 by hypothetical syllogism. |

6. | (~~B → ~~A) → (~A → ~B) | Instance of Axiom 3. |

7. | ~A → ~B | From 5 and 6 by modus ponens. |

Hence, (~B → A) ( ~A → ~B)

And by the Deduction Theorem, we have

(~B → A) → ( ~A → ~B)

Therefore, for any well-formed formula A and B, ((B
→ A) → (~A → ~B)) is theorem of **L**^{*}.

This completes the proof.

**Lemma 6 ^{*}**. Show that the following well-formed formula is
a theorem of

For any well-formed formulas A and B, ~(A → B) → (B → A).

Proof.

1. | ~(A → B) | Hypothesis. |

2. | (B → (A → B)) → (~(A → B) → ~B) | By Lemma 5^{*}. |

3. | B → (A → B) | Instance of Axiom 1. |

4. | ~(A → B) → ~B | From 2 and 3 by modus ponens. |

5. | ~B | From 1 and 5 by modus ponens. |

6. | ~B → (B → A) | By Lemma 1^{*}. |

7. | B → A | From 5 and 6 by modus ponens. |

Hence, ~(A → B) (B → A)

And by the Deduction Theorem, we have

~(A → B) → (B → A)

Therefore, for any well-formed formula A and B, (~(A →
B) → (B → A)) is theorem of **L**^{*}.

This completes the proof.