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 L remain theorems of extended formal system L^* (and new theorems are possibly introduced.) As an example, suppose we decided to replace Axiom 3 of our formal system L  by the following:

((~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^*.

Deduction Rules of Extend formal system L^*.

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 A and B, (~B → (B → A).

Proof. We shall construct proof in L^*.

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 L^*.

Proof. We shall construct proof in L^*.

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 L^*, show that the following is theorem of L^*.

(~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.'

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

Lemma 4^*. For any well-formed formulas A and B in L^*, show that the following is theorem of L^*.

((~A → A) → A)

Proof.

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 L^*.

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 L^*.

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

Proof.

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.