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

[Arnon Avron]

Hi Bob,

Here is one way to do it (I do not know if the shortest). In what follows
I freely use the implicational fragment of intuitionistic logic
and the deduction theorem.

Lemma 1: not not A-> A
Proof: Start from not not A -> ( not not  not not A ->  not not A).
 Apply the new axiom twice to get not not A -> ( not not A->A).
 Then apply contraction

Lemma 2: A-> not not A
Proof: From Lemma 1 infewr: not  not not A ->  not A. Now
 apply the new axiom.

Lemma 3: (B -> C)->(not B -> not C)
Proof: From Lemma 1 and Lemma 2 it is easy to prove that
  (B -> C)->(not not B -> not not C). Now apply the new axiom.

Now to prove (not C -> C)->C start with not C-> ((not C -> C)->C).
By Lemma 3 one can infer from it: not C-> (not C-> not (not C -> C)).
Applying contraction we get not C->not (not C -> C). A final
application of the new axioms yields (not C -> C)->C.

Cheers

Arnon


On Sun, Feb 09, 2014 at 07:58:12PM -0500, Robert Lubarsky 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