[FOM] Mendelson exercise (from Luigi Oliveri)

[Arnon Avron]

Since FOM is a very respectable place, I should note
that Oliveri's solution given below to Mendelson's exercise
is full of gaps (to say the least). They mainly boil down
to one fundamental mistake: one cannot use for the new system 
facts proved in  the text for the official one without
showing that they indeed obtain for the new one too.

Here are the gaps in Oliveri's  solution:

Line (5): what is used here is *not* (A*), but the 
  tautology (B=>C)=>(Not C=> Not B). This tautolgy
  should be proved first using in the new system (which 
  is what I did in Lemma 3 of my solution).

Line (6): This single line includes two gaps. First of
  all, the equivalence of A and not not A is used -
  but this equivalence should first be proved for the
  new system (which is what I did in Lemma 1 and Lemma 2
  of my solution). Second: one should prove that the
  rule of  subst. equiv. holds for the new system 
  (this boils down again to proving in it the schema
  (B=>C)=>(Not C=> Not B) mentioned above).

Line (8): Lemma 1.10(g), which is supposed to provide
  the justification of this line, was proved in the text
  for the main system used in the book. One has to
  show here that it is true also for the new system.

Arnon Avron



On Thu, Feb 13, 2014 at 12:49:03PM -0800, Martin Davis 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