I've been working on some examples and exercises, and I think I'm getting there, there are however 4 exercises I'm having some difficulties with, I was hoping I could get soms feedback on them, since they're a bit harder than the rest. I think I've done 2 of them reasonably well, the other 2 not so much Still, just implication and conjunction.

1) (P => Q) => (P => (P ^ Q))

Code:

1, H: P => Q
2, H: P
3, => E 1,2: Q
4, ^I 2,3: P ^ Q
5, =>I 2,4: P => (P ^ Q)
6, =>I 1,5: (P => Q) => (P => (P ^ Q))

Seems sound, right?

2) ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))

Code:

1, H: (P => Q) ^ (R => S)
2, H: (P ^ R)
3, ^E 1: P => Q
4, ^E 1: R => S
5, ^E 2: P
6, ^E 2: R
7, =>E 3,5: Q
8, =>E 4,6: S
9, ^I 5,6: P ^ R
10, ^I 7,8: Q ^ S
11, =>I 9, 10: (P ^ R) => (Q ^ S)
12, =>I 1, 11: ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))

I think I did this okay, I have no idea how to do this otherwise.

3) (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))

Code:

1, H: P => Q
2, H: P ^ R
3, ^E 2: P
4, ^E 2: R
5, =>E 1,3: Q
6, =>I 4,1: R => (P = > Q)
7, H: P ^ R
8, ^E 7: P
9, =>E 1,8 Q
10, =>I 7,9: (P ^ R) => Q
11, ^I 6, 10: (R => (P => Q)) ^ ((P ^ R) => Q)
12, =>I 1, 11: (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))

This one I'm not so sure about. Seems a bit redundant to assume P ^ Q twice for example, but I'm not sure how else I can get to the ^I I need to connect the two parts.

And lastly:

4) (P => (Q => R)) => ((P => Q) => (P => R))

And this one I get stuck, doing too many assumptions.

I tried the following

Code:

1, H: P => (Q => R)
2, H: P ^ Q
3, ^E 2: P
4, ^E 2: Q
5, =>I 2,3: P => Q
6, H: P ^ Q
7, ^E 6: P
8, ^E 6 Q
9, =>E 1,7: Q => R
10, =>E 8,9: R
11, =>I 7, 10: P => R

Im stuck here, again, assuming the same thing twice just seems wrong. I can't really wrap my head around it, any tips? I seem to miss an assumption as well, but if I would assume P, well think im being twice as redundant :P May be it's super easy, but I think this is rather harder than the other exercises hehe