In this particular sequent:
which is invalid (I drew a Truth Table, since it wasn't self-evident to me); the following explanation has been given:
The premise is q. By (tnd) we get p ∨ ¬p. We know start an assumption based proof based on the latter. Assume: p In this case by (∧i) we get p ∧ q. Assume: ¬p In this case by (∧i) we get ¬p ∧ q. Thus ¬p ∧ q holds only on the premise q.
I understand the need for a contradiction based assumption proof, however, I am having trouble connecting the last sentence in the explanation to proving invalidity. I actually had to draw a truth-table to see that this sequent was invalid.
My question is: how do I figure during writing my proof (the way it is formally done) that the sequent I am trying to proof is actually not valid? I continue to apply rules and things usually work out if the formulae are valid, but I can't seem to be able to tell during a proof that it is invalid.