[FOM] Mendelson exercise (from Luigi Oliveri)
Jeff Hirst
jlh at math.appstate.edu
Fri Feb 14 15:35:36 EST 2014
Hi Gianluigi-
I just glanced at your proof, but is (5) actually an application of A*?. It looks like the converse of A* to me…
-Jeff Hirst
On Feb 13, 2014, at 3:49 PM, Martin Davis <martin at eipye.com> wrote:
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
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom
Jeff Hirst, Professor of Mathematics
Department of Mathematical Sciences
Appalachian State University
Boone, NC 28608
828-262-2861 jlh at math.appstate.edu
More information about the FOM
mailing list