PM (IV) – Independence and Non-Independence
T56 is of course the same wff as the axiom A4; and the proof we have set out shows that it is unnecessary to put it down as an axiom, since it can be proved from the other axioms and therefore everything that can be proved by use of A4 can be proved by use of T56. We express this fact by saying that A4 is a non-independent axiom. This does not mean that it is in any way impaired as an axiom, but merely that we can do without it. In fact it is sometimes very conveulent, 132even if theoretically untidy, to have one or more non-independent axioms in a system. For example, in the present case, having A4 as an axiom allowed us to obtain the very useful Perm easily at an early stage. However, inspection of the proof of T56 will show that the only thesis used, apart from Al, A2, A3 and A5, is Syll in the form ‘(q⊃r) d ((p⊃q) ⊃ (p⊃r))’, so that T56 could, in principle, be proved at a very early stage.