Thread: Hilbert System Proof. ( p /\ q ) -> (q /\ p )

Hey guys, as the title describes i need some help for this proof!

I have to use these operations and i "just" need to find the right part of the proof.

1. {q -> ~p, ~~p} l- _______ ? ? ? Assumption
2. {q -> ~p, ~~p} l- _______ ? ? ? Thereom 3.25
3. {q -> ~p, ~~p} l- _______ ? ? ? MP 1,2
4. {q -> ~p, ~~p} l- _______ ? ? ? Assumption
5. {q -> ~p, ~~p} l- _______ ? ? ? MP 3,4
6. {q -> ~p, ~~p} l- _______ ? ? ? Thereom 3.23
7. {q -> ~p, ~~p} l- _______ ? ? ? MP 5,6
8. {q -> ~p} l- _______ ? ? ? Dedcution 7
9. {q -> ~p} l- _______ ? ? ? Contrapositive 8
10. {q -> ~p} l- _______ ? ? ? Contrapositive 9
11. l- _______ ? ? ? Deduction 10
12. l- _______ ? ? ? Thereom 3.25
13. l- _______ ? ? ? MP 11,12
14. l- ( p /\ q ) -> (q /\ p ) Definition of /\

Anyone else ? :-D

Originally Posted by Mathic

Anyone else ? :-D

Please do not bump!
You have posted a question that seems to be textbook specific.
How are we expected what theorem 3.25 is? We have no way to know.
So why do you expect help?

Plato is right: you need to say what Theorems 3.23 and 3,25 are and what is the definition of /\. I'll venture a guess that p /\ q is ~(p -> ~q), Theorem 3.23 is q -> ~~q and Theorem 3.25 is (p -> q) -> (~q -> ~p). Then the derivation would be as follows.

1. {q -> ~p, ~~p} l- q -> ~p Assumption
2. {q -> ~p, ~~p} l- (q -> ~p) -> (~~p -> ~q) Thereom 3.25
3. {q -> ~p, ~~p} l- ~~p -> ~q MP 1,2
4. {q -> ~p, ~~p} l- ~~p Assumption
5. {q -> ~p, ~~p} l- ~q MP 3,4
6. {q -> ~p, ~~p} l- ~q -> ~~~q Thereom 3.23
7. {q -> ~p, ~~p} l- ~~~q MP 5,6
8. {q -> ~p} l- ~~p -> ~~~q Deduction 7
9. {q -> ~p} l- ~~q -> ~p Contrapositive 8
10. {q -> ~p} l- p -> ~q Contrapositive 9
11. l- (q -> ~p) -> (p -> ~q) Deduction 10
12. l- ((q -> ~p) -> (p -> ~q)) -> (~(p -> ~q) -> ~(q -> ~p)) Thereom 3.25
13. l- ~(p -> ~q) -> ~(q -> ~p) MP 11,12
14. l- ( p /\ q ) -> (q /\ p ) Definition of /\