[FOM] Mendelson exercise (from Luigi Oliveri)

Robert Lubarsky Lubarsky.Robert at comcast.net
Sat Feb 15 09:52:04 EST 2014

```The proof below is incorrect. (5) is not an instance of (A*). And for (6), B
and not not B have not been proven to be equivalent. After that I stopped

I thank Arnon Avron and Paulo Oliva for their correct answers (in the latter
case with some off-line additions to the argument).

Bob Lubarsky

From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] On Behalf Of
Martin Davis
Sent: Thursday, February 13, 2014 3:49 PM
To: fom at cs.nyu.edu
Subject: [FOM] Mendelson exercise (from Luigi Oliveri)

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/20140215/007f50f1/attachment.html>
```