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.

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

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

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

Quote:

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?

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

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.

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