In this particular sequent:
q ⊢(p∧q)∨(¬p∧q)
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.
The end confuses me as well. I'd say you first show by Conjunction Introduction $$q,p\vdash p\land q$$ and from this by Disjunction Introduction $$q,p\vdash (p\land q)\lor (\neg p\land q)$$ and from this by Deduction $$\tag1q\vdash p\to ((p\land q)\lor (\neg p\land q)).$$ The same way, we show $$\tag2q\vdash \neg p\to ((p\land q)\lor (\neg p\land q)).$$ It seems you accept Tertium Non Datur $$\tag3\vdash p\lor \neg p, $$ so that we obtain by Disjunction Elimination from $(1)$, $(2)$, $(3)$ $$ q\vdash (p\land q)\lor (\neg p\land q).$$