[FOM] question about Mendelson's Intro to Math Logic

[Paulo Oliva]

Hi Bob

I think you mean replacing it with (not B -> not C) -> (C -> B), the one you wrote (not B -> not C) -> (B -> C) is not valid.

Anyway, here is a sketch of how it should go. Assume 

(*) (not B -> not C) -> (C -> B)

and let’s derive A3. If you take C be true (e.g. axiom A1) in (*) one can conclude not not B -> B, i.e. double negation elimination DNE.
Then, in order to derive (not C -> not B) -> (not C -> B) -> C one first assumes not C and given the two premises concludes B and not B,
and hence not not C. By DNE we get C.

We’ve used contraction (used not C twice) but that follows from A2.

Formalising all this just using cut will probably be painful, but it’s clear it can be done since there is
a simple translation from natural deduction to Hilbert style proofs.

On 10 Feb 2014, at 00:58, Robert Lubarsky <lubarsky.robert at comcast.net> wrote:

> There’s an exercise from Mendelson’s Intro to Mathematical Logic that I cannot do, and would like an answer to. In the 5th edition, it’s 1.59 on p. 39. Namely, he gives three axioms for a Hilbert-style propositional proof system. The first two are essentially the combinators s and k. The third is
> (not C -> not B) -> [ (not C -> B) -> C ]. The exercise in question is to show that, if you replace this last schema with (not B -> not C) -> (B -> C) then the new system proves the same as the old. I don’t see how to do this.
>  
> My attempt is as follows. We can use the deduction theorem. So assume (not C -> not B) and (not C -> B), with the goal of proving C. From the new schema, we get  B -> C. We can compose that with (not C -> B) to get (not C -> C). I don’t see how to go from that to C within this system.
>  
> Bob Lubarsky
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

--
Paulo Oliva
Royal Society University Research Fellow
Queen Mary University of London
London E1 4FZ
+44 (0) 207 882 5255
http://www.dcs.qmul.ac.uk/~pbo



-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140212/32a24c43/attachment-0001.html>