Comp Sci - Natural Deduction..

[gam3r]

Well...I'm not sure where to post this, but i think i will get the most replies here..

I'm finding natural deduction really, really tough especially formulae with ¬(negation) in it! Can anyone help me with this example, i don't understand the whole subcomputation box! Here is one my questions along with the answer. Why are we looking for Q,P,¬P in the first subcomp box?

If anyone can help, it would be very much appreciated.

 

[gam3r]

Lol yea, it's doing my nut in as well :O

 

[gam3r]

Ahh, i did a logic module last year for my course. SOO hard.

Have you tried looking at truth tables for the various connectives(i've forgot their technical name)?

Truth tables are are not part of this model, this is syntactical proof system, no truth tables needed!