# Checking validity other than Truth Table.

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.

• Could you elaborate what you mean with the sequent being invalid? – Hagen von Eitzen Feb 10 '19 at 14:08

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).$$