Deduction law
Sandip Ray
of you seem to have been confused by the proof, in particular the use
of induction. Part of the confusion might stem from the fact that
this is an instance of a property we prove _about our logic_, and we
do so outside the logic. So in this note I'll try to clarify what it
is that we did with the proof, and why we are justified in doing that.
First, for this note, we will make the following distinction between a
"derivation" and a "proof". A _derivation_ is a sequence of formulas
where each formula in the sequence is either an axiom or can be
derived from the previous formulas using the inference rules. (We say
that the last formula in such a sequence is a _theorem_ and the
sequence to be a derivaton of the formula.) A _proof_ is a
mathematical argument showing the truth of a certain proposition.
Aside: In the class we very rarely make the above distinction between
a proof and a derivation. This is because the course is about _using_
the logic we are defining, not about studying the properties of the
logic itself. But for this particular case we do make the above
distinction since we are trying to prove a proposition about the logic
itself.
We will state the deduction law more carefully below. But first here
are some definitions. Suppose A be any formula. We define an
A-derivation to be a sequence of formulas such that each formula is
either an axiom or the formula A, or is obtained from the previous
formulas in the sequence by the application of the inference rules.
Let B be the last formula in such an A-derivation. We then call the
sequnce an A-derivation of B.
Deduction Law: Suppose there is an A-derivation of B then there is
always a derivation of the formula A => B.
What we discussed in class was a _proof_ of the deduction law. That
is, we provided an _argument_ that shows that whenever there is an
A-derivation of B there is a derivation of A => B.
To recap the proof, here are the key steps. First, we assumed the
following three derived rules of inference.
(1) Generalized expansion:
Derive P => (Q v R) from P => Q
(2) Generalized contraction:
Derive P => Q from P => (Q v Q)
(3) Generalized Associativity:
Derive P => ((Q v R) v S) from P => (Q v (R v S))
(4) Generalized Cut:
Derive P => (Q v R) from P => (S v Q) and P => (~S v R)
We leave the above derived rules of inference as exercises. They can
be proven by the same approaches that we used in class to prove other
derived rules of inference.
Now we prove the deduction law by induction on the length of
A-derivation. The statement we prove by induction is as follows:
Let sigma be any A-derivation. Then for each formula alpha in
sigma, the formula A => alpha is a theorem.
Proof
=====
Base case: If the length of sigma is 1. The first formula in an
A-derivation is either an axiom of the formula A. We are then done
because of propositional axiom.
Induction step: We assume that the length of sigma is greater than 1,
sigma' is the prefix of sigma minus the last formula and gamma is the
last formula, and we assume that the proposition holds for sigma'.
Then we consider the cases for production of gamma.
(a) gamma is either an axiom or the formula A. Then we are done by
the propositional axiom.
(b) gamma is formed by applying any of the inference rules expansion,
contraction, associativity, and cut on (at most) two formulas
gamma_1 and gamma_2 in sigma'.
We can then use the induction hypothesis to show that A => gamma_1
and A => gamma_2 are theorems. Then the proposition follows by
the derived inference rules (1) - (4) above.
Q.E.D.
Note that the above proof never assumed that the formula alpha is a
theorem. We assume that if there is an A-derivation of alpha then
(A => alpha) is a theorem.
There was some concern in the class and in the emails you guys sent me
on why we are justified in using induction to do this proof. The
concern, which is well-justified, is that induction is a very powerful
rule but we never (as yet) provided it as a rule of inference. This
is an important point, which needs to be clarified at this stage.
First, consider what we have set out to do in case of the deduction
law, which is different in a certain sense from the previous
statements we have shown. For the deduction law, we are trying to
find a _proof_ (and _not_ a derivation) that when an A derivation ends
with alpha then there is a theorem of the form A => alpha. That is,
what we are doing here is a proof of a property about the logic
itself, and we are providing an arugument _outside the logic_ to do
so. (The reason we are doing it outside the logic is because the
logic itself does not provide a way to go from an A-derivation to a
derivation.) For doing such a _proof_, we are allowed to invoke _any_
mathematical argument that we know of. So in this case, we could use
induction. Note that we have not used induction to _derive_ a formula
in the logic. The deduction law is just a property of the logic which
we have proven outside the logic, and we will make use of instances of
the property in our later derivations.
Now, informally, on to the role of the induction in the above proof.
What induction lets us do is to assume, for every formula alpha in the
A-derivation, that the formula A => alpha is a theorem. In other
words, all that we did by induction is to stick in the form "A =>" to
the left of every formula that we had been produced in the
A-derivation, and claim that the resulting formula is a theorem. This
has been possible since wherever we used a given (the formula A), in
the A-derivation, we now stick in the propositional axiom (or law of
excluded middle) ~A v A, and the rest follows by the above derived
rules of inference.
Hope this clarifies the confusions that some of you might have.
Please feel free to post here if there are more questions. Although
these first few things about logic might seem simple and boring, it is
important that everyone is absolutely clear on these points.
Thanks,
-- Sandip