[FOM] Mendelson exercise (from Luigi Oliveri)
Martin Davis
martin at eipye.com
Thu Feb 13 15:49:03 EST 2014
Dear Bob,
The version of the Mendelson book available to me is the third. However,
the exercise you mention seems to correspond to Exercise 1.58, p. 39 of the
third edition. If this is the case, then since (not A => not B) => (B => A)
is a theorem of the original system L (Lemma 1.10 (d)), the only thing you
need to do is to prove (not B => not A) => ((not B => A) => B)) from (A*)
(not A => not B) => (B => A). This can be done in the following way:
(1) (not B => not A) Assumption
(2) (not B => A) Assumption
(3) (not B => not A) => (A => B) (A*)
(4) (A => B) M.P. (1), (3)
(5) (not B => A) => (not A => not not B) (A*)
(6) (not B => A) => (not A => B) subst. equiv. (5)
(7) (not A => B) M.P. (2), (6)
(8) (A => B) => ((not A => B) => B) Lemma 1.10 (g), p. 31
(9) ((not A => B) => B) M.P. (4), (8)
(10) B M.P. (7), (9)
(11) (not B => A) => B Deduct. Theor. (2), (10)
(12) (not B => not A) => ((not B => A) => B) Deduct. Theor. (1), (11).
Best wishes,
Gianluigi Oliveri
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140213/931676ee/attachment.html>
More information about the FOM
mailing list